"Some Lessons Learned on Writing Predicate Logic Proofs in Isabelle/Isar"
, Serie Research Institute for Symbolic Computation (RISC), Johannes Kepler, RISC, JKU, Hagenberg, Linz, 10-2014
Some Lessons Learned on Writing Predicate Logic Proofs in Isabelle/Isar
Sprache des Titels:
We describe our experience with the use of the proving assistant Isabelle and its proof development language Isar for formulating and proving formal mathematical statements. Our focus is on how to use classical predicate logic and well established proof principles for this purpose, bypassing Isabelle's meta-logic and related technical aspects as much as possible. By a small experiment on the proof of (part of a) verification condition for a program, we were able to identify a number of important patterns that arise in such proofs yielding to a workflow with which we feel personally comfortable; the resulting guidelines may serve as a starting point for a the application of Isabelle/Isar for the "average" mathematical user (i.e, a mathematical user who is not interested in Isabelle/Isar per se but just wants to use it as a tool for computer-supported formal theory development).
Sprache der Kurzfassung:
Research Institute for Symbolic Computation (RISC), Johannes Kepler