Minimal model generation with positive unit hyper-resolution tableaux
- 1 January 1996
- book chapter
- Published by Springer Nature
- p. 143-159
- https://doi.org/10.1007/3-540-61208-4_10
Abstract
No abstract availableKeywords
This publication has 9 references indexed in Scilit:
- A tableau calculus for minimal model reasoningPublished by Springer Nature ,1996
- Ordered model trees: A normal form for disjunctive deductive databasesJournal of Automated Reasoning, 1994
- Controlled integration of the cut rule into connection tableau calculiJournal of Automated Reasoning, 1994
- First-order syntactic characterizations of minimal entailment, domain-minimal entailment, and Herbrand entailmentJournal of Automated Reasoning, 1993
- Tableaux and sequent calculus for minimal entailmentJournal of Automated Reasoning, 1992
- Embedding negation as failure into a model generation theorem proverPublished by Springer Nature ,1992
- Model minimization ?An alternative to circumscriptionJournal of Automated Reasoning, 1988
- SATCHMO: A theorem prover implemented in PrologPublished by Springer Nature ,1987
- An improved proof procedure1Theoria, 1960