A tableau calculus for minimal model reasoning

DOI10.1007/3-540-61208-4_18zbMath1412.68247OpenAlexW2167440926MaRDI QIDQ4645243

Ilkka Niemelä

Publication date: 10 January 2019

Published in: Theorem Proving with Analytic Tableaux and Related Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61208-4_18

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Mechanization of proofs and logical operations (03B35)

Related Items

Exploring Theories with a Model-Finding Assistant, Cautious reasoning in ASP via minimal models and unsatisfiable cores, Reasoning under minimal upper bounds in propositional logic, Minimal sets on propositional formulae. Problems and reductions, ASP and subset minimality: enumeration, cautious reasoning and MUSes, Better Paracoherent Answer Sets with Less Resources, Paracoherent answer set computation, Theorem proving techniques for view deletion in databases, On the equivalence of the static and disjunctive well-founded semantics and its computation, A Tableau Calculus for Minimal Modal Model Generation, Hyper tableaux, An abductive framework for negation in disjunctive logic programming, Possible models computation and revision -- a practical approach

Uses Software

• SATCHMO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Tableaux and sequent calculus for minimal entailment
• An algorithm to compute circumscription
• A circumscriptive theorem prover
• Ordered model trees: A normal form for disjunctive deductive databases
• Computing circumscriptive databases
• Static semantics for normal and disjunctive logic programs
• Propositional circumscription and extended closed-world reasoning are \(\Pi_ 2^ P\)-complete
• The Taming of the Cut. Classical Refutations with Analytic Cut
• Minimal model generation with positive unit hyper-resolution tableaux