Soundness and Completeness Proofs by Coinductive Methods

Abstract : We show how codatatypes can be employed to produce compact, high-level proofs of key results in logic: the soundness and completeness of proof systems for variations of first-order logic. For the classical completeness result, we first establish an abstract property of possibly infinite derivation trees. The abstract proof can be instantiated for a wide range of Gentzen and tableau systems for various flavors of first-order logic. Soundness becomes interesting as soon as one allows infinite proofs of first-order formulas. This forms the subject of several cyclic proof systems for first-order logic augmented with inductive predicate definitions studied in the literature. All the discussed results are formalized using Isa-belle/HOL's recently introduced support for codatatypes and corecursion. The development illustrates some unique features of Isabelle/HOL's new coinductive specification language such as nesting through non-free types and mixed recursion–corecursion.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2017, 58 (1), pp.149 - 179. 〈10.1007/s10817-016-9391-3〉
Liste complète des métadonnées

Littérature citée [48 références]  Voir  Masquer  Télécharger
Contributeur : Jasmin Christian Blanchette <>
Soumis le : mardi 21 novembre 2017 - 10:38:11
Dernière modification le : mardi 18 décembre 2018 - 16:38:25


Fichiers produits par l'(les) auteur(s)



Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel. Soundness and Completeness Proofs by Coinductive Methods. Journal of Automated Reasoning, Springer Verlag, 2017, 58 (1), pp.149 - 179. 〈10.1007/s10817-016-9391-3〉. 〈hal-01643157〉



Consultations de la notice


Téléchargements de fichiers