A tableau calculus for minimal model reasoning

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

64 Citations (Scopus)

Abstract

The paper studies the automation of minimal model inference, i.e., determining whether a formula is true in every minimal model of the premises. A novel tableau calculus for propositional minimal model reasoning is presented in two steps. First an analytic clausal tableau calculus employing a restricted cut rule is introduced. Then the calculus is extended to handle minimal model inference by employing a groundedness property of minimal models. A decision procedure based on the basic calculus is devised and then it is extended to minimal model inference. The basic decision procedure and its extension enjoy some interesting properties. When deciding logical consequence, the basic procedure explores the search space of counter-models with a preference to minimal models and each counter-model is not generated more than once. The procedures can be implemented to run in polynomial space, and they provide polynomial time decision procedures for Horn clauses. The extended decision procedure can also be used to finding all minimal models of a set of clauses.

Original languageEnglish
Title of host publicationTheorem Proving with Analytic Tableaux and Related Methods - 5th International Workshop, TABLEAUX 1996, Proceedings
Subtitle of host publicationTerrasini, Palermo, Italy, May 15–17, 1996
EditorsP Miglioli, U Moscato, D Mundici, M Ornaghi
Pages278-294
Number of pages17
ISBN (Electronic)978-3-540-68368-1
DOIs
Publication statusPublished - 1996
MoE publication typeA4 Article in a conference publication
EventInternational Workshop on Theorem Proving with Analytic Tableaux and Related Methods - Palermo, Italy
Duration: 15 May 199617 May 1996
Conference number: 5

Publication series

NameLecture Notes in Artificial Intelligence
PublisherSPRINGER-VERLAG BERLIN
Volume1071
ISSN (Print)0302-9743

Workshop

WorkshopInternational Workshop on Theorem Proving with Analytic Tableaux and Related Methods
Abbreviated titleTABLEAUX
CountryItaly
CityPalermo
Period15/05/199617/05/1996

Keywords

  • CIRCUMSCRIPTION
  • DATABASES

Cite this