arrow
Return

Proofs without syntax

delete2006-11-01
delete39
delete
OA
AI
D
Dominic Hughes *
DOI:10.4007/annals.2006.164.1065delete
deleteOriginal
deleteOriginal request for help
deleteShare
deleteSave
Abstract

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

Annals of Mathematics cover
Annals of Mathematics
IF:
5.3
Papers:
1.4K
Citations:
1.6W

Organization

S
Stanford University
Scholars:
9.6W
Papers: 8.2W
Citations: 17.0W
Cited Papers

Cited Papers

No cited papers available