Projects per year
Abstract
Isabelle is a proof assistant, i.e. a computer program that helps its user to deﬁne concepts in mathematics and computer science as well as to prove properties about them. This process is called formalization. Proof assistants aid their users by ensuring that proofs are constructed correctly and by conducting parts of the proofs automatically. A logical calculus is a set of rules and axioms that can be applied to construct theorems of the calculus. Logical calculi are employed in e.g. tools for formal veriﬁcation of computer programs. Two important properties of logical calculi are soundness and completeness, since they state, respectively, that all theorems of a given calculus are valid, and that all valid statements are theorems of the calculus. Validity is deﬁned by a semantics, which gives meaning to formulas. This thesis describes formalizations in Isabelle of several logics as well as tools built upon these. Speciﬁcally this thesis explains and discusses the following contributions of my PhD project:
• A formalization of the resolution calculus for ﬁrstorder logic, Herbrand’s theorem and the soundness and completeness of the calculus.
• A formalization of the ordered resolution calculus for ﬁrstorder logic, an abstract prover based on it and the prover’s soundness and completeness.
• A veriﬁed automatic theorem prover for ﬁrstorder logic. The prover is a reﬁnement of the above formalization of an abstract prover. This explicitly shows that the abstract notion of a prover can describe concrete computer programs. • The Natural Deduction Assistant (NaDeA), which is a tool for teaching ﬁrstorder logic that allows users to build proofs in natural deduction. The tool is based on a formalization of natural deduction and its soundness and completeness.
• A veriﬁed proof assistant for ﬁrstorder logic with equality. It is based on an axiomatic system and constitutes a tool for teaching logic and proof assistants.
• A formalization of the propositional fragment of a paraconsistent inﬁnitevalued higherorder logic. Theorems about the necessity of having inﬁnitely many truth values are proved and formalized. Proof assistants are built to reject proofs that contain gaps or mistakes. Therefore, the formalized results are highly trustworthy. The tools based on formalized calculi consequently have an increased trustworthiness. The above formalizations revealed ﬂaws and mistakes in the literature. In addition to the formalizations and tools themselves, my PhD project contributes solutions that repair these ﬂaws and mistakes.
• A formalization of the resolution calculus for ﬁrstorder logic, Herbrand’s theorem and the soundness and completeness of the calculus.
• A formalization of the ordered resolution calculus for ﬁrstorder logic, an abstract prover based on it and the prover’s soundness and completeness.
• A veriﬁed automatic theorem prover for ﬁrstorder logic. The prover is a reﬁnement of the above formalization of an abstract prover. This explicitly shows that the abstract notion of a prover can describe concrete computer programs. • The Natural Deduction Assistant (NaDeA), which is a tool for teaching ﬁrstorder logic that allows users to build proofs in natural deduction. The tool is based on a formalization of natural deduction and its soundness and completeness.
• A veriﬁed proof assistant for ﬁrstorder logic with equality. It is based on an axiomatic system and constitutes a tool for teaching logic and proof assistants.
• A formalization of the propositional fragment of a paraconsistent inﬁnitevalued higherorder logic. Theorems about the necessity of having inﬁnitely many truth values are proved and formalized. Proof assistants are built to reject proofs that contain gaps or mistakes. Therefore, the formalized results are highly trustworthy. The tools based on formalized calculi consequently have an increased trustworthiness. The above formalizations revealed ﬂaws and mistakes in the literature. In addition to the formalizations and tools themselves, my PhD project contributes solutions that repair these ﬂaws and mistakes.
Original language  English 

Publisher  DTU Compute 

Number of pages  168 
Publication status  Published  2018 
Series  DTU Compute PHD2018 

Volume  493 
ISSN  09093192 
Fingerprint
Dive into the research topics of 'Formalization of Logic in the Isabelle Proof Assistant'. Together they form a unique fingerprint.Projects
 1 Finished

Formalization of Algorithms and Logical inference Systems in Proof Assistants
Schlichtkrull, A., Villadsen, J., Blanchette, J. C., Bolander, T., Mödersheim, S. A., Bengtson, J. & Nipkow, T.
Technical University of Denmark
15/09/2015 → 14/11/2018
Project: PhD