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 -
