Abstract Soundness (Q7361541)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Abstract_Soundness
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Abstract Soundness |
AFP entry Abstract_Soundness |
Statements
10 February 2017
0 references
Jasmin Christian Blanchette
0 references
Andrei Popescu
0 references
Dmitriy Traytel
0 references
Abstract Soundness (English)
0 references
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.
0 references
