19TH INTERNATIONAL CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING

# LPAR ON THURSDAY, DECEMBER 19TH, 2013

09:00-10:00 Session 17: Invited talk by Stephan Schulz
 09:00 Where, What, and How? Lessons from the Evolution of ESPEAKER: Stephan SchulzABSTRACT. E is a theorem prover for first-order logic with equality. It has evolved over the last 15 years from a basic implementation of the superposition calculus to a fully-featured theorem prover supporting a rich language, an efficient inference engine, and several levels of manual and automatic control. Most of the changes to the prover have been conservative extensions. This allows us to take a virtual step back in time and to evaluate which features have had how much of an influence on the power of the system, and thus maybe inform us where future research is particularly promising.
10:00-10:30Coffee Break
10:30-12:00 Session 18
 10:30 Polarizing Double Negation TranslationsSPEAKER: Olivier HermantABSTRACT. Double-negation translations allow to encode and decode classical proofs in intuitionistic logic. We show that, in the cut-free fragment, we can simplify the translations and introduce fewer negations. To achieve this, we consider the polarization of the formulae and adapt those translation to the different connectives and quantifiers. We show that the embedding results still hold, using a customized version of the focused classical sequent calculus. We also prove the latter equivalent to more usual versions of the sequent calculus. This polarization process allows lighter embeddings, and sheds some light on the relationship between intuitionistic and classical connectives. 10:50 A Proof of Strong Normalisation of the Typed Atomic Lambda-CalculusSPEAKER: Willem HeijltjesABSTRACT. The atomic lambda-calculus is a typed lambda-calculus with explicit sharing, which originates in a Curry-Howard interpretation of a deep-inference system for intuitionistic logic. It has been shown that it allows fully lazy sharing to be reproduced in a typed setting. The talk will introduce the calculus in detail, and give an outline of the latest development, a proof of strong normalization of the typed atomic lambda-calculus using Tait's reducibility method. 11:10 Complexity Analysis in Presence of Control Operators and Higher-order FunctionsSPEAKER: Giulio PellittaABSTRACT. A polarized version of Girard, Scedrov and Scott’s Bounded Linear Logic is introduced and its normalization properties studied. Following Laurent, the logic naturally gives rise to a type system for the λμ-calculus, whose derivations reveal bounds on the time complexity of the underlying term. This is the first example of a type system for the λμ-calculus guaranteeing time complexity bounds for typable programs. 11:30 Semantic A-Translations and Super-Consistency entail Classical Cut EliminationSPEAKER: Olivier HermantABSTRACT. We show that if a theory R defined by a rewrite system is super-consistent, the classical sequent calculus modulo R enjoys the cut elimination property, which was an open question. For such theories it was already known that proofs strongly normalize in natural deduction modulo R, and that cut elimination holds in the intuitionistic sequent calculus modulo R. We first define a syntactic and a semantic version of Friedman's A-translation, showing that it preserves the structure of pre-Heyting algebra, our semantic framework. Then we relate the interpretation of a theory in the A-translated algebra and its A-translation in the original algebra. This allows to show the stability of the super-consistency criterion and the cut-elimination theorem. 11:50 Effectively Monadic PredicatesSPEAKER: Margus VeanesABSTRACT. Monadic predicates play a prominent role in many decidable cases, including decision procedures for symbolic automata. We are here interested in discovering whether a formula can be rewritten into a Boolean combination of monadic predicates. Our setting is quantifier-free formulas over a decidable background theory, such as arithmetic and we here develop a semi-decision procedure for extracting a monadic decomposition of a formula when it exists.
12:00-14:00Lunch
14:00-15:30 Session 19
 14:00 Incorporating Hypothetical Views and Extended Recursion into SQL Database SystemsSPEAKER: Gabriel ArandaABSTRACT. Current database systems supporting recursive SQL impose restrictions on queries such as linearity, and do not implement mutual recursion. In a previous work we presented the language and prototype R-SQL to overcome those drawbacks. Now we introduce a formalization and an implementation of the database system HR-SQL that, in addition to extended recursion, incorporates hypothetical reasoning in a novel way which cannot be found in any other SQL system, allowing both positive and negative assumptions. The formalization extends the fixpoint semantics of R-SQL. The implementation improves the eciency of the previous prototype and is integrated in a commercial DBMS. 14:10 Zenon Modulo: When Achilles Outruns the Tortoise using Deduction ModuloSPEAKER: Pierre HalmagrandABSTRACT. We propose an extension of the tableau-based first order automated theorem prover Zenon to deduction modulo. The theory of deduction modulo is an extension of predicate calculus, which allows us to rewrite terms as well as propositions, and which is well suited for proof search in axiomatic theories, as it turns axioms into rewrite rules. We also present a heuristic to perform this latter step automatically, and assess our approach by providing some experimental results obtained on the benchmarks provided by the TPTP library, where this heuristic is able to prove difficult problems in set theory in particular. Finally, we describe an additional backend for Zenon that outputs proof certificates for Dedukti, which is a proof checker based on the lambda-Pi-calculus modulo. 14:30 Polar: A Framework for Proof RefactoringSPEAKER: Iain WhitesideABSTRACT. We present a prototype refactoring framework based on graph rewriting and bidirectional transformations that is designed to be generic, extensible, and declarative. Our approach uses a language-independent graph meta-model to represent proof developments in a generic way. We use graph rewriting to enrich the meta-model with dependency information and to perform refactorings, which are written as declarative rewrite rules. Our framework, called POLAR, is implemented in the GRGEN graph rewriting engine. 14:50 The Complexity of Clausal Fragments of LTLSPEAKER: Vladislav RyzhikovABSTRACT. We introduce and investigate a number of fragments of propositional temporal logic LTL over the flow of time (Z, <). The fragments are defined in terms of the available temporal operators and the structure of the clausal normal form of the temporal formulas. We determine the computational complexity of the satisfiability problem for each of the fragments, which ranges from NLogSpace to PTime, NP and PSpace. 15:10 A Seligman-style Tableau SystemSPEAKER: Klaus Frovin JoergensenABSTRACT. Proof systems for hybrid logic typically use $@$-operators to access information hidden behind modalities; this labeling approach lies at the heart of most resolution, natural deduction, and tableau systems for hybrid logic. But there is another, less well-known approach, which we have come to believe is conceptually clearer. We call this Seligman-style inference, as it was first introduced and explored by Jerry Seligman in the setting of natural deduction and sequent calculus in the late 1990s. The purpose of this paper is to introduce a Seligman-style tableau system. The most obvious feature of Seligman-style systems is that they work with arbitrary formulas, not just formulas prefixed by $@$-operators. To achieve this in a tableau system, we introduce a rule called $\mathsf{GoTo}$ which allows us to jump to a named world'' on a tableau branch, thereby creating a local proof context (which we call a \textit{block}) on that branch. To the surprise of at least some of the authors (who have worked extensively on developing the labeling approach) Seligman-style inference is often much clearer. Not only is the approach more modular, but individual proofs are often more direct. We conclude with a discussion of termination and first-order hybrid logic.
15:30-16:00Coffee Break
16:00-17:30 Session 20