Date: Wed, 20 Nov 1996 19:15:08 GMT Server: Apache/1.0.3 Content-type: text/html Content-length: 2064 Last-modified: Thu, 25 Apr 1996 15:00:00 GMT Structurally Free Logic

Structurally Free Logic

Description:
In the last few years there has been great interest in so-called "substructural logics," whereby various well-known logics are distinguished by the structural rules that are postulated in the Gentzen systems for the logics. Most notorious have been thinning (relevance logic), contraction (BCK logic), and linear logic (linear logic). But there is no reason to stop there, as people have considered non-commutative linear logic (better, the associative Lambek calculus), and people have even looked at non-associative logice. The point of view taken in this project is that structural rules should be done away with altogether, and their place taken by explicit introduction rules for combinators. Combinators are take as "first-class' objects, and still a cut-elimination theorem can be proven. Further the ternary relational semantics (Routley-Meyer semantics) for the Lambek calculus can be extended so as to provide a semantics for combinatory logic. The key idea is that a ternary relation on states can be interpreted as an indexed action on states. So a set of states (a proposition) can be simultaneously be viewed as a set of actions, and so it makes sense to talk of applying one proposition to another (even itself). There are still a number of open problems, mostly centering about the addition of conjunction and disjunction. These include proving the cut- theorem with respect to the distributive combination of the two, and providing a completeness theorem for their non-distributive combination.

Associated Faculty: Michael Dunn

Affiliated Projects: Robert K. Meyer (Automated Reasoning Project, Australian National University)

Support: College of Arts and Sciences

Return to Computer Science Research Page