Tableau-based characterization and theorem proving for default logic

DOI10.1007/BF00881957MaRDI QIDQ1344885zbMATH OpenOpenAlexFDO

Authors Vincent Risch, Camilla 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

algorithmdecidabilitynonmonotonic logicdefault reasoningdefault logiccomputation of extensionsPROLOG IItableau theorem proving

Mathematics Subject Classification ID

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

Recommendations

• A tableaux-based theorem prover for a decidable subset of default logic
• Analytic tableaux for default logics
• A proof theoretical approach to default reasoning I: tableaux for default logic
• scientific article; zbMATH DE number 140378
• A propositional tableaux based proof calculus for reasoning with default rules

Cites work

• scientific article; zbMATH DE number 4075021 (Why is no real title available?)
• scientific article; zbMATH DE number 4089520 (Why is no real title available?)
• scientific article; zbMATH DE number 46359 (Why is no real title available?)
• scientific article; zbMATH DE number 4117898 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• A circumscriptive theorem prover
• A logic for default reasoning
• An algorithm to compute circumscription
• Circumscription - a form of non-monotonic reasoning
• Formalizing nonmonotonic reasoning systems
• Saturation, nonmonotonic reasoning and the closed-world assumption
• Tableaux and sequent calculus for minimal entailment
• The Pure Logic of Necessitation
• The foundations of mathematics. A study in the philosophy of science

Cited in

(25)

• A tableaux calculus for default intuitionistic logic
• Realizing Default Logic over Description Logic Knowledge Bases
• Computing with default logic
• scientific article; zbMATH DE number 516983 (Why is no real title available?)
• scientific article; zbMATH DE number 517004 (Why is no real title available?)
• Default reasoning using classical logic
• Default databases: Extending the approach of deductive databases using default logic
• A propositional tableaux based proof calculus for reasoning with default rules
• A tableaux-based theorem prover for a decidable subset of default logic
• Proof complexity of non-classical logics
• Alternative foundations for Reiter's default logic
• A sequent calculus for skeptical Default Logic
• A query answering algorithm for Lukaszewicz' general open default theory
• DARR- a theorem prover for constrained and rational default logics
• Analytic tableaux for default logics
• scientific article; zbMATH DE number 140388 (Why is no real title available?)
• scientific article; zbMATH DE number 1748572 (Why is no real title available?)
• Is default logic a reinvention of inductive-statistical reasoning?
• Consistency defaults
• Sequent calculi for default and autoepistemic logics
• Prolog technology for default reasoning: proof theory and compilation techniques
• Skeptical rational extensions
• Proof complexity of propositional default logic
• A system for computing constrained default logic extensions
• \(\mathsf{XRay}\): a Prolog technology theorem prover for default reasoning: a system description

This page was built for publication: Tableau-based characterization and theorem proving for default logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1344885)