Linear inferences and derivations 3

[This is the third of 3 emails to the Frogs list concerning linear 
inferences and derivations in deep inference. The first is about linear 
inferences that are independent of the usual basis {switch, medial}. The 
second concerns the size of linear derivations in deep inference, in the 
presence of units, and the third will present recent work towards 
efficiently automating the checking and search of new linear inferences.]

Dear all,

I would like to advertise the following work of Alvin Sipraga (title and 
abstract below):

http://arcturus.su/mimir/autolininf.pdf

and website:

http://arcturus.su/mimir/

Alvin did an undergraduate project with me last year and this work 
implements an approach towards conducting proof-search in the linear 
fragment of propositional deep inference. In upcoming work it is proved 
that proof-search in arbitrary Gentzen/Frege systems can be reduced (in 
polynomial-time) to proof-search in the linear fragment.

Kind regards,
Anupam


An automated search of linear inference rules

A linear inference is a logical inference where every variable occurs 
exactly once in the premiss and conclusion. In the paradigm of deep 
inference there are two well-studied linear inference rules, switch and 
medial. It has been shown that these are insufficient to generate all 
linear inferences under composition and deep inference. We consider the 
problem of finding the minimal inference not generated by switch and 
medial using computational methods and develop a tool to search for it.