A tableau prover for domain minimization

DOI10.1007/BF00881950zbMath0815.03004OpenAlexW2081898972MaRDI QIDQ1344878

Sven Lorenz

Publication date: 22 February 1995

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00881950

zbMATH Keywords

nonmonotonic logicminimal entailmentdomain circumscriptiondomain minimizationtableau theorem proving

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Mechanization of proofs and logical operations (03B35)

Related Items

General domain circumscription and its first-order reduction, Blocking and other enhancements for bottom-up model generation methods, A Tableau Calculus for Minimal Modal Model Generation, MiniTab

Cites Work

• Tableaux and sequent calculus for minimal entailment
• Formalizing nonmonotonic reasoning systems
• An algorithm to compute circumscription
• A circumscriptive theorem prover
• Circumscription - a form of non-monotonic reasoning
• The mathematics of non-monotonic reasoning
• First-order syntactic characterizations of minimal entailment, domain- minimal entailment, and Herbrand entailment
• On the relative merits of path dissolution and the method of analytic tableaux
• The liberalized \(\delta\)-rule in free variable semantic tableaux
• Unnamed Item