previous day
next day
all days

View: session overviewtalk overview

10:00-10:30 Session 7: Invited Talks
Proof Schemata and Herbrand Systems  

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.


10:30-11:00Coffee Break
11:00-12:30 Session 8: Invited Talks
Witness algebra, or who needs category theory?

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.

Counter-model-based quantifier Instantiation in SMT

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.


12:30-14:00Lunch Break
14:00-15:30 Session 9: Invited Talks
Taylor Models for ERA

ABSTRACT. Taylor Models for Exact Real Computation with Applications

Higher-order automated theorem proving -- Why has there been such a resistance?
ENIGMA Given Clause Guidance
15:30-16:00Coffee Break
16:00-17:30 Session 10: Invited Talks
Breaking the rules
Abstraction-refinement automated reasoning
Andrei ... Superman or Rocketman?