FTP 2011 - International Workshop on First-Order Theorem Proving

FTP 2011 is the eighth in a series of workshops intended to focus effort on First-Order Theorem Proving as a core theme of Automated Deduction, and to provide a forum for presentation of recent work and discussion of research in progress.

The workshop welcomes original contributions on theorem proving in first-order classical, many-valued, modal and description logics, including nonexclusively: resolution, tableau methods, equational reasoning, term-rewriting, model construction, constraint reasoning, unification, description logics, propositional logic, specialized decision procedures; strategies and complexity of theorem proving procedures; implementation techniques and applications of first-order theorem provers to verification, artificial intelligence, mathematics and education.

See for further information.

Gentzen Systems and Beyond '11

This is a workshop on Gentzen-style proof systems and generalisations or extensions of them. Since the introduction of the Sequent Calculus and Natural Deduction by Gerhard Gentzen in the 1930s, a wide spectrum of formalisms have been used to construct proof systems for logics, including Hypersequents, Display Calculi, Labelled Deductive Systems, Tableaux, Deep Inference, and Proof Nets, to name just a few. The aim of this workshop is in particular to explore and compare the motivations for and relative merits of these different approaches. Potential topics include:

  • Cut-elimination and its applications, e.g. decidability, interpolation, amalgamation, completeness proofs, computational interpretations, etc.
  • Scope, limitations, interrelationships, and philosophical aspects of various formalisms.

A broader aim of this workshop is to build a bridge between researchers into theoretical aspects of structural proof theory and the more application-oriented goals of the Tableaux community, particularly in cases where the methods, such as constructing analytic systems, are shared.

See for further information.