First-order proofs without syntax
Dominic Hughes ( Chief Scientist, concept.io )
- 16:30 12th November 2013 ( week 5, Michaelmas Term 2013 )Lecture Theatre B
Proofs of first-order logic are traditionally syntactic, built inductively from symbolic inference rules. This talk reformulates first-order logic with proofs which are combinatorial rather than syntactic. A combinatorial proof is defined by graph-theoretic 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 undergraduate-level logic.
This work extends 'Proofs Without Syntax' [Annals of Mathematics, 2006], which treated the propositional case.
Speaker bio
Based in Silicon Valley, Dominic has the good fortune of being able to split his research between industry (machine learning and algorithm design, as Chief Scientist and cofounder of concept.io) and academia (graphical logic and categories, until recently as a Visiting Scholar at Stanford). Before Stanford, Dominic did his D.Phil. right here in Oxford, with Luke Ong. Prior to that he studied mathematics at Cambridge.Share this:
