DHBW theorem prover scores at World Championship for automated reasoning systems

In computer science, so-called theorem provers can be applied to logical puzzles like the aforementioned, but also for proving mathematical theorems, answering common-sense questions, demonstrating biological relationships, or showing properties like zero-defect software. The idea is to start with a real world problem, formalize it, and then let the computer find a proof, or a countermodel.

Poster of the world championship
Each year, the world’s best scientists in the field of automated reasoning meet at the CADE ATP System Competition (CASC). It is associated with the Conference on Automated Deduction and regarded as the "World Championship" for automated reasoning systems. This year, it was held at the Federated Logic Conference, an event that co-located many conferences concerned with logic, formal methods, and automated reasoning, at the Technion in Haifa, Israel.

The 2022 edition of CASC saw 18 competitors working on problems from 7 different so-called “divisions". In each division, systems try to solve as many logical problems as possible within a given time limit, usually by proving a conjecture from a given set of axioms. One of the Divisions, FNT, instead challenges systems  to demonstrate that the conjecture is false (e.g. by providing a counterexample, or, in more technical language, a counter-model). 

The theorem prover E, primarily developed by DHBW Professor and ZfKI member Stephan Schulz, competed in six divisions. It achieved a first place in the SLH division (proving "real user problems" within a 30s time limit) and came in second in three more divisions: proving theorems in higher-order logic, proving theorems in first-order logic (often considered the premiere category with the most mature theorem provers), and proving purely equational problems. In the LTB division (proving a large number of problems from one application domain), it came in third. This continues the successes of the last 3 years, where E (or it’s higher-order variant) also won first places and good placements in various divisions.