CADE on Saturday

Detailed program
Saturday July 27th, 2002
See also the unified by-slot program

Sessions take place in auditorium 3 unless otherwise indicated.

Session 1: Description logics and Semantic Web

09:00-10:00  Ian Horrocks, U Manchester, UK
Invited talk: Reasoning with expressive description logics: Theory and practice
Description Logics are a family of class based knowledge representation formalisms characterised by the use of various constructors to build complex classes from simpler ones, and by an emphasis on the provision of sound, complete and (empirically) tractable reasoning services. They have a wide range of applications, but their use as ontology languages has been highlighted by the recent explosion of interest in the "Semantic Web", where ontologies are set to play a key role. DAML+OIL is a description logic based ontology language specifically designed for use on the web. The logical basis of the language means that reasoning services can be provided, both to support ontology design and to make DAML+OIL described web resources more accessible to automated processes.

10:00-10:30  Guoqiang Pan, Rice U, USA
Ulrike Sattler, Dresden U of Techn., Germany
Moshe Y. Vardi, Rice U, USA
BDD-based decision procedures for K
We describe BDD-based decision procedures for K. Our approach is inspired by the automata-theoretic approach, but we avoid explicit automata construction. Our algorithms compute the fixpoint of a set of types, which are sets of formulas satisfying some consistency conditions. We use BDDs to represent and manipulate such sets. Experimental results show that our algorithms are competitive with contemporary methods using benchmarks from TANCS 98 and TANCS 2000.

Session 2: Proof-carrying code and compiler verification

11:00-11:30  Andrew Bernard, Carnegie Mellon U, USA
Peter Lee, Carnegie Mellon U, USA
Temporal logic for proof-carrying code
Proof-carrying code (PCC) is a framework for ensuring that untrusted programs are safe to install and execute. When using PCC, untrusted programs are required to contain a proof that allows the program text to be checked efficiently for safe behavior. In this paper, we lay the foundation for a potential engineering improvement to PCC. Specifically, we present a practical approach to using temporal logic to specify security policies in such a way that a PCC system can enforce them.

11:30-12:00  George C. Necula, U California-Berkeley, USA
Robert R. Schneck, U California-Berkeley, USA
A gradual approach to a more trustworthy, yet scalable, proof-carrying code
Proof-carrying code (PCC) allows a code producer to associate to a program a machine-checkable proof of its safety. In the original approach to PCC, the safety policy includes proof rules which determine how various actions are to be proved safe. These proof rules have been considered part of the trusted code base (TCB) of the PCC system. We wish to remove the proof rules from the TCB by providing a formal proof of their soundness. This makes the PCC system more secure, by reducing the TCB; it also makes the system more flexible, by allowing code producers to provide their own safety-policy proof rules, if they can guarantee their soundness. Furthermore this security and flexibility are gained without any loss in the ability to handle large programs. In this paper we discuss how to produce the necessary formal soundness theorem given a safety policy. As an application of the framework, we have used the Coq system to prove the soundness of the proof rules for a type-based safety policy for native machine code compiled from Java.

12:00-12:30  Martin Strecker, Techn. U of Munich, Germany
Formal verification of a java compiler in isabelle
This paper reports on the formal proof of correctness of a compiler from a substantial subset of Java source language to Java bytecode in the proof environment Isabelle. This work is based on extensive previous formalizations of Java, which comprise all relevant features of object-orientation. We place particular emphasis on describing the effects of design decisions in these formalizations on the compiler correctness proof.

Session 3: Non-classical logics

14:00-14:30  Uwe Egly, Vienna U of Techn., Austria
Embedding lax logic into intuitionistic logic
Lax logic is obtained from intuitionistic logic by adding a single modality () which captures properties of necessity and possibility. This modality was considered by Curry in two papers from 1952 and 1957 and rediscovered recently in different contexts like verification of circuits and the computational λ-calculus. We show that lax logic can be faithfully embedded into the underlying intuitionistic logic and discuss (computational) properties of the embedding. Using the proposed polynomial-time computable embedding, PSPACE-completeness of the provability problem of propositional lax logic is shown.

14:30-15:00  Dominique Larchey-Wendling, LORIA Nancy, France
Combining proof-search and counter-model construction for deciding Gödel-Dummett logic
We present an algorithm for deciding Gödel-Dummett logic. The originality of this algorithm comes from the combination of proof-search in sequent calculus, which reduces a sequent to a set of pseudo-atomic sequents, and counter-model construction of such pseudo-atomic sequents by a fixpoint computation. From an analysis of this construction, we deduce a new logical rule which provides shorter proofs than the corresponding rule of G4-LC. We also present a linear implementation of the counter-model generation algorithm for pseudo-atomic sequents.

