ESCoR on Monday, August 21st

Invited System Paper (09:00‑10:00)
Chair: Geoff Sutcliffe

09:00‑10:00

Matt Kaufmann (University of Texas) Maintaining the ACL2 Theorem Proving System [pdf] This talk will provide a view into the task of improving the ACL2 theorem prover to meet users' needs.

Systems Papers (10:00‑10:30)
Chair: Geoff Sutcliffe

10:00‑10:30

Virgile Prevosto (CEA -- LIST, Centre de Saclay) Uwe Waldmann (MPI für Informatik) SPASS+T SPASS+T is an extension of the superposition-based theorem prover SPASS that allows us to enlarge the reasoning capabilities of SPASS using an arbitrary SMT procedure for arithmetic and free function symbols as a black-box. We discuss the architecture of SPASS+T and the capabilities, limitations, and applications of such a combination.

Break (10:30‑11:00)

Systems Papers (11:00‑12:30)
Chair: Geoff Sutcliffe

11:00‑11:30	Petr Pudlak (KTIML, MFF, Charles University, Prague, Czech Republic) Search for faster and shorter proofs using machine generated lemmas When we have a set of conjectures formulated in a common language and proved from a common set of axioms using an automated theorem prover, it is often possible to automatically construct lemmas that can be used to prove the conjectures in a shorter time and/or with shorter proofs. We have implemented a system that repeatedly tries to improve the set of assumptions for proofs of given conjectures using lemmas that it extracts from the proofs constructed by an automated theorem prover. In many cases it can significantly reduce the total time or the overall sum of the lengths of the proofs of the conjectures. We present several examples of such sets of conjectures and show the improvements gained by the system.
11:30‑12:00	Jia Meng (NICTA) Lawrence Paulson (University of Cambridge) Lightweight Relevance Filtering for Machine-Generated Resolution Irrelevant clauses in resolution problems increase the search space, making it hard to find proofs in a reasonable time. Simple relevance filtering methods, based on counting function symbols in clauses, improves the success rate for a variety of automatic theorem provers and with various initial settings. We have designed these techniques as part of a project to link automatic theorem provers to the interactive theorem prover Isabelle. They should be applicable to other situations where the resolution problems are produced mechanically and where completeness is less important than achieving a high success rate with limited processor time.
12:00‑12:15	Jia Meng (NICTA) Lawrence Paulson (University of Cambridge) Translating Higher-Order Problems to First-Order Clauses Formal specifications and verifications are typically carried out through interactive provers that use higher-order logic. A promising approach to improve automation of interactive provers is by integrating them with automatic provers, which are usually based on first-order logic. Consequently, it is necessary to translate higher-order logic formulae to first-order form. An important issue is the preservation of higher-order logic's types. This translation should be correct and also practical. We have implemented three higher-order to first-order translations, with particular emphasis on the formalisation of types in first-order logic. In this paper, we will describe our translations and experimental data that compares the three translations in respect of their success rates for various automatic provers.

Lunch break (12:30‑14:00)

Invited Application Paper (14:00‑15:00)
Chair: Renate Schmidt

14:00‑15:00

Johan Bos (University of Rome "La Sapienza") Three Stories on Automated Reasoning for Natural Language Understanding [ppt] Three recent applications of computerised reasoning in natural language processing are presented. The first is a text understanding system developed in the late 1990s, the second is a spoken-dialogue interface to a mobile robot and automated home, and the third is a system that determines textual entailment. In all of these applications, off-the-shelf tools for reasoning with first-order logic (theorem provers as well as model builders) are employed to assist in natural language understanding. This overview is not only an attempt to identify the added value of computerised reasoning in natural language understanding, but also to point out the limitations of the first-order inference techniques currently used in natural language processing.

Applications Papers (15:00‑15:30)
Chair: Renate Schmidt

15:00‑15:30

Michael Wessel (TUHH) Ralf Moeller (Hamburg University of Technology) A Flexible DL-based Architecture for Deductive Information Systems We consider the information system domain of deductive geographic information systems (GIS), which can be called a ``non-standard domain''. We describe the problems encountered and pragmatic solutions found during the endeavor of building an ontology-based query answering system to digital city maps. We used RACERPRO as a description logic system which can be called an empirically successful system.

