Tableau-based characterization and theorem proving for default logic
Ray Reiter's default logic is a propositional or predicate logic system augmented with so-called defaults. Defaults are rules of the form `if \(a\) holds and \(b\) can be consistently assumed then \(c\) can be derived', `\(b\) can be consistently assumed' means that the negation of \(b\) is not provable. This is a highly nonmonotonic system because adding new facts may prevent the application of a default rule. Moreover, one cannot do simple forward reasoning. The application of a default rule may add new facts which destroy the property that \(b\) can be consistently assumed. In the model theory of default logic there is therefore the notion of an extension. An extension is a maximally consistent set of formulae where further applications of defaults do not add new facts. A database consisting of some facts and some default rules may have no extension at all (then it is inconsistent), it may have one extension and it may have several extensions. If the basic logic is undecidable, then the extension with defaults is not even semidecidable anymore because the applicability of a default rule cannot be decided. Therefore defaults have mostly been investigated for decidable basic logics, in particular propositional logic. This paper considers default reasoning for the propositional case and briefly mentions an extension to predicate logic without function symbols, which is decidable. The authors present a method for deciding whether there are extensions of a given default theory and for computing these extensions. In contrast to previously proposed methods, which operate in a forward reasoning mode, the algorithm generates candidates for the extensions and then manipulates these candidates until extensions are obtained. The candidates are models of the basic facts, they are generated with a tableaux system, combined with models of the conclusions of the defaults. For all maximally consistent subsets of the candidates it is then checked whether the conclusions of the defaults are actually justified, i.e. whether the two preconditions hold. The algorithm is implemented in PROLOG II, but no systematic performance tests are reported.
- 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
- 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
- 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?)
- Saturation, nonmonotonic reasoning and the closed-world assumption
- Tableaux and sequent calculus for minimal entailment
- The foundations of mathematics. A study in the philosophy of science
- The Pure Logic of Necessitation
- Prolog technology for default reasoning: proof theory and compilation techniques
- Is default logic a reinvention of inductive-statistical reasoning?
- Alternative foundations for Reiter's default logic
- Computing with default logic
- Default reasoning using classical logic
- A tableaux calculus for default intuitionistic logic
- Consistency defaults
- A propositional tableaux based proof calculus for reasoning with default rules
- Realizing Default Logic over Description Logic Knowledge Bases
- Default databases: Extending the approach of deductive databases using default logic
- scientific article; zbMATH DE number 140388 (Why is no real title available?)
- scientific article; zbMATH DE number 516983 (Why is no real title available?)
- scientific article; zbMATH DE number 517004 (Why is no real title available?)
- scientific article; zbMATH DE number 1748572 (Why is no real title available?)
- A sequent calculus for skeptical Default Logic
- Sequent calculi for default and autoepistemic logics
- \(\mathsf{XRay}\): a Prolog technology theorem prover for default reasoning: a system description
- Analytic tableaux for default logics
- A proof theoretical approach to default reasoning I: tableaux for default logic
- Skeptical rational extensions
- A query answering algorithm for Lukaszewicz' general open default theory
- A system for computing constrained default logic extensions
- DARR- a theorem prover for constrained and rational default logics
- Proof complexity of non-classical logics
- Proof complexity of propositional default logic
- A tableaux-based theorem prover for a decidable subset of default logic
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)
