Minimal model generation with positive unit hyper-resolution tableaux

DOI10.1007/3-540-61208-4_10zbMATH Open1412.68212OpenAlexW1528245710MaRDI QIDQ4645233FDOQ4645233

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

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

zbMATH Keywords

minimal modelexpansion ruleground atomopen branchredundant model

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• An improved proof procedure1
• Title not available (Why is that?)
• Tableaux and sequent calculus for minimal 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
• First-order syntactic characterizations of minimal entailment, domain- minimal entailment, and Herbrand entailment
• Title not available (Why is that?)

Cited In (11)

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

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)