First prize for automatic theorem prover developed by VU

A team of computer scientists from the theoretical computer science section at Vrije Universiteit Amsterdam won the annual theorem proving system competition, with a prototype system called Zipperposition.

07/16/2020 | 2:01 PM

Automatic theorem provers are software programs that automatically establish the truth of a logical formula. For example, given a formula such as "under the hypothesis that a = b and b = c, we have that f(a, b) = f(c, c)", these tools would quickly return "yes", indicating that the formula is a theorem.

They can also output detailed proofs to justify their answers and can handle much larger formulas, containing hundreds, sometimes thousands, of hypotheses. These software tools are used as backends to program verifiers and proof assistants, also called interactive theorem provers.

Impressive outcome
The prover developed by the VU team, Zipperposition, finished 21 percentage points ahead of the second place and 35 percentage points ahead of last year's winner. Colleagues have expressed that they were deeply impressed by this prototype prover. CASC has been held for 24 years. It is an informal affair, organized by a well-known researcher. Winners get cheap trophies. Winning at CASC is a good way to raise one's profile in the automatic theorem proving community.

Zipperposition is developed by Petar Vukmirović, in collaboration with Alexander Bentkamp, Visa Nummelin, and Jasmin Blanchette. They got help from colleagues based in Germany and the US. The work is funded by Blanchette's ERC grant Matryoshka and his NWO Vidi grant Lean Forward.

Higher-order provers
Since 2017, the theoretical computer science section, led by professor Wan Fokkink, investigates the theory and practice of a special kind of provers, called higher-order provers. These support a more expressive logic than traditional first-order provers and can be used to express formulas that arise when developing computer-checked proofs of mathematics and software. A typical example of a higher-order formula is Cantor's theorem: "For any set A, the set of all subsets of A has a strictly greater cardinality than A itself." The challenge with higher-order formulas is that the search space for a proof is gigantic. Good theory and heuristics are necessary to avoid duplicated work and to explore promising alleys first.