@techreport{RISC5073,author = {Wolfgang Schreiner},
title = {{Some Lessons Learned on Writing Predicate Logic Proofs in Isabelle/Isar}},
language = {english},
abstract = {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).},
year = {2014},
month = {October},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {proof assistants, automated reasoning, formal methods},
length = {32}
}