We are increasingly letting computers reason for us: Self-driving cars predict the future state of traffic based on their current surroundings, IBM’s Watson deduces possible diagnoses of illnesses based on medical data, and Amazon employs automated reasoning to verify security properties in the cloud like ensuring that confidential data is not publicly accessible. The growing expectations of the computers around us call for more sophisticated methods of reasoning and means that it becomes even more important to ensure their correctness.
Reasoning about this reasoning has, however, remained a human activity, with all the possibilities for error that entails. These possibilities reduce the trust we can put in decisions made by these machines and possibly raise issues of safety and security. Our motivation is to advance the state and understanding of reasoning systems by developing new deduction methods for computational logic and applying state-of-the-art proof assistants like Isabelle or Coq to prove them formally correct. This formal verification is not standard practice and means that the computer checks every claim we make.
The application of a proof assistant will not only allow us to fully trust the considered logics but will produce fully-spelled out, non-ambiguous formalizations to learn from, in a format that makes them easy for others to build on or modify for new purposes. Meanwhile, it may be necessary to develop new proof-assisting techniques, contributing to automatic or interactive theorem proving itself and making similar work easier for others. The Isabelle proof assistant allows the export of verified algorithms into programming languages like Haskell, OCaml and Scala, enabling us to produce concrete, executable software.
Picture: Official Isabelle logo