Methods for Modalities 1
Institute for Logic, Language and Computation, University of Amsterdam, May 6-7, 1999
Invited Talks
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.

Methods for Modalities
Contact address

Henry Chinaski Productions 1999