Projects per year
Abstract
Some logics make it easier to say what we want than others and some methods of deduction are simpler to work with than others. One thing typically remains important: that we can deduce all valid things (completeness). In this thesis I tackle completeness of various deduction methods for various logics. The work is formalized in the proof assistant Isabelle/HOL which offers a common language for mathematics and computer science where proofs can be checked mechanically. This thesis discusses the following contributions of my PhD project in particular:
• A historical overview of formalized completeness proofs and a formalization that explains the essence of synthetic completeness proofs.
• A formalization of a concise completeness proof for firstorder logic in Isabelle/HOL, including solutions to the issues of formalizing quantifiers and proving completeness for formulas with free variables.
• A verified prover for firstorder logic with functions, with a formalized completeness proof that takes the search strategy of the prover into account.
• A synthetic completeness proof for a tableau system for basic hybrid logic which is both terminating and in the Seligman style where the proof rules reflect the local perspective that modal logic is based on.
• Formalized soundness and completeness results for epistemic and public announcement logic, instantiated to a range of concrete axiom systems.
• A bestfirst proof search tactic for the proof assistant Lean 4.
• An abstract framework for synthetic completeness proofs.
• A historical overview of formalized completeness proofs and a formalization that explains the essence of synthetic completeness proofs.
• A formalization of a concise completeness proof for firstorder logic in Isabelle/HOL, including solutions to the issues of formalizing quantifiers and proving completeness for formulas with free variables.
• A verified prover for firstorder logic with functions, with a formalized completeness proof that takes the search strategy of the prover into account.
• A synthetic completeness proof for a tableau system for basic hybrid logic which is both terminating and in the Seligman style where the proof rules reflect the local perspective that modal logic is based on.
• Formalized soundness and completeness results for epistemic and public announcement logic, instantiated to a range of concrete axiom systems.
• A bestfirst proof search tactic for the proof assistant Lean 4.
• An abstract framework for synthetic completeness proofs.
Original language  English 

Publisher  Technical University of Denmark 

Number of pages  175 
Publication status  Published  2023 
Keywords
 Propositional logic
 Henkinstyle completeness
 Isabelle/HOL
Fingerprint
Dive into the research topics of 'Formally Correct Deduction Methods for Computational Logic'. Together they form a unique fingerprint.Projects
 1 Finished

Formally Correct Deduction Methods for Computational Logic
From, A. H., Paulson, L. C., Villadsen, J., Gierasimczuk, N. & Braüner, T.
01/02/2020 → 14/06/2023
Project: PhD