Oxford Quantum Talks Archive
Phase semantics and focused proof search for the Lambek-Grishin calculus
Arno Bastenhof, University of UtrechtFlowin'Cat 2010, October 2010, University of Oxford
The Lambek-Grishin calculus (LG) conservatively extends Lambek's (unit-free) non-associative syntactic calculus by a coresiduated family of connectives, consisting of a multiplicative disjunction (par) and direction-sensitive subtractions. We propose a one-sided sequent calculus for LG accommodating focussing, a technique introduced by Andreoli within full linear logic that aims at removing don't care nondeterminism from Cut-free backward chaining proof search. To demonstrate completeness, we construct a syntactic phase model wherein every 'truth' is shown to have a corresponding focused proof.
[video] [streaming video] [slides]