IJCAR on Monday, July 19th

09:00‑10:00 Invited Talk
Location: AT LT5
09:00 Leonardo de Moura (Microsoft Research Redmond)
Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development

Symbolic reasoning is in the core of many software development tools such as: bug-finders, test-case generators, and verifiers. Of renewed interest is the use of symbolic reasoning for synthesing code, loop invariants and ranking functions. Satisfiability Modulo Theories (SMT) solvers have been the focus of increased recent attention thanks to technological advances and an increasing number of applications. In this paper we review some of these applications that use software verifiers as bug-finders "on steroids" and suggest that new model finding techniques are needed to increase the set of applications supported by these solvers.

10:30‑12:00 Applications
Location: AT LT5
10:30 Vincent Cheval, Hubert Comon-Lundh and Stephanie Delaune
Automating security analysis: symbolic equivalence of constraint systems

We consider security properties of cryptographic protocols, that are either trace properties (such as confidentiality or authenticity) or equivalence properties (such as anonymity or strong secrecy).

Infinite sets of possible traces are symbolically represented using deducibility constraints. We give a new algorithm that decides the trace equivalence for the traces that are represented using such constraints, in the case of symmetric/asymmetric encryption and signatures.

Our algorithm is implemented and performs well on typical benchmarks. This is the first implemented algorithm, deciding symbolic trace equivalence.

11:00 Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Daniel Weller and Bruno Woltzenlogel Paleo
The Proof Transformation System CERES

Cut-elimination is the most prominent form of proof transformation in logic. The elimination of cuts in formal proofs corresponds to the removal of intermediate statements (lemmas) in mathematical proofs. The cut-elimination method CERES (cut-elimination by resolution) works by extracting an always unsatisfiable set of clauses from a proof with cuts. Any resolution refutation of this set then serves as a skeleton for an atomic cut normal form (ACNF), an LK-proof with only atomic cuts.

