A tableau calculus for minimal model reasoning

Ilkka Niemelä

doi:10.1007/3-540-61208-4_18

A tableau calculus for minimal model reasoning

Ilkka Niemelä

Not published at Aalto University

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-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 language	English
Title of host publication	Theorem Proving with Analytic Tableaux and Related Methods - 5th International Workshop, TABLEAUX 1996, Proceedings
Subtitle of host publication	Terrasini, Palermo, Italy, May 15–17, 1996
Editors	P Miglioli, U Moscato, D Mundici, M Ornaghi
Pages	278-294
Number of pages	17
ISBN (Electronic)	978-3-540-68368-1
DOIs	https://doi.org/10.1007/3-540-61208-4_18
Publication status	Published - 1996
MoE publication type	A4 Article in a conference publication
Event	International Workshop on Theorem Proving with Analytic Tableaux and Related Methods - Palermo, Italy Duration: 15 May 1996 → 17 May 1996 Conference number: 5

Publication series

Name	Lecture Notes in Artificial Intelligence
Publisher	SPRINGER-VERLAG BERLIN
Volume	1071
ISSN (Print)	0302-9743

Workshop

Workshop	International Workshop on Theorem Proving with Analytic Tableaux and Related Methods
Abbreviated title	TABLEAUX
Country	Italy
City	Palermo
Period	15/05/1996 → 17/05/1996

Keywords

CIRCUMSCRIPTION
DATABASES

Access to Document

10.1007/3-540-61208-4_18

Cite this

Niemelä, I. (1996). A tableau calculus for minimal model reasoning. In P. Miglioli, U. Moscato, D. Mundici, & M. Ornaghi (Eds.), Theorem Proving with Analytic Tableaux and Related Methods - 5th International Workshop, TABLEAUX 1996, Proceedings: Terrasini, Palermo, Italy, May 15–17, 1996 (pp. 278-294). (Lecture Notes in Artificial Intelligence; Vol. 1071). https://doi.org/10.1007/3-540-61208-4_18

@inproceedings{0c9ee9090e4f4538ad6a8c0cafc16352,

title = "A tableau calculus for minimal model reasoning",

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.",

keywords = "CIRCUMSCRIPTION, DATABASES",

author = "Ilkka Niemel{\"a}",

year = "1996",

doi = "10.1007/3-540-61208-4_18",

language = "English",

isbn = "3-540-61208-4",

series = "Lecture Notes in Artificial Intelligence",

publisher = "SPRINGER-VERLAG BERLIN",

pages = "278--294",

editor = "P Miglioli and U Moscato and D Mundici and M Ornaghi",

booktitle = "Theorem Proving with Analytic Tableaux and Related Methods - 5th International Workshop, TABLEAUX 1996, Proceedings",

note = "International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, TABLEAUX ; Conference date: 15-05-1996 Through 17-05-1996",

}

Niemelä, I 1996, A tableau calculus for minimal model reasoning. in P Miglioli, U Moscato, D Mundici & M Ornaghi (eds), Theorem Proving with Analytic Tableaux and Related Methods - 5th International Workshop, TABLEAUX 1996, Proceedings: Terrasini, Palermo, Italy, May 15–17, 1996. Lecture Notes in Artificial Intelligence, vol. 1071, pp. 278-294, International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Palermo, Italy, 15/05/1996. https://doi.org/10.1007/3-540-61208-4_18

A tableau calculus for minimal model reasoning. / Niemelä, Ilkka.

Theorem Proving with Analytic Tableaux and Related Methods - 5th International Workshop, TABLEAUX 1996, Proceedings: Terrasini, Palermo, Italy, May 15–17, 1996. ed. / P Miglioli; U Moscato; D Mundici; M Ornaghi. 1996. p. 278-294 (Lecture Notes in Artificial Intelligence; Vol. 1071).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review

TY - GEN

T1 - A tableau calculus for minimal model reasoning

AU - Niemelä, Ilkka

N1 - Conference code: 5

PY - 1996

Y1 - 1996

N2 - 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.

AB - 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.

KW - CIRCUMSCRIPTION

KW - DATABASES

U2 - 10.1007/3-540-61208-4_18

DO - 10.1007/3-540-61208-4_18

M3 - Conference contribution

SN - 3-540-61208-4

SN - 978-3-540-61208-7

T3 - Lecture Notes in Artificial Intelligence

SP - 278

EP - 294

BT - Theorem Proving with Analytic Tableaux and Related Methods - 5th International Workshop, TABLEAUX 1996, Proceedings

A2 - Miglioli, P

A2 - Moscato, U

A2 - Mundici, D

A2 - Ornaghi, M

T2 - International Workshop on Theorem Proving with Analytic Tableaux and Related Methods

Y2 - 15 May 1996 through 17 May 1996

ER -

Niemelä I. A tableau calculus for minimal model reasoning. In Miglioli P, Moscato U, Mundici D, Ornaghi M, editors, Theorem Proving with Analytic Tableaux and Related Methods - 5th International Workshop, TABLEAUX 1996, Proceedings: Terrasini, Palermo, Italy, May 15–17, 1996. 1996. p. 278-294. (Lecture Notes in Artificial Intelligence). https://doi.org/10.1007/3-540-61208-4_18