eric@uio.no (Eric Monteiro) (05/21/91)
We are a group of people in oslo (who like everybody else are)
interested in girard's linear logic.
Further below follows a paper where we
give an alternative semantics for linear logic with "wirings" :
* identify the litereals which will end up as axiom (leaf)nodes.
Remark : - the bookkeeping of instances makes this possible in linear logic
- the approach is similar to proof nets but our approach covers
all of (propositional) linear logic
* our ambition is to use the "wirings" for two purposes : automated proof search,
models of computation (more general than Petri nets).
Remark : - these further ideas are for the future
- anyone interested in automated proof search should note that
propositional linear logic is undecidable ("Decision problems for
propositional linear logic", P.Lincoln et al., in Proc. 31st annual
IEEE symp. on foundation of computer science, October 1990)
- eric monteiro (eric@nr.no), also writing for
morten elvang, herman jervell, arild waaler