Title: "Formalization of Logic in the Isabelle Proof Assistant"
Monday 22 October, 2018 at 13:00, The Technical University of Denmark, Building 101A, S09, Anker Engelunds Vej 1, 2800 Kgs. Lyngby
Principal supervisor: Associate Professor Jørgen Villadsen, DTU Compute
Co-supervisors: Associate Professor Thomas Bolander, DTU Compute and Assistant
Professor Jasmin Christian Blanchette, Vrije Universiteit Amsterdam, The Netherlands
Examiners:
Associate Professor Sebastian Mödersheim, DTU Compute
Associate Professor Jesper Bengtson, IT-University of Copenhagen
Professor Tobias Nipkow, Technical University of Munich
Chairperson at defence:
Professor Jørgen Fischer Nilsson, DTU Compute
Summary:
Computer programs are central to many of the technological advances of modern day society. Enormous amounts of resources are spent fighting problems caused by defects and bugs in computer programs. A way to solve this problem is to apply tools that prove correctness of hardware and software, and thus avoid defects and bugs in the first place.
To prove something means to argue rigorously that it is true. Proof assistants are computer programs that help their users prove properties. In proof assistants, the proofs have to be written in special proof languages which are in some ways similar to programming languages, and the proof assistant ensures that all the arguments used in the proofs follow logically. The proof assistant can also conduct parts of the proofs automatically. The process of writing proofs in a proof assistant is called formalization.
This thesis utilizes the Isabelle proof assistant to prove that a number of logics and computer programs work correctly, i.e. as intended. For instance, Isabelle is used to prove that a program from the field of automated reasoning (a sub-field of artificial intelligence and logic) can make flawless and sufficient reasoning within a formal language.
Specifically, the thesis presents formalizations of the resolution calculus, the ordered resolution calculus, natural deduction and an axiomatic system ? all for first-order logic. The ordered resolution calculus and the axiomatic system are used to build verified provers, and a tool for teaching logic is based on the formalized natural deduction system. Soundness is formalized for all the mentioned proof systems, and for the resolution calculi and natural deduction systems completeness is also formalized. The meta-theory of a propositional fragment of a paraconsistent infinite-valued higher-order logic is formalized, and theorems about the necessity of having infinitely many truth values are proved and formalized. These innovations can be utilized as resources for developing new research in logic, as companions to the published literature on logic and as tools for teaching logic.
READ MORE at orbit.dtu.dk
A copy of the PhD thesis is available for reading at the department
Everyone is welcome.