We should be able to automate what the human mind can express. Our idea is to take charge of the bureaucratic details of a proof so that the developer needs only concentrate on the creative and interesting part of that proof.
This is the motto of Hans-Jörg Schurr, a young Austrian who currently prepares his PhD thesis in the joint VeriDis project team of Inria, LORIA, and the Max-Planck Institute for Computer Science. He received the award for the best paper of a junior researcher at the conference FroCos (Frontiers of Combining Systems). This international meeting, organized online between September 8 and 10, 2021, by the University of Birmingham, gathered computer scientists interested in the development of techniques and methods for the combination and the integration of formal system, their modularity, and their analysis.
Among the 16 scientific papers accepted by the FroCos program committee, the one jointly authored by Hans-Jörg Schurr and his PhD advisor Pascal Fontaine stood out from the rest. Entitled Quantifier Simplification by Unification in SMT, the paper addresses a key topic in computer science, namely the automation of formal logic (i.e., the principles of mathematical reasoning) by computer programs. Among the fundamental interests of this topic ranks software for the detection and reporting of errors, a crucial challenge for computer security, among other domains.
The mathematical intelligence of computers increases.
The method of the two researchers, which has been integrated in their open-source software tool veriT, combines elements of two automatic reasoning methods that coexisted so far: SMT (satisfiability modulo theories) and superposition reasoning. “This is a first crack in the wall between two modes of automated reasoning: the mathematical intelligence of computers increases a little”, jokes Hans-Jörg, who recognizes well the innovative potential of his research.
In order to arrive at their results, the two authors adopted an original approach: rather than concentrating on theoretical impossibilities of connecting two universes of formal logic, they focused their efforts on several concrete problems in order to investigate whether a common pattern existed. Their intuition was rewarded: they found a recurring model, “a recipe that is easy to exploit in order to simplify complex formulas and solve a majority of problems”. Based on its implementation in veriT, their solution has already been adopted by the proof assistant Isabelle, and the two scientists believe that “the best is still to come”. Their objective is to see their method being widely adopted, leading to an increased access to automated reasoning within verification platforms and proof assistants.
