 | |
Sessions
take place in auditorium 3 unless otherwise indicated.| 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. |
| 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. |
| 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. |
| 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-x2≤d, 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. |
Joint
with CAV
Room:
Lobby Room:
Restaurant Da Mario | |
![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
