The Optimised Functional Translation and Graded Modal Logics

Hans Jürgen Ohlbach Renate A. Schmidt^{∗}

Max-Planck-Institut für Informatik, Im Stadtwald 66123 Saarbrücken, Germany

July 1995

We investigate and develop predicate logic methods, in particular, resolution methods for automating modal deduction. An important ingredient of our work is the transformation of modal formulae and theories into adequate clausal formulation and suitably refined resolution calculi that provide for decidable logics practical decision procedures. Here, we focus on the transformation from normal modal logics to clause form and present a non-trivial encoding of a modal logic of numerical quantifiers. To a large extent the transformation procedures are automated.

We use an optimised version of the functional transformation technique (Ohlbach and Schmidt 1995). The functional transformation of Ohlbach (1988) captures accessibility in modal frames not like the relational transformation by binary relations but by sets of functions mapping worlds to accessible worlds. The optimised functional transformation captures accessibility by maximal sets of transition functions. It has the advantage that functional quantifiers may be permuted arbitrarily. In general, the formula obtained by moving an existential quantifier outward over a universal quantifier is weaker than the original formula. In functional frames the resulting formula is equivalent to the original formula. Moving existential quantifiers to the front eliminates complex Skolem terms other than Skolem constants in the clause form. The optimised functional translation yields for modal formulae a set of clauses over unary predicates, Skolem constants and one designated functional symbol for functional application. Initially, modal theories translate to second-order formulae to which we apply the quantifier elimination algorithm of Gabbay and Ohlbach (1992) in an attempt to find their first-order equivalents. For these, we then devise special resolution refinements that capture the modal theory. The functional and also the optimised functional translation methods are sound and complete for first-order definable normal multi-modal logics.

Numerical modal quantifiers are modal operators indexed with non-negative integer values and are called graded modalities as they express ‘grades of truth’, like φ is true in more than n (at most n, less than n, at least n or exactly n) accessible worlds.

∗Combined abstract of talks held at the RelMiCs’96 Workshop in Parati, Brasil, 10–14 July.

We cannot directly apply the functional transformation to graded modal logics because they are not standard multi-modal logics. However, graded modal logics can be embedded in a multi-modal logic and via this intermediary logic reduce to theories of clauses and equations (Ohlbach, Schmidt and Hustadt 1995a,b).

Compared with existing calculi, our calculus has advantages and disadvantages. For example, the tableaux method is a popular decision procedure used also in the area of knowledge representation. Reasoning by the tableaux method is facilitated by the generation and manipulation of constants and leads to the consideration of combinatorially many case distinctions. The advantage of our approach is, instead of processing constants we can reason with sets and their cardinalities. In many cases the length of proofs for theorems of our calculus is independent of the cardinalities. The disadvantage of our calculus is, that it requires complex equational reasoning and the realisation will not be easy. Because the original logic of graded modalities is decidable we hope to find a resolution strategy that ensures termination yielding a resolution decision procedure.

Gabbay, D. M. and Ohlbach, H. J. (1992), Quantifier elimination in second-order predicate logic, South African Computer Journal 7, 35–43. Also in Proc. of KR‘92, 425–436.

Ohlbach, H. J. (1988), A Resolution Calculus for Modal Logics, PhD thesis, Univ. Kaiserslautern, Germany.

Ohlbach, H. J. and Schmidt, R. A. (1995), Functional translation and second-order frame properties of modal logics, Technical Report MPI-I-95-2-002, Max-Planck-Institut für Informatik, Saarbrücken, Germany. Submitted for publication.

Ohlbach, H. J., Schmidt, R. A. and Hustadt, U. (1995a), Translating graded modalities into predicate logic, in H. Wansing (ed.), Proof Theory of Modal Logic, Studies in Applied Logic Series, Kluwer, chapter 14, 245–285.

Ohlbach, H. J. and Schmidt, R. A. and Hustadt, U. (1995b), Symbolic Arithmetical Reasoning with Qualified Number Restrictions, Proc. of Intern. Workshop on Description Logics’95, 89–95.