Minimal model generation with positive unit hyper-resolution tableaux

DOI10.1007/3-540-61208-4_10zbMath1412.68212OpenAlexW1528245710MaRDI QIDQ4645233

François Bry, Adnan Yahya

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_10

zbMATH Keywords

minimal modelexpansion ruleground atomopen branchredundant model

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Reasoning under minimal upper bounds in propositional logic, Simplifying and generalizing formulae in tableaux. Pruning the search space and building models, A tableau calculus for minimal model reasoning, Efficient model generation through compilation, Theorem proving techniques for view deletion in databases, Combining enumeration and deductive techniques in order to increase the class of constructible infinite models, Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving, Efficient model generation through compilation.

Uses Software

• SATCHMO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Tableaux and sequent calculus for minimal entailment
• First-order syntactic characterizations of minimal entailment, domain- minimal entailment, and Herbrand entailment
• On the duality of abduction and model generation in a framework for model generation with equality
• Controlled integration of the cut rule into connection tableau calculi
• Ordered model trees: A normal form for disjunctive deductive databases
• An improved proof procedure1