A tableau calculus for minimal model reasoning

DOI10.1007/3-540-61208-4_18MaRDI QIDQ4645243zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• A tableau calculus for minimal modal model generation
• On computing minimal models
• Positive unit hyperresolution tableaux and their application to minimal model generation
• Reasoning with minimal models: efficient algorithms and applications
• Minimal model generation with positive unit hyper-resolution tableaux

Cites work

• A circumscriptive theorem prover
• An algorithm to compute circumscription
• Computing circumscriptive databases
• scientific article; zbMATH DE number 4094866 (Why is no real title available?)
• scientific article; zbMATH DE number 46359 (Why is no real title available?)
• scientific article; zbMATH DE number 1348475 (Why is no real title available?)
• scientific article; zbMATH DE number 592370 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• Minimal model generation with positive unit hyper-resolution tableaux
• Ordered model trees: A normal form for disjunctive deductive databases
• Propositional circumscription and extended closed-world reasoning are \(\Pi_ 2^ P\)-complete
• Static semantics for normal and disjunctive logic programs
• Tableaux and sequent calculus for minimal entailment
• The Taming of the Cut. Classical Refutations with Analytic Cut

Cited in

(22)

• Reasoning with minimal models: efficient algorithms and applications
• A tableau prover for domain minimization
• Positive unit hyperresolution tableaux and their application to minimal model generation
• Minimal sets on propositional formulae. Problems and reductions
• lean\(T^ AP\): Lean tableau-based deduction
• Possible models computation and revision -- a practical approach
• A non-clausal tableau calculus for \textsc{MinSat}
• Paracoherent answer set computation
• A tableau calculus for minimal modal model generation
• Computing minimal models modulo subset-simulation for modal logics
• Exploring theories with a model-finding assistant
• scientific article; zbMATH DE number 1341467 (Why is no real title available?)
• scientific article; zbMATH DE number 1341481 (Why is no real title available?)
• Cautious reasoning in ASP via minimal models and unsatisfiable cores
• Minimal model generation with positive unit hyper-resolution tableaux
• Better paracoherent answer sets with less resources
• Hyper tableaux
• An abductive framework for negation in disjunctive logic programming
• Theorem proving techniques for view deletion in databases
• On the equivalence of the static and disjunctive well-founded semantics and its computation
• ASP and subset minimality: enumeration, cautious reasoning and MUSes
• Reasoning under minimal upper bounds in propositional logic

Describes a project that uses

Uses Software

• SATCHMO

This page was built for publication: A tableau calculus for minimal model reasoning

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