Invited Speakers

Michel Parigot (University of Paris VII)

Deep inference: why and how?

Abstract. Deep inference is a deduction framework introduced a decade ago by Alessio Guglielmi. The starting idea is to allow deduction rules to apply arbitrarily deep inside formulae, contrary to traditional proof systems like natural deduction and sequent calculus, where deduction rules deal only with their outermost structure. This simple idea leads to a natural change in the underlying structure of proofs, where rules are unary: one premiss and one conclusion, which open new possibilites for deduction systems.

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

Abstract. The Thousands of Problems for Theorem Provers (TPTP) problem library is the basis of a well known and well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. The services and standards provided by this infrastructure have made it increasingly easy to build, test, and apply reasoning systems that use ATP technology. This talk reviews the core features of the TPTP world, describes some successful applications, and gives an overview of the most recent developments.

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