Firstorder proofs without syntax
Dominic Hughes ( Chief Scientist, concept.io )

16:30 12th November 2013 ( week 5, Michaelmas Term 2013 )Lecture Theatre B
Proofs of firstorder logic are traditionally syntactic, built inductively from symbolic inference rules. This talk reformulates
firstorder logic with proofs which are combinatorial rather than syntactic. A combinatorial proof is defined by graphtheoretic
conditions, verifiable in polynomial time.
To be accessible to a broad audience of computer scientists, mathematicians and logicians, this lecture uses many illustrative
examples and presupposes only introductory undergraduatelevel logic.
This work extends 'Proofs Without Syntax' [Annals of Mathematics, 2006], which treated the propositional case.