On July 13th and 14th 2018, the 2018 World Championship for Automated Theorem Proving (CASC-J9) took place in Oxford at the 2018 Federated Logic Conference (FLoC18). This was the 23rd issue of the competition, running annually since 1996. More than twenty systems by teams from USA, Asia and Europe competed in six divisions.
Two divisions of the competition were won by systems developed by the CIIRC/CTU team of AI4REASON ERC project of Dr. Josef Urban and their collaborators. The LTB (large theory) division was won by the „Machine Learner for Automated Reasoning“ (MaLARea 0.6) system developed by J. Urban and his colleagues, solving 16% more of the 5000 competition problems than the runner up. The THF (higher-order) division was won by the Satallax 3.3 system developed by Dr. Chad Brown and his colleagues, solving 14% more of the 500 competition problems than the runner up.
The LTB division contains problems arising in large projects in verification of mathematics and software. This year the problems came from the CakeML project that produces a verified implementation of the ML programming language. The THF division contains a selection of problems formulated in higher-order logic. This is one of the most common formalism used for verification of large mathematical proofs and complicated software designs.
[…] and other methods combining learning, theorem proving and automated formalisation. Our systems have won a number of competitions in automated reasoning and the methods developed by us today assist formal […]
Comments are closed.