Models and quantifier elimination for quantified Horn formulas
From MaRDI portal
Publication:944709
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
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
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