Special Session on the Past, Present and Future of Automated Deduction

August 3, 14:00 - 17:30

Invited Speakers

Chair: Aart Middeldorp

History and Prospects for First-Order Automated Deduction

David Plaisted
(University of North Carolina at Chapel Hill, USA)

On the fiftieth anniversary of the appearance of Robinson's resolution paper [Robinson 1965], it is appropriate to consider the history and status of theorem proving, as well as its possible future directions. Here we discuss the history of first-order theorem proving both before and after 1965, with some personal reflections. We then generalize model-based reasoning to first-order provers, and discuss what it means for a prover to be goal sensitive. We also present a way to analyze asymptotically the size of the search space of a first-order prover in terms of the size of a minimal unsatisfiable set of ground instances of a set of first-order clauses.

Robinson, J.: A machine-oriented logic based on the resolution principle. Journal of the ACM 12(1), 23-41 (1965)


Andrei Voronkov
(University of Manchester, UK)

We describe a new architecture for first-order resolution and superposition theorem provers called AVATAR (Advanced Vampire Architecture for Theories and Resolution). Its original motivation comes from the problem well-studied in the past --- dealing with problems having clauses containing propositional variables and other clauses that can be split into components with disjoint sets of variables. Such clauses are common in problems coming from applications, for example in verification and program analysis, where many ground literals occur in the problems and even more are generated during the proof-search.
This problem was previously addressed by adding various versions of splitting. The addition of splitting resulted in considerable improvements in the performance of theorem provers. However, even with various versions of splitting implemented, the performance of superposition theorem provers is nowhere near SMT solvers on purely ground problems or SAT solvers on propositional problems. In AVATAR ground problems are solved with the same efficiency as that of the underlying SMT solver. On problems with quantifiers the introduction of AVATAR in Vampire resulted in drastic improvements over all previous implementation of splitting. Several hundred TPTP problems previously unsolvable by any first-order theorem prover, including Vampire itself, have been proved, including an open problem in semigroups.

Chair: Amy Felty

On the Role of Proof Theory in Automated Deduction

Frank Pfenning
(Carnegie Mellon University, USA)

Since the seminal work by Gentzen, who developed both natural deduction and the sequent calculus, there has been a line of research concerned with discovering deep structural properties of proofs in order to control the search space in theorem proving. This is particularly important in non-classical logics where traditional model-theoretic techniques may be more difficult to apply. We will walk through some of the key developments, starting with cut elimination and identity expansion, followed by focusing, polarization, and the separation of judgments and propositions. These concepts have been surprisingly robust, applicable to many non-classical logics, to the extent that one may consider them a litmus test on whether a set of rules or axioms form a coherent logic. We illustrate how each of these ideas affect proof search. In some cases, proofs are sufficiently restricted so that proof search can be seen as a fundamental computational mechanism, giving rise to logic programming.

Stumbling Around in the Dark: Lessons from Everyday Mathematics

Ursula Martin
(University of Oxford, UK)

The growing use of the internet for collaboration, and of numeric and symbolic software to perform calculations it is impossible to do by hand, not only augment the capabilities of mathematicians, but also afford new ways of observing what they do. In this essay we look at four case studies to see what we can learn about the everyday practice of mathematics: the experiments for the collaborative production of mathematics, which tell us about mathematicians attitudes to working together in public; the experiments in the same vein, from which we can examine in finer grained detail the kinds of activities that go on in developing a proof; the mathematical questions and answers in math overflow, which tell us about mathematical-research-in-the-small; and finally the role of computer algebra, in particular the GAP system, in the production of mathematics. We conclude with perspectives on the role of computational logic.

Location: Takustrasse 9, 14195 Berlin, Germany (More information on how to reach the venue)
Room: 003