Break (15:30‑16:00)

Applications Papers (16:00‑17:30)
Chair: Renate Schmidt

16:00‑16:30	Gerd Beuster (University Koblenz-Landau) Niklas Henrich (University Koblenz-Landau) Markus Wagner (University Koblenz-Landau) Real World Verification - Experiences from the Verisoft Email Client This paper reports our experiences developing a completely verified email client. The formal specification of the email client includes all informal requirements and security goals. Compliance to the formal specification has been proven for the complete source code. The email client is part of project Verisoft, where pervasively verified systems are developed.
16:30‑16:45	Florian Rabe (CMU) Towards Determining the Subset Relation between Propositional Modal Logics We present design and implementation of a system that tries to automatically determine the subset relation between two given axiomatizations of almost arbitrary propositional modal logics, which is an open challenge problem for automated theorem proving. A test suite shows that relatively simple strategies can lead to satisfactory results, but also that certain subproblems are hard for current automated theorem provers.
16:45‑17:00	Gonçalo Lopes (Centro de Inteligência Artificial - CENTRIA - Universidade Nova de Lisboa) Luís Moniz Pereira (Centro de Inteligência Artificial - CENTRIA - Universidade Nova de Lisboa) Prospective Logic Programming with ACORDA As we face the real possibility of modelling programs that are capable of non-deterministic self-evolution, we are confronted with the problem of having several different possible futures for a single such program. It is desirable that such a system be somehow able to look ahead, prospectively, into such possible futures, in order to determine the best courses of evolution from its own present, and then to prefer amongst them. This is the objective of the ACORDA, a prospective logic programming system. We start from a real-life working example of differential medical diagnosis illustrating the benefits of addressing these concerns, and follow with a brief description of the concepts and research results supporting ACORDA, and on to their implementation. Then we proceed to fully specify the implemented system and how we addressed each of the enounced challenges. Next, we take on the proffered example, as codified into the system, and describe the behaviour of ACORDA as we carefully detail the resulting steps involved. Finally, we elaborate upon several considerations regarding the current limitations of the system, and conclude with the examination of possibilities for future work.
17:00‑17:15	Matthias Baaz (Institute of Discrete Mathematics and Geometry, Vienna University of Technology) Stefan Hetzl (Institute of Computer Languages, Vienna University of Technology) Alexander Leitsch (Institute of Computer Languages, Vienna University of Technology) Clemens Richter (Institute of Computer Languages (E185), Vienna University of Technology) Hendrik Spohr (Institute of Computer Languages, Vienna University of Technology) System Description: The Cut-Elimination 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 constructing a set of clauses from a proof with cuts. Any resolution refutation of this set then serves as a skeleton of an LK-proof with only atomic cuts. The use of resolution and the enormous size of (formalized) mathematically relevant proofs suggest an implementation able to handle rather complex cut-elimination problems. In this paper we present an implementation of CERES: the system CERES. It already implements an improvement based on an extension of LK to the calculus LKDe containing equality rules and rules for introduction of definitions which makes it feasible to formalize and interpret mathematical proofs in LK. Furthermore it increases the efficiency of the cut-elimination method. The system CERES already performed well in handling quite large proofs.
17:15‑17:30	Boontawee Suntisrivaraporn (Dresden University of Technology) Franz Baader (TU Dresden) Carsten Lutz (Dresden University of Technology) CEL---A Short System Demonstration CEL (Classifier for EL) is a reasoner for the small description logic EL+ which can be used to compute the subsumption hierarchy induced by EL+ ontologies. The most distinguishing feature of CEL is that, unlike all other modern DL reasoners, it is based on a polynomial-time subsumption algorithm, which allows it to process very large ontologies in reasonable time. The evidence that CEL is empirically successful is its robustness and scalability, especially in the case of the Systematized Nomenclature of Medicine. With almost four hundred thousand concepts, CEL can classify it in less than half an hour, whereas most standard DL reasoners fail.

ESP - An Empirically Successful Panel (17:30‑18:30)
Chair: Geoff Sutcliffe

17:30‑18:30

Matt Kaufmann, Boris Motik, Michael Norrish, Cesare Tinelli My Top Ten Things To Do for more Empirically Successful Computerized Reasoning