×

Interactive theorem proving from the perspective of Isabelle/Isar. (English) Zbl 1431.68125

Woltzenlogel Paleo, Bruno (ed.) et al., All about proofs, proofs for all. London: College Publications. Stud. Log. (Lond.) 55, 91-115 (2015).
Summary: Interactive theorem proving (ITP) has a long tradition, going back to the 1970s when interaction was introduced as a concept in computing. The main provers in use today can be traced back over 20–30 years of development. As common traits there are usually strong logical systems at the bottom, with many layers of add-on tools around the logical core, and big applications of formalized mathematics or formal methods. There is a general attitude towards flexibility and open-endedness in the combination of logical tools: typical interactive provers use automated provers and disprovers routinely in their portfolio.
The subsequent exposition of ITP takes Isabelle/Isar as the focal point to explain concepts of the greater “LCF family”, which includes Coq and various HOL systems. Isabelle itself shares much of the relatively simple logical foundations of HOL, but follows Coq in the ambition to deliver a sophisticated system to end-users, without requiring self-assembly of individual parts. Isabelle today is probably the most advanced proof assistant concerning its architecture and extra-logical infrastructure.
The Isar aspect of Isabelle refers first to the structured language for human-readable and machine-checkable proof documents, but also to the Isabelle architecture that emerged around the logical framework in the past 10 years. Thus Isabelle/Isar provides extra structural integrity beyond the core logical framework, with native support for parallel proof processing and asynchronous interaction in its prover IDE (PIDE).
For the entire collection see [Zbl 1334.03007].

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B35 Mechanization of proofs and logical operations
PDFBibTeX XMLCite