.png){kind=icon}
返回
.png){kind=icon}
.png){kind=icon}
.png){kind=icon}
.png){kind=icon}
.png){kind=icon}
摘要
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).
Keyword:
GRAPHS
