| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Abstract Completeness
| Title: | Abstract Completeness |
| Authors: | Jasmin Christian Blanchette (j /dot/ c /dot/ blanchette /at/ vu /dot/ nl), Andrei Popescu (a /dot/ popescu /at/ mdx /dot/ ac /dot/ uk) and Dmitriy Traytel |
| Submission date: | 2014-04-16 |
| Abstract: | A formalization of an abstract property of possibly infinite derivation trees (modeled by a codatatype), representing the core of a proof (in Beth/Hintikka style) of the first-order logic completeness theorem, independent of the concrete syntax or inference rules. This work is described in detail in the IJCAR 2014 publication by the authors. The abstract proof can be instantiated for a wide range of Gentzen and tableau systems as well as various flavors of FOL---e.g., with or without predicates, equality, or sorts. Here, we give only a toy example instantiation with classical propositional logic. A more serious instance---many-sorted FOL with equality---is described elsewhere [Blanchette and Popescu, FroCoS 2013]. |
| BibTeX: |
@article{Abstract_Completeness-AFP,
author = {Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel},
title = {Abstract Completeness},
journal = {Archive of Formal Proofs},
month = apr,
year = 2014,
note = {\url{http://isa-afp.org/entries/Abstract_Completeness.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Collections |
| Used by: | Abstract_Soundness, Incredible_Proof_Machine |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |