Return
Proofs without syntax
DOI:10.4007/annals.2006.164.1065.png)
Abstract
En 中文
a Proofs are traditionally syntactic, inductively generated objects. This paper presents an abstract mathematical formulation of propositional calculus (propositional logic) in which proofs are combinatorial (graph-theoretic), rather than syntactic. It defines a combinatorial proof of a proposition phi as a graph homomorphism h: C -> G(phi), where G(phi) is a graph associated with phi and C is a coloured graph. The main theorem is soundness and completeness: phi is true if and only if there exists a combinatorial proof h: C -> G(phi).
Keywords:
GRAPHS
Journal
IF:
5.3
Papers:
1.4K
Citations:
1.6W
Organization
Cited Papers
No cited papers available

