Constraint superposition for higher-order logic

Abstract

Prädikatenlogik erster Stufe galt lange als optimale Grundlage für automatisierte Theorembeweiser in Bezug auf die Ausdrucksstärke im Verhältnis zum Automatisierungsgrad. Führende Theorembeweiser verwenden den Superpositionskalkül, welcher kürzlich auf Prädikatenlogik höherer Stufe, auch als einfache Typentheorie bezeichnet, erweitert wurde. Diese Erweiterung erlaubt es großteils, dass Beweisführung höherer Stufe auch nur für Probleme höherer Stufe verwendet wird. Die empirische Evaluierung dieses Kalküls durch den Theorembeweiser Zipperposition hat die Konkurrenzfähigkeit gegenüber anderen aktuellen Theorembeweisern für Logik höherer Stufe unter Beweis gestellt. Obwohl der Superpositionskalkül für Logik höherer Stufe vielversprechend ist, gibt es Möglichkeiten zur Verbesserung. Durch den Sprung von Prädikatenlogik erster Stufe zu höheren Stufen wird das Unifikationsproblem unentscheidbar. Weil möglicherweise unendlich viele Unifizierer enumeriert werden müssen, kann eine Explosion des Suchraums erfolgen. G.P. Huet stellte fest, dass eine vollständige Unifikation für Kalküle höherer Ordnung nicht notwendig ist, während gleichzeitig die Eigenschaft der Widerlegungsvollständigkeit erhalten werden kann. Er führte einen Resolutionskalkül für die einfache Typentheorie ein, bei dem Constraints verwendet werden, um die Unifikation aufzuschieben. Die Unifikationsprobleme können dann mit einem Ansatz namens Preunifizierung gelöst werden, bei dem die Unifikation gestoppt werden kann, wenn es offensichtlich ist, dass eine Lösung existiert. In dieser Arbeit wird die Idee von Huet auf den Superpositionskalkül angewandt, was den Namen \emph{Constraint-Superpositionskalkül} ergibt. Dadurch ist es möglich, die Unifikation hinauszuzögern und die entstehenden Unifikationsconstraints erst später zu lösen. Außerdem müssen bei diesem Ansatz einige Unifizierer während des Saturationsprozesses nicht berücksichtigt werden, was zu einer Einschränkung des Suchraums führt. Aufbauend auf früheren Arbeiten präsentieren wir eine Beweisskizze für Widerlegungsvollständigkeit. Schließlich wird der in Zipperposition implementierte Ansatz erläutert und basierend auf TPTP und Sledgehammer Benchmarks evaluiert.

For many years, first-order logic was considered the sweet spot for automated theorem provers regarding expressiveness in relation to the degree of automation. The leading theorem provers employ the superposition calculus. Recently, this calculus was successfully extended to higher-order logic, which is also called simple type theory. The extension is mostly graceful, in a sense that higher-order reasoning should exclusively be used for higher-order problems. Its empirical evaluation in the theorem prover Zipperposition proved the extension to be competitive with other current theorem provers for higher-order logic. While the superposition calculus for higher-order logic is promising, there are possibilities for improvement. When going from first-order to higher-order logic, the unification problem becomes undecidable. Since the calculus needs to eagerly enumerate unifiers, a potential explosion in search space is possible. It was noted by G.P. Huet that full eager unification is not necessary for higher-order calculi, while still enjoying the property of refutational completeness. He introduced a resolution calculus for simple type theory, where constraints are used to postpone unification. The unification problems can then be solved using an approach called preunification, where the unification can be stopped when it is apparent that the problem admits a solution. In this thesis, the idea of Huet is applied to the superposition calculus, which gives the name constraint superposition calculus. This makes it possible to postpone unification and lazily solve the arising unification constraints. Moreover, with this approach some unifiers need not be considered during saturation, which leads to a restriction of the search space. Building upon previous work, we present a proof sketch for refutational completeness. Finally, the implementation in Zipperposition is discussed and evaluated on TPTP and Sledgehammer benchmarks.