BEGIN:VCALENDAR VERSION:2.0 PRODID:-//DTU.dk//NONSGML DTU.dk//EN CALSCALE:GREGORIAN BEGIN:VEVENT DTSTART:20181022T110000Z DTEND:20181021T220000Z SUMMARY:PhD Defence by Anders Schlichtkrull DESCRIPTION:
Title: Formalization of Logic in the Isabelle Proof Assistant
\nMonday 22 October, 2018 at 13:00, The Technical University of Denmark, Building 101A, S09, Anker Engelunds Vej 1, 2800 Kgs. Lyngby\n
\nPrincipal supervisor: Associate Professor Jørgen Villadsen, DTU Compute.
\nCo-supervisor: Associate Professor Thomas Bolander, DTU Compute and Assistant\nProfessor Jasmin Christian Blanchette, Vrije Universiteit Amsterdam, The Netherlands.\n
Examiners:\n
\nAssociate Professor Sebastian Mödersheim, DTU Compute\n
\nAssociate Professor Jesper Bengtson, IT-University of Copenhagen\n
\nProfessor Tobias Nipkow, Technical University of Munich\n
Chairperson at defence:\nProfessor Jørgen Fischer Nilsson, DTU Compute\n
\nSummary:\n
\nComputer 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.\n
\nTo 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.\n
\nThis 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.\n
\nSpecifically, 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.\n
READ MORE in DTU Orbit.\n
\nA copy of the PhD thesis is available for reading at the department\n
\nEveryone is welcome.
X-ALT-DESC;FMTTYPE=text/html:Title: Formalization of Logic in the Isabelle Proof Assistant
\nMonday 22 October, 2018 at 13:00, The Technical University of Denmark, Building 101A, S09, Anker Engelunds Vej 1, 2800 Kgs. Lyngby\n
\nPrincipal supervisor: Associate Professor Jørgen Villadsen, DTU Compute.
\nCo-supervisor: Associate Professor Thomas Bolander, DTU Compute and Assistant\nProfessor Jasmin Christian Blanchette, Vrije Universiteit Amsterdam, The Netherlands.\n
Examiners:\n
\nAssociate Professor Sebastian Mödersheim, DTU Compute\n
\nAssociate Professor Jesper Bengtson, IT-University of Copenhagen\n
\nProfessor Tobias Nipkow, Technical University of Munich\n
Chairperson at defence:\nProfessor Jørgen Fischer Nilsson, DTU Compute\n
\nSummary:\n
\nComputer 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.\n
\nTo 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.\n
\nThis 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.\n
\nSpecifically, 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.\n
READ MORE in DTU Orbit.\n
\nA copy of the PhD thesis is available for reading at the department\n
\nEveryone is welcome.
URL:https://www.compute.dtu.dk/english/kalender/2018/10/phd-defence-by-anders-schlichtkrull-lyngby DTSTAMP:20240319T113000Z UID:{68622FD9-FB7C-4615-80F2-77670C391CA7}-20181022T110000Z-20181022T110000Z LOCATION: DTU, Building 101A, S09 END:VEVENT END:VCALENDAR