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

Jasmin Christian Blanchette

doi:10.1145/3293880.3294087

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 proceeding › Conference contribution › Academic › peer-review

15 Downloads (Pure)

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 language	English
Title of host publication	CPP 2019
Subtitle of host publication	Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs
Editors	Assia Mahboubi
Publisher	Association for Computing Machinery, Inc
Pages	1-13
Number of pages	13
ISBN (Electronic)	9781450362221
DOIs	https://doi.org/10.1145/3293880.3294087
Publication status	Published - Jan 2019
Event	8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019 - Cascais, Portugal Duration: 14 Jan 2019 → 15 Jan 2019

Conference

Conference	8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019
Country/Territory	Portugal
City	Cascais
Period	14/01/19 → 15/01/19

Keywords

proof assistants
proof systems
theorem provers

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1145/3293880.3294087

Formalizing the metatheory of logical calculi and automatic provers in Isabelle or HOLFinal published version, 792 KBLicence: Article 25fa Dutch Copyright Act

Handle.net

Persistent link

Cite this

@inproceedings{c07c32c3ba6a4e1ba7403b9ee65f5d6c,

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

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.",

keywords = "proof assistants, proof systems, theorem provers",

author = "Blanchette, {Jasmin Christian}",

year = "2019",

month = jan,

doi = "10.1145/3293880.3294087",

language = "English",

pages = "1--13",

editor = "Assia Mahboubi",

booktitle = "CPP 2019",

publisher = "Association for Computing Machinery, Inc",

note = "8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019 ; Conference date: 14-01-2019 Through 15-01-2019",

}

Blanchette, JC 2019, Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). in A Mahboubi (ed.), CPP 2019 : Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery, Inc, pp. 1-13, 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, 14/01/19. https://doi.org/10.1145/3293880.3294087

Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). / Blanchette, Jasmin Christian.
CPP 2019 : Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. ed. / Assia Mahboubi. Association for Computing Machinery, Inc, 2019. p. 1-13.

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - Blanchette, Jasmin Christian

PY - 2019/1

Y1 - 2019/1

N2 - 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.

AB - 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.

KW - proof assistants

KW - proof systems

KW - theorem provers

UR - http://www.scopus.com/inward/record.url?scp=85061191555&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85061191555&partnerID=8YFLogxK

U2 - 10.1145/3293880.3294087

DO - 10.1145/3293880.3294087

M3 - Conference contribution

AN - SCOPUS:85061191555

SP - 1

EP - 13

BT - CPP 2019

A2 - Mahboubi, Assia

PB - Association for Computing Machinery, Inc

T2 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019

Y2 - 14 January 2019 through 15 January 2019

ER -

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

Abstract

Conference

Keywords

UN SDGs

Access to Document

Handle.net

Other files and links

Cite this