Tableau-based characterization and theorem proving for default logic

DOI10.1007/BF00881957zbMath0815.03005OpenAlexW2085184180MaRDI QIDQ1344885

Vincent Risch, Camilla B. Schwind

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/bf00881957

zbMATH Keywords

algorithmnonmonotonic logicdecidabilitydefault logicdefault reasoningtableau theorem provingcomputation of extensionsPROLOG II

Mathematics Subject Classification ID

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

Related Items

Analytic tableaux for default logics, A sequent calculus for skeptical Default Logic, Proof complexity of propositional default logic, Sequent calculi for default and autoepistemic logics, Proof Complexity of Non-classical Logics, Prolog technology for default reasoning: proof theory and compilation techniques, A system for computing constrained default logic extensions, Is default logic a reinvention of inductive-statistical reasoning?, Alternative foundations for Reiter's default logic

Cites Work

• Tableaux and sequent calculus for minimal entailment
• The foundations of mathematics. A study in the philosophy of science
• Saturation, nonmonotonic reasoning and the closed-world assumption
• Formalizing nonmonotonic reasoning systems
• An algorithm to compute circumscription
• A circumscriptive theorem prover
• A logic for default reasoning
• Circumscription - a form of non-monotonic reasoning
• The Pure Logic of Necessitation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item