-
Master internship offer: Integration of abduction in the proof assistant Isabelle/HOL
When something goes wrong, we want to know why. When a plane or a rocket crashes, we spare no effort in the investigation of the cause, to prevent further accidents. We are, however, poorly equipped for similar in-depth investigations involving logic-based objects such as mathematical proofs despite their increasing importance in everyday life (e.g., in the cryptography behind online banking systems).
Indeed, abduction, the logical equivalent of seeking explanations, is underdeveloped in expressive logics that can represent such abstractions. Although abduction has a few success stories, there are currently no techniques generic enough to lead to a wide adoption of abduction in practice in expressive logics. This in turn direly restrains the explanation capabilities of objects expressed in these logics.
We want to tackle this challenge starting with a master internship, first by integrating the cvc5 abduction engine to the proof assistant Isabelle/HOL to better evaluate the weaknesses of this state-of-the-art abduction technique in the context of machine-verified mathematical proofs and then by improving the abduction engine based on the result of the experiments.
