Tutorials

The idea behind IBMs is already present in a rudimentary way in the work by Davis, Putnam, Logemann and Loveland in the early sixties. The contemporary stream of research on IBMs was initiated with the Plaisted's Hyperlinking calculus in 1992. Since then, other methods have been developed by Plaisted and his coworkers. Billon's disconnection calculus was picked up by Letz and Stenz and has been significantly developed further since then. New methods have also been introduced by Hooker, Baumgartner and Tinelli, and more recently by Ganzinger and Korovin. The stream of publications over the last years demonstrates a growing interest in IBMs. The ideas presented there show that research on IBMs still is in the middle of development, and that there is high potential further improvements and extensions like equality and theory handling, which is currently investigated.

In the tutorial, we will cover the following topics: Early IBMs, the common principle behind IBMs; classification of IBMs (one-level vs. two-level calculi), comparison to resolution and free variable tableaux; selected IBMs in greater detail: ordered semantic hyper linking, the disconnection method, the model evolution calculus; the completeness proof of one selected method; extension to equality reasoning; implementation techniques, particularly the disconnection method.

Gernot Stenz has been directly involved in instance based theorem proving for several years. He is the (co-)author of 12 scientific papers and system descriptions at international conferences and some other publications in journals and books. Nearly all of his more recent publications deal with instance based theorem proving in general and the disconnection calculus in particular. The implementation of theorem prover systems is among his principal matters of interest, he was a co-author of the e-SETHEO prover system, where his work also included automated learning methods for theorem provers and he has been developing and improving the DCTP theorem prover implementation of the disconnection calculus. Both of these systems have won trophies at the annual CADE theorem prover competitions.

Already in 1950s Paul Lorenzen suggested a two person dialogue game to serve as a foundation for constructive logics. It took many years before the exact relation between his game and Gentzen's LJ for intuitionistic logic had been clarified; but nowadays a host of similar games and corresponding analytic proof systems for various forms of logics can be found in the literature.

Circumventing the more abstract forms of dialogue games, that have become popular in so-called game semantics for linear logic and functional programming languages, we will discuss Lorenzen's original game and different generalizations of it to explain some more recent applications to the proof theory of intermediate logics and fuzzy logics.

More precisely, our guided tour through the varied landscape of analytic systems and dialogue games will call at vantage points that (hopefully) allow a clear view at the following areas:

• Parallel versions of Lorenzen's game and corresponding hypersequent systems for intermediate logics.
• Dialogue games as models of distributed proof search.
• Model building, "sequents of relations" and a dialogue game for Goedel-Dummett logic.
• Giles's game for Lukasiewicz logic and its relation to recent proof theoretic results in fuzzy logic.

Note that our "tour" is designed to highlight own results. However, we hope that our approach also makes interesting aspects of related work more visible.

The framework is actually a programming language with a strong type system, but also unbounded recursion. A proof in this system is correct if it is type correct, and if it is guaranteed to terminate.

Agda is a type checker and an interpreter for Structured Type Theory, but not only. It has also commands for developing proofs such as filling in holes, checking termination, asking for information, pretty printing etc.

On top of Agda we have two interfaces, one emacs-based interface that we will be used in the tutorial. The other interface, Alfa, is a graphical interface, which provides syntax directed, direct manipulation of proofs and programs.

The tutorial will cover basics of the type theory, proof construction and interaction with Agda, as well as combining interactive and automated proofs.