Models and quantifier elimination for quantified Horn formulas

DOI10.1016/j.dam.2007.10.005zbMath1152.68051MaRDI 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 elimination; satisfiability; model; quantified Boolean formula; quantified Horn formula

Mathematics Subject Classification ID

68Q25: Analysis of algorithms and problem complexity

03B35: Mechanization of proofs and logical operations

68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

03C10: Quantifier elimination, model completeness, and related topics

Related Items

Complexity and expressive power of second‐order extended Horn logic, Disjunctive closures for knowledge compilation, Complexity of validity for propositional dependence logics, Transformations into Normal Forms for Quantified Circuits, 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