Quantifier Rewriting and Equivalence Models for Quantified Horn Formulas

摘要

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, ∣any∣ universal quantifiers and an arbitrary number of existential quantifiers can be transformed into an equivalent formula of length O(∣any∣ · ∣Φ∣) 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 (exiszHORN~*). An application described in the paper is to solve QHORN~*-SAT in O(∣any∣ · ∣Φ∣ by using this transformation in combination with a linear-time satisfiability checker for propositional Horn formulas.