Complementation: a bridge between finite and infinite proofs
Logic in Computer Science
2023-04-12 v1
Abstract
When a proposition has no proof in an inference system, it is sometimes useful to build a counter-proof explaining, step by step, the reason of this non-provability. In general, this counter-proof is a (possibly) infinite co-inductive proof in a different inference system. In this paper, we show that, for some decidable inference systems, this (possibly) infinite proof has a representation as a finite proof in yet another system, equivalent to the previous one.
Cite
@article{arxiv.2304.05085,
title = {Complementation: a bridge between finite and infinite proofs},
author = {Gilles Dowek and Ying Jiang},
journal= {arXiv preprint arXiv:2304.05085},
year = {2023}
}