## Invited Speakers | |

## Michel Parigot (University of Paris VII)## Deep inference: why and how?
While proofs in usual deduction systems take the asymmetric form of a tree, deep inference allows to design deduction systems where proofs can be dualised by flipping. More generally, it allows to shift the monotone connectives - like and, or, not - from the level of formulas to the level of proofs. The resulting system, called open deduction, decreases synctactic dependency: proofs which only differs by the order of application of rules to independant subformulas have a unique canonical form, where rules are somehow applied in parallel. At the level of logical rules, deep inference allows also to have more symmetries and finer structural properties than sequent calculus. For instance, cut and identity become really dual of each other, whereas they are only morally so in sequent calculus, and all structural rules can be reduced to their atomic form, whereas this is false for contraction in sequent calculus. In this talk we give a survey of the main possibilities offered by Deep Inference and the questions it raises. ## Geoff Sutcliffe (University of Miami)## The TPTP World - Infrastructure for Automated Reasoning
LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR LPAR |