Topic: Automated Theorem Proving

During the last years we have developped three main approaches to theorem proving for non-classical logics.

1. We have extended the resolution principle to modal logics. The main difficulty in this approach is the non-existence of simple clausal normal forms for modal logics. This has led to the definition of a non-classical logic programming language MOLOG.

2. We have studied in depth methods of translation. they can be divided into two:
   The first one consists in translating a modal logic in a first-order equational theory. This permits to re-use much of the work done in the domain of equality handling. This approach is particularly attractive for first-order modal logics.
   The second one consists in translating a given modal logic into another one, which should be simpler and for which an automated deduction method exists. In this way we have defined translations from the modal logic of provability into K4, and from the family of non-normal modal logics (classical, monotonic, and regular modal logics, as well as Humberstone's inaccessible worlds logic) into multi-modal logics of the Sahlqvist family, for which proof methods exist (tableaux, resolution, or translation into classical logic).
   The study of these methods has been supported by the ESPRIT Basic Research Actions ``Mechanizing Deduction in the Logics of Practical Reasoning'' (MEDLAR I, MEDLAR II).

3. We have recently started to investigate tableau methods. This interest has been motivated by our research topic of reasoning about actions. We have started by defining a tableau procedure for dynamic logic-like logics of actions within which a notion of dependence has been integrated.

   Our approach allows to define tableau calculi in a modular way, with completeness proofs that are much simpler than that of the literature. We have in particular studied modal logics which are most difficult for the standard procedures, such as those with a dense or confluent accessibility relation. We are currently developping a general tableau theorem prover.

A related research topic of ours is proof theory and foundations of modal and conditional logics.

WWW links

• two web-based theorem provers for modal logics
  • The Logics Workbench (LWB) by Gerhard Jäger's group at University of Bern
  • SCAN by Hans Jürgen Ohlbach's former group at MPII Saarbrücken
• a survey on other modal theorem provers by Renate Schmidt at Manchester Metropolitan University.
• first-order logic theorem provers
  • OTTER (resolution method; by B. McCune and others)
  • LeanTAP (semantic tableaux; by B. Beckert and J. Possegga, University of Karlsruhe).
• other automated deduction systems
  • directory at Argonne Labs (higher-order, first-order)
  • directory at Stanford (higher-order, first-order)
  • AI Planning systems.

last update: june 1999