[Back]

B. Afshari:
"When formal proofs meet formal grammars";
Talk: Gothenburg Logic Seminar, Gothenburg, Schweden (invited); 2015-09-15 - 2015-09-16.

Herbrand's seminal work from 1930 demonstrates how to reduce first-order logic to propositional logic. Herbrand's theorem, in its simplest form, states that if an existential formula Ǝx F(x) (with F quantifier-free) is valid then there exist terms t0, ... , tk such that F(t0) v...v F(tk) is a tautology. In this talk I will introduce a novel approach to Herbrand's theorem based on a recently discovered connection between proof theory and formal language theory. To a proof of a formula F in first-order logic one can associate a formal grammar that succinctly generates the terms needed to form a tautology from F. The approach not only captures Herband's theorem but also opens the door to tackle a number of questions in proof theory such as proof equivalence, proof compression and proof complexity which will be discussed.