ABSTRACT. Herbrand's theorem allows to transform a proof p of a first-order formula F to a proof p' of a propositional formula F' obtained from F by replacing quantifiers by terms instantiations. These instantiations may contain important information on the validity of F. Generally, the construction of such a proof p' requires cut-elimination in the proof p (or at least the elimination of quantified cuts). The method CERES (cut-elimination by resolution) provides an algorithmic tool to compute F' even without constructing a cut-free proof p'. In proofs with mathematical induction Herbrand's theorem typically fails. To overcome this problem we replace induction by recursive definitions and proofs by proof schemata. An extension of CERES to proof schemata (CERESs) allows to compute inductive definitions of Herbrand expansions (so-called Herbrand systems), resulting in a form of Herbrand's theorem for inductive proofs.

ABSTRACT. Witness algebra, or
Who needs category theory?

Of course mathematicians do, at least some of them do, because category theory is instrumental in some branches of mathematics, e.g. algebraic topology.

But what about computer scientists or physicists? Do they need category theory?

If category theory is your hammer, some computing problems look like appropriate nails. However the speaker was not impressed and remained skeptical. When he learned that the generally accepted mathematical basis for topological quantum computing is sophisticated category theory, he proposed to his long-time collaborator Andreas Blass to ``decategorize" topological quantum computing.

It turned out, surprisingly, that category theory or something like it is necessary for topological quantum computing. Moreover the root cause of the necessity is not specific to topological quantum computing. There should be numerous other computing problems where something like category theory is necessary. Understanding the root cause allowed us to simplify the mathematical basis for the topological quantum computing and to decategorize it to the extent possible.

In the main part of the talk, without assuming any knowledge of category theory or quantum computing, we illustrate, on a simplified example, why category theory or something like it is necessary for topological quantum computing.

ABSTRACT. Reasoning efficiently about formulas containing both quantifiers and built-in symbols for a given background theory remains a challenge in automated deduction. However, several advances have been made in the last few years in two main directions: integrating theory reasoning in general-purpose calculi and integrating quantified reasoning into frameworks for ground Satisfiability Modulo Theories (SMT). Focusing on the latter, this talk provides an overview of a general approach to reason with quantified formulas in SMT. The approach maintains a set S of ground formulas incrementally expanded with selected instances of quantified input formulas, with the selection based on counter-models of S. In addition to being quite effective in practice, in first-order theories that admit quantifier elimination and have a decidable universal fragment, this approach also leads to practically efficient decision procedures for the full theory.

ABSTRACT. Taylor Models for Exact Real Computation with Applications