Models and quantifier elimination for quantified Horn formulas

DOI10.1016/j.dam.2007.10.005zbMath1152.68051OpenAlexW2027576655MaRDI QIDQ944709

Hans Kleine Büning, Uwe Bubeck

Publication date: 10 September 2008

Published in: Discrete Applied Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.dam.2007.10.005

zbMATH Keywords

quantifier eliminationsatisfiabilitymodelquantified Boolean formulaquantified Horn formula

Mathematics Subject Classification ID

Related Items (5)

Disjunctive closures for knowledge compilation ⋮ Transformations into Normal Forms for Quantified Circuits ⋮ Complexity of validity for propositional dependence logics ⋮ Complexity and expressive power of second‐order extended Horn logic ⋮ Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits

Uses Software

• Quantor

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• Resolution for quantified Boolean formulas
• Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae
• Bounded Universal Expansion for Preprocessing QBF
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• On sentences which are true of direct unions of algebras

This page was built for publication: Models and quantifier elimination for quantified Horn formulas