Soundness and Completeness Proofs by Coinductive Methods |
| |
Authors: | Jasmin Christian Blanchette Andrei Popescu Dmitriy Traytel |
| |
Affiliation: | 1.Inria Nancy and LORIA,Villers-lès-Nancy,France;2.Max-Planck-Institut für Informatik,Saarbrücken,Germany;3.Department of Computer Science, School of Science and Technology,Middlesex University,London,UK;4.Institute of Information Security, Department of Computer Science,ETH Zurich,Zurich,Switzerland;5.Institute of Mathematics Simion Stoilow of the Romanian Academy,Bucharest,Romania |
| |
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 Isabelle/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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|