A TPTP Syntax for First-Order Modal Logic

Jens Otten and Thomas Raths
University of Potsdam

Geoff Sutcliffe
University of Miami

Introduction

There are currently some efforts to compile a problem library for first-order modal logics. For this reason the TPTP syntax needs to be extended by some modal operators.

Syntax

An extension of the TPTP syntax to first-order modal logic should meet the following requirements: The standard modal logics use two unary operators for necessity and possibility. We propose the two operators "#box" and "#dia", where "#" indicates a modal operator. The BNF of the TPTP syntax needs to be extended in the following way:

<modal_operator> ::= #box | #dia
<modal_formula>  ::= <modal_operator> : <unitary_formula>
%----#box for necessarily and #dia for possibly. Syntactically, the
%----modal operator is the left operand of :, and the <unitary_formula>
%----is the right operand. Although : is a binary operator syntactically
%----it is not a <binary_connective>, and thus a <modal_formula> is a
%----<unitary_formula>.
%----Necessarily operator example: #box : ((p & p) => q).
%----Possibly operator example:    #dia : (p & p) & ~ q.
%----Modal operators have higher precedence than binary connectives, so in
%----the possibly operator example the operator applies to only (p & p).

For multi-modal logics the two operators "#box(term)" and "#dia(term)" are used, i.e. the BNF syntax is extended by

<multi_modal_operator> ::= #box(<term>) | #dia(<term>)
<multi_modal_formula>  ::= <multi_modal_operator> : <unitary_formula>

For a future extension to temporal logic, the following temporal operators could be used: "#f", "#g", "#p", and "#h".

Semantics

The standard Kripke semantics is being used.

Problem Library

A preliminary version of the QMLTP (Quantified Modal Logic Theorem Proving) library [1] is available at http://www.iltp.de/qmltp. This preliminary version uses an "old" syntax without the "#" symbol.

Conclusion

The aim of the QMLTP library is to provide a comprehensive collection of problems for first-order modal logic. For this reason the TPTP syntax needs to be extended by the standard modal operators. Once it has been agreed on a syntax, it will be used in the first official and all future releases of the QMLTP library.

Furthermore, we invite everybody to submit problems and ATP systems that use a first-order modal logic. See the web site of the QMLTP library for details.

References

[1] T. Raths and J. Otten. Building a Problem Library for First-Order Modal Logics. TABLEAUX '09. Technical Report, University of Oslo. Available at http://www.iltp.de/qmltp.