Models and quantifier elimination for quantified Horn formulas

DOI10.1016/J.DAM.2007.10.005MaRDI QIDQ944709zbMATH OpenOpenAlexFDO

Authors Uwe Bubeck, Hans Kleine Büning

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

modelsatisfiabilityquantified Boolean formulaquantifier eliminationquantified Horn formula

Mathematics Subject Classification ID

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

Recommendations

• Theory and Applications of Satisfiability Testing
• Dependency Quantified Horn Formulas: Models and Complexity
• Logic versus Approximation
• scientific article; zbMATH DE number 4085614
• Resolution for quantified Boolean formulas

Cites work

• scientific article; zbMATH DE number 4012495 (Why is no real title available?)
• scientific article; zbMATH DE number 1470716 (Why is no real title available?)
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Bounded Universal Expansion for Preprocessing QBF
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• On sentences which are true of direct unions of algebras
• Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae
• Resolution for quantified Boolean formulas
• 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

Cited in

(17)

• Elimination of quantifiers in Horn theories having a small number of models
• Characterization results for d-Horn formulas, or on formulas that are true on dual reduced products
• Theory and Applications of Satisfiability Testing
• Logic versus Approximation
• scientific article; zbMATH DE number 1330425 (Why is no real title available?)
• Theory and Applications of Satisfiability Testing
• Resolution for quantified Boolean formulas
• Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits
• Rewriting (dependency-)quantified 2-CNF with arbitrary free literals into existential 2-HORN
• Transformations into normal forms for quantified circuits
• Introducing \(w\)-Horn and \(Z\)-Horn: a generalization of Horn and \(q\)-Horn formulae
• Dependency Quantified Horn Formulas: Models and Complexity
• Complexity of validity for propositional dependence logics
• Complexity and expressive power of second-order extended Horn logic
• Disjunctive closures for knowledge compilation
• Quantifier elimination and other model-theoretic properties of BL-algebras
• scientific article; zbMATH DE number 4085614 (Why is no real title available?)

Describes a project that uses

Uses Software

• Quantor

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q944709)