### 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.

### License

BSD License

### Topics

- Logic/Proof theory

### Session Abstract_Soundness

- Finite_Proof_Soundness
- Infinite_Proof_Soundness

### Depends on

- Abstract Completeness

### Used by

- A Naive Prover for First-Order Logic
- A Sequent Calculus Prover for First-Order Logic with Functions

### Auto-related entries

- A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
- Soundness and Completeness of an Axiomatic System for First-Order Logic
- Relational Characterisations of Paths
- A Sequent Calculus for First-Order Logic
- First-Order Logic According to Fitting

## Cite

×

Abstract_Soundness-AFP

    @article{Abstract_Soundness-AFP,
      author  = {Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel},
      title   = {Abstract Soundness},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Abstract_Soundness.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Feb 13, 2017 : Isabelle2016-1