|
- Thursday, May 6, 09:30-10:45
- David Basin, Verification
Based on Monadic Logic
Logic offers the possibility of modeling and reasoning about hardware and
software systems. But which logic? We propose monadic logics of strings
and trees as good candidates for many kinds of discrete systems. These
logics are natural, decidable, yet substantially more expressive,
extensions of Boolean logic. We motivate their applicability through
examples and report on experience with a verification tool based on the
WS2S (the weak second-order monadic theory of two successors) , which
implements validity checking/counter-model generation based on a reduction
of formulas to canonical automata.
- Thursday, May 6, 11:00-12:15
- Renate Schmidt, Using
Resolution for Testing Modal Satisfiability and Building Models
There are a variety of automated reasoning approaches for modal logics. An
approach which this talk will focus on is resolution via translation to
first-order logic. The approach offers much more than just another
inference calculus. Indeed, as I will illustrate, resolution provides a
very general and powerful framework for developing practical inference
methods for very expressive logics, and also for studying other issues such
as decidability, the finite model property, the automatic generation of
models, and the characterisation of models. In this talk I will
concentrate on extended modal logics, different translation methods,
different refinement strategies for obtaining decision procedures, and ways
of generating models.
- Thursday, May 6, 16:15-17:30
- Patrick Blackburn,
Internalizing Labelled Deduction
In this talk I am going to discuss labelled deduction, but from a somewhat
unusual perspective. Instead of viewing labelled deduction as the process
of manipulating modal formulas with the help of a labelling algebra, I want
to discuss what happens when the modal object language is enriched so that
it contains labels as first class citizens. The resulting language is
called the {\it basic hybrid language\/}, and as I shall show, it provides
a setting for modal deduction in which labelling discipline emerges as
logic. For the most part this talk will be an example-driven introduction
to the method, but I also want to indicate the relevance of other recent
work on hybrid languages.
- Friday, May 7, 09:00-10:15
- Ian Horrocks, Tableaux
Algorithms and Implementations
Reasoning in propositional modal logics is inherently intractable: even for
K, deciding the satisfiability of a single formula is in PSpace, while
satisfiability with respect to a theory (a set of axioms) is already in
ExpTime. In spite of this, implementations of tableaux algorithms, even for
logics significantly more expressive than K, have proved effective in
realistic applications. This has been achieved by a careful choice of
logical language (avoiding, for example, the transitive closure operator),
and the use of a range of optimisation techniques in the implementation.
This talk will briefly introduce Description Logics (DLs) as notational
variants of propositional modal logics, and discuss how studies of DLs and
DL applications have both influenced the choice of language and suggested
ideas for optimisation techniques. We will then see how the choice of
logical language facilitates optimised implementation and study in more
detail some optimisation techniques that have proved particularly
effective.
- Friday, May 7, 11:15-12:30
- Hans de Nivelle, Resolution Implementations
We explain the most important design decisions that were made during
the implementation of the theorem prover Bliksem.
Bliksem is a first order, resolution based theorem prover. One of
its design objectives was to efficiently implement resolution based
decision procedures.
First, we discuss the problem of how to internally represent terms,
and formulae. We present 5 different ways of representing terms.
Benchmarks indicate that the differences are significant.
The fastest is what we call the 'prefix with end' representation.
Second, we consider the problem of how to implement substitutions.
Here again the difference between good and bad implementation is
quite large.
The third problem that we consider is the question of how to implement
the simplification operations subsumption, demodulation, unit-resolution.
The question of how to implement them cannot be separated from
the theoretical question up to what level, and when, these simplifications
should be made.
This problem is particularly important for theorem proving in the
context of modal logics, since the termination behaviour may depend
on simplification.
- Friday, May 7, 16:00-17:15
- Roberto Sebastiani, Evaluating the Efficiency of Decision Procedures for Modal Logics
Five years ago we started testing extensively the performances of modal
theorem provers.
Since then, extensive empirical testing has been playing a key role in
stimulating and
guiding the development of increasingly faster procedures.
In this talk I will try to summarize this five-year experience in empirical
testing.
I will present a brief summary of the main testing methodologies, describing
the main ideas and goals; in particular, I'll focus on those methods based
on randomly generated
formulas. I'll discuss some efficiency issues suggested by the empirical
results,
and outline some lessons learned about empirical testing itself.
|
|
