Proofs without syntax

By Dominic J. D. Hughes. 2004

86 citations recorded by the source corpus.

Proofs are traditionally syntactic, inductively generated objects. This paper presents an abstract mathematical formulation of propositional calcu lus (propositional logic) in which proofs are combinatorial (graph-theoretic), rather than syntactic. It defines a combinatorial proof of a proposition 0 as a graph homomorphism h : C ? G((f>), where G((j>) is a graph associated with and C is a coloured graph. The main theorem is soundness and completeness: (f) is true if and only if there exists a combinatorial proof h : C ?? G(

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/236b0dcf92ed8f18eee13e5171dad76ad1877dff