Superposition for Higher-Order Logic

This thesis presents an extension of the superposition calculus to higher-order logic (also called simple type theory) and its implementation and empirical evaluation in an automated theorem prover. The standard first-order superposition calculus is extended step by step to richer logics in three major milestones, culminating with full higher-order logic.

The first milestone takes the form of four calculi for lambda-free higher-order logic. They closely resemble Bachmair and Ganzinger’s first-order superposition calculus, but support partial applications and applied variables. Crucially, they also support nonmonotone term orders, an essential feature in preparation for higher-order logic.

The second milestone extends one of these calculi further to a clausal fragment of higher-order logic that includes anonymous functions but excludes Booleans. It uses higher-order unification and can cope with beta-eta-conversion of lambda-terms.

The third milestone is the calculus for full higher-order logic. It adds support for an interpreted Boolean type with the familiar connectives and quantifiers, as well as a choice operator.

As a secondary contribution, the thesis introduces the embedding path order, a term order for lambda-free higher order terms that resembles the first-order recursive path order. It is a ground-total simplification order; in particular it is monotone and thus avoids the complications dealt with in our first milestone, at the cost of being less efficiently computable.

Each milestone has been implemented in the Zipperposition prover and evaluated on TPTP and Sledgehammer benchmarks. Based on this implementation, Zipperposition outperformed all other provers in the higher-order category of the 2020 edition of the CASC prover competition.