2023/04/11 by Gilles Dowek, Ying Jiang, Dowek, Gilles +1
Arts and Humanities · Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Philosophy and History of Science #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.2304.05085
openalex publication_date 2023/04/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.