Minimal model generation with positive unit hyper-resolution tableaux

DOI10.1007/3-540-61208-4_10MaRDI QIDQ4645233zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Positive unit hyperresolution tableaux and their application to minimal model generation
• scientific article; zbMATH DE number 1341481
• On computing minimal models
• A tableau calculus for minimal modal model generation
• A tableau calculus for minimal model reasoning

Cites work

• scientific article; zbMATH DE number 4094866 (Why is no real title available?)
• scientific article; zbMATH DE number 1348475 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• scientific article; zbMATH DE number 3254919 (Why is no real title available?)
• An improved proof procedure1
• Controlled integration of the cut rule into connection tableau calculi
• 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
• Ordered model trees: A normal form for disjunctive deductive databases
• Tableaux and sequent calculus for minimal entailment

Cited in

(11)

• Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
• Positive unit hyperresolution tableaux and their application to minimal model generation
• Efficient model generation through compilation
• Efficient model generation through compilation.
• A tableau calculus for minimal modal model generation
• Reasoning under minimal upper bounds in propositional logic
• A tableau calculus for minimal model reasoning
• scientific article; zbMATH DE number 177515 (Why is no real title available?)
• Non-Horn magic sets to incorporate top-down inference into bottom-up theorem proving
• Combining enumeration and deductive techniques in order to increase the class of constructible infinite models
• Theorem proving techniques for view deletion in databases

Describes a project that uses

Uses Software

• SATCHMO

This page was built for publication: Minimal model generation with positive unit hyper-resolution tableaux

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