An Abstract Fixed-point Theorem
              for Horn Formula Equations
                                  (Abstract)

                     Stefan Hetzl and Johannes Kloibhofer

        Institute of Discrete Mathematics and Geometry, TU Wien, Austria
                stefan.hetzl@tuwien.ac.at, j.kloibhofer@gmx.net

We consider the problem of solving a formula equation, i.e., given a formula
∃X ϕ where ϕ is first-order and X is a tuple of predicate variables, to find
a substitution [X\ψ] s.t. ϕ[X\ψ] is a valid first-order formula. This problem is
also known as Boolean solution problem in the literature [9] and is closely related
to second-order quantifier elimination.
    More specifically, we focus on the class of Horn formula equations, which is
defined by restricting ϕ to be a Horn clause set w.r.t. the predicate variables.
We state and prove a fixed-point theorem for Horn formula equations based on
expressing the fixed-point computation of a minimal model (in the sense of logic
programming) of a set of Horn clauses on the object level as a formula in first-
order logic with a least fixed-point operator. This result is shown by an extension
of the fixed-point approach of Nonnengart and Szalas to second-order quantifier
elimination [7]. Our fixed-point theorem applies not only to the usual semantics
of second-order logic and first-order logic with a least fixed-point operator but
also to model abstractions, a semantics for logical formulas that corresponds to
abstract interpretation of programs using Galois connections [2].
    Our fixed-point theorem allows both new results and simpler proofs of exist-
ing results as applications and corollaries.
 1. It entails expressibility of the weakest precondition and the strongest post-
    condition, and thus the partial correctness of an imperative program, in
    first-order logic with a least fixed-point operator.
 2. It allows a generalisation of a result by Ackermann [1] on approximating a
    second-order formula by first-order formulas in a direction different from the
    recent generalisation [8].
 3. It allows to obtain a result from a recently introduced approach to automated
    inductive theorem proving with tree grammars [3] as another straightforward
    corollary.
 4. Since it incorporates abstract interpretation, it permits to considerably sim-
    plify the proof of the decidability of affine formula equations originally pre-
    sented in [5].
   This work is rooted in the second author’s master’s thesis [6]. Some of these
results have been presented at the 8th Workshop on Horn Clauses for Verification
and Synthesis [4].
  Copyright © 2021 for this paper by its authors. Use permitted under Creative
  Commons License Attribution 4.0 International (CC BY 4.0).
60      Stefan Hetzl and Johannes Kloibhofer

References
1. Ackermann, W.: Untersuchungen über das Eliminationsproblem der math-
   ematischen Logik. Mathematische Annalen 110(1), 390–413 (1935).
   https://doi.org/10.1007/BF01448035
2. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model
   for static analysis of programs by construction or approximation of fix-
   points. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) 4th ACM Sym-
   posium on Principles of Programming Languages. pp. 238–252. ACM (1977).
   https://doi.org/10.1145/512950.512973
3. Eberhard, S., Hetzl, S.: Inductive theorem proving based on tree gram-
   mars. Annals of Pure and Applied Logic 166(6), 665–700 (2015).
   https://doi.org/10.1016/j.apal.2015.01.002
4. Hetzl, S., Kloibhofer, J.: A fixed point theorem for Horn for-
   mula equations. In: Kafle, B., Hojjat, H. (eds.) 8th Workshop on
   Horn Clauses for Verification and Synthesis (2021), available at
   https://www.sci.unich.it/hcvs21/papers/HCVS 2021 paper 1.pdf
5. Hetzl, S., Zivota, S.: Decidability of affine solution problems. Journal of Logic and
   Computation 30(3), 697–714 (2020). https://doi.org/10.1093/logcom/exz033
6. Kloibhofer, J.: A fixed-point theorem for Horn formula equations. Master’s thesis,
   TU Wien, Austria (2020)
7. Nonnengart, A., Szalas, A.: A Fixpoint Approach to Second-Order Quantifier Elim-
   ination with Applications to Correspondence Theory. In: Orlowska, E. (ed.) Logic
   at Work: Essays Dedicated to the Memory of Helena Rasiowa, Studies in Fuzziness
   and Soft Computing, vol. 24, pp. 307–328. Springer (1998)
8. Wernhard, C.: Approximating resultants of existential second-order quantifier elim-
   ination upon universal relational first-order formulas. In: Koopmann, P., Rudolph,
   S., Schmidt, R.A., Wernhard, C. (eds.) Workshop on Second-Order Quantifier Elim-
   ination and Related Topics (SOQE 2017). CEUR Workshop Proceedings, vol. 2013,
   pp. 82–98 (2017)
9. Wernhard, C.: The Boolean Solution Problem from the Perspective of Predicate
   Logic. In: Dixon, C., Finger, M. (eds.) 11th International Symposium on Frontiers
   of Combining Systems (FroCoS). Lecture Notes in Computer Science, vol. 10483,
   pp. 333–350. Springer (2017). https://doi.org/10.1007/978-3-319-66167-4 19