Abstract: |
A formalized coinductive account of the abstract development of
Brotherston, Gorogiannis, and Petersen [APLAS 2012], in a slightly
more general form since we work with arbitrary infinite proofs, which
may be acyclic. This work is described in detail in an article by the
authors, published in 2017 in the Journal of Automated
Reasoning. The abstract proof can be instantiated for
various formalisms, including first-order logic with inductive
predicates. |
BibTeX: |
@article{Abstract_Soundness-AFP,
author = {Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel},
title = {Abstract Soundness},
journal = {Archive of Formal Proofs},
month = feb,
year = 2017,
note = {\url{http://isa-afp.org/entries/Abstract_Soundness.html},
Formal proof development},
ISSN = {2150-914x},
}
|