Details

Autor(en) / Beteiligte

• Bubeck, Uwe
• Büning, Hans Kleine
• Zhao, Xishun

Titel

Quantifier Rewriting and Equivalence Models for Quantified Horn Formulas

Ist Teil von

• Lecture notes in computer science, 2005, p.386-392

Ort / Verlag

Berlin, Heidelberg: Springer Berlin Heidelberg

Erscheinungsjahr

2005

Link zum Volltext

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• In this paper, quantified Horn formulas with free variables (QHORN*) are investigated. The main result is that any quantified Horn formula Φ of length |Φ| with free variables, |∀| universal quantifiers and an arbitrary number of existential quantifiers can be transformed into an equivalent formula of length O(| ∀ | ·|Φ|) which contains only existential quantifiers. Moreover, it is shown that quantified Horn formulas with free variables have equivalence models where every existential quantifier is associated with a monotone Boolean function. The results allow a simple representation of quantified Horn formulas as purely existentially quantified Horn formulas (∃ HORN*). An application described in the paper is to solve QHORN*-SAT in O(| ∀ | ·|Φ|) by using this transformation in combination with a linear-time satisfiability checker for propositional Horn formulas.