Minimal model generation with positive unit hyper-resolution tableaux
From MaRDI portal
Publication:4645233
DOI10.1007/3-540-61208-4_10zbMath1412.68212OpenAlexW1528245710MaRDI QIDQ4645233
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
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
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