Special Lecture †
Date, Time & Venue †
October 29 (Tue), 2013.
16:00 -- 17:00
(ROOM 122, Faculty of Mathematics, B1F)
Formalising Mathematics with Isabelle/HOL: The First Steps
(Dept. Computer Science, University of Sheffield, U.K.)
Isabelle/HOL is a popular theorem proving environment developed at the Universities of Cambridge and Munich. It allows mathematicians to design theory hierarchies and link axiomatic specifications of theories with concrete models. It also allows users to check proofs by machine, prove simple statements fully automatically and search for counterexamples. Formally, Isabelle/HOL is based on a typed higher-order logic with support for sets and recursive functions. This leads to a particular style of programming mathematical objects. This lecture teaches the first steps of programming and specifying mathematical objects in Isabelle/HOL and of reasoning fformally about these objects. Examples will be drawn, e.g. from monoids, boolean algebras or formal languages. After attending this lecture, students will be able to explore Isabelle independently with the help of its excellent documentation and extensive mathematical libraries.
Contact address †
Institute of Mathematics for Industry, Kyushu University