Resolution for Higher-Order Constrained Horn Clauses submitted

In this work we continue the investigation into the algorithmic and model theoretic properties of higher-order constrained Horn clauses, a fragment of higher-order logic with background theories proposed in [Cathcart Burn et al., 2018] for the verification of higher-order functional programs. As an important stepping stone, we consider theories with a single (standard) model, such as linear arithmetic, although we demonstrate that our approach is more versatile and can also deal with some theories with an infinite number of models. Notwithstanding the fact that full higher-order logic with respect to standard semantics is not recursively enumerable, we present a simple resolution proof system for higher-order constrained Horn clauses and prove its soundness and (refutational) completeness with respect to both standard and Henkin semantics. As a corollary, we obtain an alternative proof of the equivalence of standard, continuous and monotone semantics for higher-order constrained Horn clauses. For the completeness proof we establish novel model theoretic properties which are refinements of known negative results: (i) The structure obtained by iterating the immediate consequence operator is a least model for a carefully chosen relation and (ii) the immediate consequence operator is “quasi-continuous”. Finally, we prove that the well-known translation from higher-order to first-order logic is not only sound and complete for Henkin semantics but also for standard semantics. This gives rise to another semi-decision procedure provided that the background theory is decidable.