The system ceres (see http://www.logic.at/ceres), an implementation of CERES, has been used successfully in analyzing nontrivial mathematical proofs (see [1]). A major problem in using ceres in mathematical practice is due to the large size of the output proofs, which are hard to interpret by humans. To overcome this problem, we extended the system by algorithms extracting Herbrand sequents, which contain the essential mathematical information of the constructed ACNF. It turned out that redundancy in the ACNF is still reflected in the Herbrand sequent and, therefore, methods of (algebraic and logical) simplification of Herbrand sequents have been added to CERES. In this paper we describe the main features of the ceres system with special emphasis on the extraction of Herbrand sequents and the corresponding simplification methods. We demonstrate the Herbrand sequent extraction by a mathematical example. A new version of ceres capable of performing cut-elimination in higher-order logic is under development ([2]).

[1] M. Baaz, S. Hetzl, A. Leitsch, C. Richter and H. Spohr. CERES: An Analysis of Fürstenberg's Proof of the Infinity of Primes, Theoretical Computer Science 403(2-3), 160-175, 2008 [2] S. Hetzl, A. Leitsch, D. Weller, B. Woltzenlogel Paleo. A Clausal Approach to Proof Analysis in Second-Order Logic, Logical Foundations of Computer Science 2009, Sergei Artemov and Anil Nerode (eds.), Springer LNCS 5407

11:15 Daniel Kühlwein, Marcos Cramer, Peter Koepke and Bernhard Schröder
Premise Selection in the Naproche System

The Naproche project (Natural language Proof Checking) studies the semi-formal language of mathematics from an interdisciplinary point of view.

The Naproche System checks mathematical texts written in a controlled natural language for syntactical and mathematical correctness. Automated theorem provers (ATPs) are used to check that each statement is a logical consequence of its premises, the preceding axioms, theorems, definitions and assumptions. The longer a texts gets the more premises are available. Generally, the more premises are available, the harder it is for an ATP to find a proof for a conjecture.

In this paper we describe a premises selection algorithm that is based on textual and logical proximity of statements and present first results of its implementation. The algorithm tries to mimic the human way of understanding mathematical texts.

11:30 Martin Suda, Christoph Weidenbach and Patrick Wischnewski
On the Saturation of YAGO

YAGO is an automatically generated ontology out of Wikipedia and WordNet. It is created in a proprietary flat text file format and a core comprises 10 million facts and formulas. We present a translation of YAGO into the Bernays-Schoenfinkel class with equality. A new variant of the superposition calculus is sound, complete and terminating for this class. Employing extended term indexing data structures the calculus is implemented in SPASS-YAGO. YAGO can be finitely saturated by SPASS-YAGO in about 4 hours. We have found 49 inconsistencies in the ontology which we have fixed. SPASS-YAGO can then prove non-trivial conjectures with respect to the resulting saturated and consistent clause set of about 2 GB in less than one second.

12:00 Geoff Sutcliffe
Results of the CASC-J5 System Competition
14:00‑15:00 Description Logic II
Location: AT LT5
14:00 Birte Glimm, Ian Horrocks and Boris Motik
Optimized Description Logic Reasoning via Core Blocking

State of the art reasoners for expressive Description Logics, such as those that underpin the OWL ontology language, are typically based on highly optimised implementations of (hyper-) tableau algorithms. In spite of their numerous optimisations, there are still existing and emerging ontologies that pose a significant challenge to such reasoners, mainly because of the size of the (abstractions of) models that they (try to) construct. To address this problem we propose a new "speculative" blocking technique that tries to identify and halt redundant construction at a much earlier stage than standard blocking techniques. An evaluation of a prototypical implementation of (several variations of) this technique in the HermiT reasoner shows that it can dramatically reduce the size of constructed "models" and greatly reduce the time required for reasoning.

14:30 Yevgeny Kazakov
An Extension of Complex Role Inclusion Axioms in the Description Logic SROIQ

We propose an extension of the syntactic restriction for complex role inclusion axioms in the description logic SROIQ. Like the original restriction in SROIQ, our restrictions can be checked in polynomial time and they guarantee regularity for the sets of role chains implying roles, and thereby decidability for the main reasoning problems. But unlike the original restrictions, our syntactic restrictions can represent any regular compositional properties on roles. In particular, many practically relevant complex role inclusion axioms, such as those describing various parthood relations, can be expressed in our extension, but could not be expressed in original SROIQ.

15:30‑17:30 Termination
Location: AT LT5
15:30 Nao Hirokawa and Aart Middeldorp
Decreasing Diagrams and Relative Termination

In this paper we use the decreasing diagrams technique to show that a left-linear term rewrite system $\RR$ is confluent if all its critical pairs are joinable and the critical pair steps are relatively terminating with respect to $\RR$. We further show how to encode the rule-labeling heuristic for decreasing diagrams as a satisfiability problem. Experimental data for both methods are presented.

16:00 Friedrich Neurauter, Aart Middeldorp and Harald Zankl
Monotonicity Criteria for Polynomial Interpretations over the Naturals

Polynomial interpretations are a useful technique for proving termination of term rewrite systems. In an automated setting, termination tools are concerned with parametric polynomials whose coefficients (i.e., the parameters) are initially unknown and have to be instantiated suitably such that the resulting concrete polynomials satisfy certain conditions. We focus on monotonicity and well-definedness, the two main conditions that are independent of the respective term rewrite system considered, and provide exact constraints on the abstract coefficients for linear, quadratic and cubic parametric polynomials such that monotonicity and well-definedness of the resulting concrete polynomials are guaranteed whenever the constraints are satisfied. Our approach subsumes the absolute positiveness approach, which is currently used in many termination tools. In particular, it allows for negative numbers in certain coefficients. We also give an example of a term rewrite system whose termination proof relies on the use of negative coefficients, thus showing that our approach is more powerful.

16:30 Sarah Winkler and Aart Middeldorp
Termination Tools in Ordered Completion

Ordered completion is one of the most frequently used calculi in equational theorem proving. The performance of an ordered completion run strongly depends on the reduction order supplied as input. This paper describes how termination tools can replace fixed reduction orders in ordered completion procedures, thus allowing for a novel degree of automation. Our method can be combined with the multi-completion approach proposed by Kondo and Kurihara. We present experimental results obtained with our ordered completion tool omkbTT for both ordered completion and equational theorem proving.

17:00 Albert Rubio
Results of the Termination 2010 System Competition
17:30‑18:00 Herbrand Award Ceremony
Location: AT LT5
17:30 Maria Paola Bonacina (Master of Ceremony)
Presentation of the Herbrand Award to David Plaisted