University of Oxford Logo University of OxfordDepartment of Computer Science - Home
On Facebook
Facebook
Follow us on twitter
Twitter
Linked in
Linked in
Flickr
Flickr
Google plus
Google plus
Digg
Digg
Pinterest
Pinterest
Stumble Upon
Stumble Upon

Oxford Quantum Talks Archive

Phase semantics and focused proof search for the Lambek-Grishin calculus

Arno Bastenhof, University of Utrecht
Flowin'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]