Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk)

被引：25

作者：

Blanchette, Jasmin Christian ^{[1
]}

机构：

[1] Vrije Univ Amsterdam, Dept Comp Sci, Theoret Comp Sci, Amsterdam, Netherlands

来源：

PROCEEDINGS OF THE 8TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP' 19) | 2019年

基金：

欧洲研究理事会;

关键词：

proof systems; theorem provers; proof assistants; SAT MODULO THEORIES; VERIFICATION; TERMINATION; PROOFS; INCOMPLETENESS; GENERATION; FRAMEWORK; SOLVERS;

D O I：

10.1145/3293880.3294087

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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 lambda-free higher-order logic.

引用

页码：1 / 13

页数：13

共 105 条

[11]

Berghofer S., 2007, Archive of Formal Proofs

[12] Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic [J].

Biendarra, Julian ;

Blanchette, Jasmin Christian ;

Bouzy, Aymeric ;

Desharnais, Martin ;

Fleury, Mathias ;

Holzl, Johannes ;

Kuncar, Ondrej ;

Lochbihler, Andreas ;

Meier, Fabian ;

Panny, Lorenz ;

Popescu, Andrei ;

Sternagel, Christian ;

Thiemann, Rene ;

Traytel, Dmitriy .

FRONTIERS OF COMBINING SYSTEMS (FROCOS 2017), 2017, 10483 :3-21

[13]

Biere A., 2017, P SAT COMP, P14

[14] A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality [J].

Blanchette, Jasmin Christian ;

Fleury, Mathias ;

Lammich, Peter ;

Weidenbach, Christoph .

JOURNAL OF AUTOMATED REASONING, 2018, 61 (1-4) :333-365

[15] A Lambda-Free Higher-Order Recursive Path Order [J].

Blanchette, Jasmin Christian ;

Waldmann, Uwe ;

Wand, Daniel .

FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2017), 2017, 10203 :461-479

[16] Soundness and Completeness Proofs by Coinductive Methods [J].

Blanchette, Jasmin Christian ;

Popescu, Andrei ;

Traytel, Dmitriy .

JOURNAL OF AUTOMATED REASONING, 2017, 58 (01) :149-179

[17] A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality [J].

Blanchette, Jasmin Christian ;

Fleury, Mathias ;

Weidenbach, Christoph .

AUTOMATED REASONING (IJCAR 2016), 2016, 9706 :25-44

[18]

Blanchette JC, 2013, LECT NOTES COMPUT SC, V8152, P245, DOI 10.1007/978-3-642-40885-4_17

[19]

Blanchette JC, 2010, LECT NOTES COMPUT SC, V6172, P131, DOI 10.1007/978-3-642-14052-5_11

[20]

Blanchette Jasmin Christian, 2013, ARCH FORMAL PROOFS

← 1 2 3 4 5 6 7 8 9 10 →