Classical Logic in Deep Inference and Some Ideas on Proof Search

deduction, tableaux, etc.) can be conveniently grouped under the
notion of `shallow inference'. Contrary to what happens in the
shallow inference realm, the recently introduced notion of deep
inference allows for inference steps to occur anywhere inside a
formula. This is a very natural notion from the semantic point of
view, but it has nontrivial consequences. Much of the proof theory
of shallow inference has no use in deep inference, in particular
techniques for cut elimination need to be redesigned from scratch.

I will preliminarily report on five years of research on deep
inference. We have now a fully explored formalism in deep inference,
called the Calculus of Structures (CoS), where all the important
logics can be expressed with many benefits and no disadvantages
(since CoS is more general than the other formalisms). I will
introduce CoS by way of examples.

In the second part of the talk I will show some of the benefits of
the CoS presentation of classical logic. In particular, I will show
a technique for exploring a trade-off between size of proofs and
non-determinism in the proof search space which could be interesting
for automated deduction and related areas.

More information on the web site <http://alessio.guglielmi.name/res/cos>.