interana: interactive prover for Multiplicative Linear Logic

Hello,

The members of this group might be interested in the following paper
and the tool. The tool implements the ideas in the paper.  Comments on
both are most welcome.

Kind regards,
Ozan

---
Interaction and Depth against Nondeterminism in Proof Search

Deep inference is a proof theoretic methodology that generalises the
standard notion of inference of the sequent calculus, whereby
inference rules become applicable at any depth inside logical
expressions. Deep inference provides more freedom in the design of
deductive systems for different logics and a rich combinatoric
analysis of proofs. In particular, construction of exponentially
shorter analytic proofs becomes possible, however with the cost of a
greater nondeterminism than in the sequent calculus. In this paper,
building on our previous work on proof search with deep inference, we
show that, by exploiting an interaction and depth scheme in the
logical expressions, the nondeterminism in proof search can be reduced
without losing the shorter proofs and without sacrificing from proof
theoretic cleanliness. We demonstrate our method on deep inference
systems for multiplicative linear logic and classical logic, discuss
its proof complexity and its relation to focusing, and present
implementations.

https://dl.dropbox.com/u/34033496/deep.pdf
---


---
interana: interactive prover for Multiplicative Linear Logic

http://sites.google.com/site/ozankahramanogullari/software/interana
---


-------------------------------------------------------------------------
http://sites.google.com/site/ozankahramanogullari/
--------------------------------------------------------------------------