15:00-15:30  Didier Galmiche, LORIA Nancy, France
Daniel Mery, LORIA Nancy, France
Connection-based proof search in propositional BI logic
We present a connection-based characterization of propositional BI (logic of bunched implications), a logic combining linear and intuitionistic connectives. This logic, with its sharing interpretation, has been recently used to reason about mutable data structures and needs proof search methods. Our connection-based characterization for BI, is based on standard notions but involves, in a specific way, labels and constraints in order to capture the interactions between connectives during the proof-search. As BI is conservative w.r.t. intuitionistic logic and multiplicative intuitionistic linear logic, we deduce, by some restrictions, new connection-based characterizations and methods for both logics.

Session 4: System descriptions

16:00-16:15  Jesper Møller, IT U of Copenhagen, Denmark
System description: DDDLIB: A library for solving quantified difference inequalities
DDDLIB is a library for manipulating formulae in a first-order logic over Boolean variables and inequalities of the form x1-x2d, where x1,x2 are real variables and d is an integer constant. Formulae are represented in a semi-canonical data structure called difference decision diagrams (DDDs) which provide efficient algorithms for constructing formulae with the standard Boolean operators (conjunction, disjunction, negation, etc.), eliminating quantifiers, and deciding functional properties (satisfiability, validity and equivalence). The library is written in C and has interfaces for C++, Standard ML and Objective Caml.

16:15-16:30  Joe Hurd, U Cambridge, UK
System description: An LCF-style interface between HOL and first-order logic
Performing interactive proof in the HOL theorem prover involves reducing goals to simpler subgoals. It turns out that many of these subgoals can be efficiently `finished off' by an automatic first-order prover. Given this level of demand for automatic first-order proof by users performing interactive proof in HOL, it seems worthwhile to look for ways to narrow the gap between these two worlds.

16:30-16:45  Michael Kohlhase, Carnegie Mellon U, USA
Jürgen Zimmer, Saarland U, Germany
System description: System description: The MathWeb software bus for distributed mathmatical reasoning
This system description summarizes the development of MathWeb in the last three years. We further extended the list of reasoning systems integrated in the MathWeb-SB, stabilized existing integrations and explored new application domains for the MathWeb-SB. The main improvements are a more flexible architecture and increased standards support in the communication protocols used in MathWeb-SB. As a consequence, it is much simpler now to use and integrate mathematical services into the MathWeb-SB.

16:45-17:00  Jörg Siekmann, Saarland U, Germany
et al.
System description: Proof development with OMEGA
OMEGA is a mathematical assistant tool that supports proof development in mathematical domains at a user-friendly level of abstraction. It is a modular system with a central data structure and several complementary subsystems. OMEGA has many characteristics in common with systems like NUPRL, COQ, HOL, and PVS. However, it differs from these systems with respect to its focus on proof planning. We present an overview of the architecture of the OMEGA system and sketch some of its novel features. Special features of OMEGA include (1) facilities to access a considerable number of different reasoning systems and to integrate their results into a single proof structure, (2) support for interactive proof development through some non-standard inspection facilities and guidance in the search for a proof, and (3) methods to develop proofs at a knowledge-based level.

17:00-17:15  Mateja Jamnik, U Cambridge, UK
Manfred Kerber, U Birmingham, UK
Martin Pollet, Saarland U, Germany
System description: LearnOmatic: System description
We devised a framework within which a proof planning system can learn frequently occurring patterns of reasoning automatically from a number of typical examples, and then use them in proving new theorems. The availability of such patterns, captured as proof methods in a proof planning system, reduces search and proof length. We implemented this learning framework for the proof planner OMEGA, and present it in this paper - we call our system LearnOmatic.

17:15-17:30  Carlos E. Areces, U Amsterdam, The Netherlands
Juan Heguiabehere, U Amsterdam, The Netherlands
System description: HyLoRes 1.0: Direct resolution for hybrid logics
HLR is a direct resolution prover for hybrid logics. The most interesting distinguishing feature of HLR is that it is not based on tableau algorithms but on (direct) resolution. HLR implements a version of the "given clause" algorithm, which has become the skeleton underlying most first-order provers. In contrast to translation based provers like MSPASS, HLR performs resolution directly on the modal (or hybrid) input, with no translation into background logics. It is often said that hybrid logics combine interesting features from both modal and first-order logics. In the same spirit, HLR fuses ideas from state-of-the-art first-order proving with the simple representation of the hybrid object language.

17:30-19:00  Welcome reception

Joint with CAV
Room: Lobby

19:30-21:00  CASC dinner

Room: Restaurant Da Mario