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

Yoshihiro Mizoguchi
Institute of Mathematics for Industry, Kyushu University

Institute of Mathematics for Industry

Faculty of Mathematics

添付ファイル: fileMy_Nats.thy 140件 [詳細] fileMy_Monoid.thy 142件 [詳細] fileMy_Lists.thy 129件 [詳細]

トップ   編集 凍結 差分 バックアップ 添付 複製 名前変更 リロード   新規 一覧 単語検索 最終更新   ヘルプ   最終更新のRSS
Last-modified: 2013-10-29 (火) 16:07:11 (1449d)