Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)

Jasmin Christian Blanchette*

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

IsaFoL (Isabelle Formalization of Logic) is an undertaking that aims at developing formal theories about logics, proof systems, and automatic provers, using Isabelle/HOL. At the heart of the project is the conviction that proof assistants have become mature enough to actually help researchers in automated reasoning when they develop new calculi and tools. In this paper, I describe and reflect on three verification subprojects to which I contributed: A first-order resolution prover, an imperative SAT solver, and generalized term orders for-free higher-order logic.

Original languageEnglish
Title of host publicationCPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019
EditorsAssia Mahboubi
PublisherAssociation for Computing Machinery, Inc
Pages1-13
Number of pages13
ISBN (Electronic)9781450362221
DOIs
Publication statusPublished - 14 Jan 2019
Event8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019 - Cascais, Portugal
Duration: 14 Jan 201915 Jan 2019

Conference

Conference8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019
CountryPortugal
CityCascais
Period14/01/1915/01/19

Keywords

  • proof assistants
  • proof systems
  • theorem provers

Cite this