A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae

Schmidt, R. A. and Hustadt, U. (2004)

Preprint Series CSPP-22, University of Manchester, UK. BiBTeX, Postscript, SpringerLink.

In this paper we present a translation principle, called the axiomatic translation, for reducing propositional modal logics with background theories, including triangular properties such as transitivity, Euclideanness and functionality, to decidable fragments of first-order logic. The goal of the axiomatic translation principle is to find simplified theories, which capture the inference problems in the original theory, but in a way that is more amenable to automation and easier to deal with by existing (first-order) theorem provers. The principle of the axiomatic translation is conceptually very simple and can be largely automated. Soundness is automatic under reasonable assumptions, and termination of ordered resolution is easily achieved; the non-trivial part of the approach is proving completeness.

The short version of this paper appears in Baader, F. (ed.), Automated Deduction CADE-19. Lecture Notes in Artificial Intelligence 2741, Springer.
Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 26 May 06
Copyright © 2004 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk