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

Analysis of algorithms and problem complexity (68Q25) Mechanization of proofs and logical operations (03B35) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Quantifier elimination, model completeness, and related topics (03C10)

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