Prolog technology for default reasoning: proof theory and compilation techniques

DOI10.1016/S0004-3702(98)00092-7zbMATH Open0909.68161OpenAlexW4248795502MaRDI QIDQ1275596FDOQ1275596

Torsten Schaub, Stefan Brüning

Publication date: 12 January 1999

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0004-3702(98)00092-7

Recommendations

• scientific article; zbMATH DE number 516983
• \(\mathsf{XRay}\): a Prolog technology theorem prover for default reasoning: a system description
• scientific article; zbMATH DE number 1748572
• scientific article; zbMATH DE number 1301757

zbMATH Keywords

automated reasoningdefault reasoningdefault logicmodel eliminationmodel-based consistency checkingPTTP

Mathematics Subject Classification ID

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• A Computing Procedure for Quantification Theory
• SETHEO: A high-performance theorem prover
• A Prolog technology theorem prover: A new exposition and implementation in Prolog
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• An algorithm to compute circumscription
• Title not available (Why is that?)
• A logic for default reasoning
• Title not available (Why is that?)
• Title not available (Why is that?)
• A logical framework for default reasoning
• Title not available (Why is that?)
• Basis property in \(L_{p}(0, 1)\) of the system of eigenfunctions corresponding to a problem with a spectral parameter in the boundary condition
• Title not available (Why is that?)
• Complexity Results for Nonmonotonic Logics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Alternative approaches to default logic
• Title not available (Why is that?)
• Default reasoning by deductive planning
• Title not available (Why is that?)
• Mechanical Theorem-Proving by Model Elimination
• Tableau-based characterization and theorem proving for default logic
• A sequent calculus for skeptical Default Logic
• Sequent calculi for default and autoepistemic logics
• A proof theoretical approach to default reasoning I: tableaux for default logic
• Cumulative default logic: In defense of nonmonotonic inference rules
• Compiling a default reasoning system into Prolog
• Model elimination without contrapositives
• A circumscriptive theorem prover
• Title not available (Why is that?)
• Title not available (Why is that?)
• Refutation graphs
• Controlled integration of the cut rule into connection tableau calculi
• Title not available (Why is that?)
• On cumulative default logics
• A decision method for nonmonotonic reasoning based on autoepistemic reasoning
• A new methodology for query answering in default logics via structure-oriented theorem proving
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Towards a classification of defaults logics
• XRay: A prolog technology theorem prover for default reasoning: A system description
• Analytic tableaux for default logics
• KoMeT
• A tableaux-based theorem prover for a decidable subset of default logic

Cited In (3)

• Compiling a default reasoning system into Prolog
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• Investigating the Mapping between Default Logic and Inconsistency-Tolerant Semantics

Uses Software

• SETHEO
• GraphBase
• SCOTT
• Datalog
• PROTEIN
• KoMeT

This page was built for publication: Prolog technology for default reasoning: proof theory and compilation techniques

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