Creating SATURATE Input Files
From (Non-)Classical Logic Formulae


Introduction Getting Started Usage Theory Examples


Introduction

The purpose of this program is twofold: First, it provides us with a means to translate modal and intuitionistic formulae into classical first-order predicate logic, and, second, it generates the clause normal form of arbitrary first-order predicate logic formulae. It is meant to serve as a preprocessor for the SATURATE theorem prover.


Getting started

"translate" defines some logical operators as listed in the following table.

OperatorSemanticsAssociativity
andlogical andyfx
orlogical oryfx
<=>equivalentxfx
=>impliesxfy
~notfy
diamodal diamondfy
boxmodal boxfy
::internal functionyfx
^^internal functionxfx

Moreover, the predicates "logic_list/1", "translate/0", "translate/6", and "make_file/4", are provided (see explanation below).


Usage

The predicate logic_list(X) shows which logics are currently available. The value of X might change in different versions of this translator. Quite typical is the following:
  | ?- logic_list(List).

  List = [classic,intuitionistic,k,kd,kd45,s4,s42,s5] ? 
  yes
I.e. this version allows us to create SATURATE files from (first-order) formulae of classical predicate logic, intuitionistic logic, and the modal logics K, KD, KD45, S4, S4.2, and S5 (this list might be extended, however).

The purpose of "translate/0" is to briefly inform the user about the usage of the predicate "translate/6" (a short description of the respective arguments).

"translate/6" expects a formula as its first argument, a logic name (as provided by "logic_list/1" above), and a list of options as second and third argument respectively. All these three arguments are mandatory, i.e. they are not allowed to be variables (this means that if there are no special options to be mentioned, the third argument has to be the empty list rather than an anonymous variable). If some options are required but none are mentioned then certain default values take place.
The final three arguments contain the result of the procedure. This result consists of a list of skolem symbols introduced by the translation (in the form "skolems([f,g,h])"), a list of theory clauses and a list of theorem clauses. In case of classical logic there are no theory clauses. Otherwise, the translation of non-classical formulae into predicate logic induces a certain theory which is reflected by these theory clauses. This holds also in case of intuitionistic logic since formulae of this logic are first translated into formulae of the modal logic S4.
The "theorem clauses", as probably expected, contain the result obtained from the input formula (the theorem) after negating, translating into predicate logic (in the non-classical case) and transforming into clause normal form.
For the average user this predicate is of importance only in combination with "make_file/4" (see below).

In case the user is interested in saturating modal logic background theories rather than in proving theorems there is a possibility to call "translate" with the ground term "none" as its first argument. The translator then provides with the background theory of the modal logic specified in the option list in the list of theory clauses.

Formulae are built according to the following rules:

	FORMULA	= ATOM | FORMULA and FORMULA | FORMULA or FORMULA |
		  FORMULA => FORMULA | FORMULA <=> FORMULA | ~ FORMULA |
		  exists(VARIABLE,FORMULA) | all(VARIABLE,FORMULA) |
		  box FORMULA | dia FORMULA
	ATOM	= anything, e.g. q(x,f(Y)) (no capital letters as predicate names)
	VARIABLE= anything (small or capital letters)

The Option list (the third argument of "translate/6") contains informations about the kind of translation that is to be used, how the background theory is to be described and, in the first-order case, what kind of domain restrictions are to be assumed. The following possibilities are available up to now.

FunctionArgument
translationrelational
semi_functional
functional
theoryfull
abbreviated
domainconstant
increasing
decreasing
varying

Thus a usual Option list looks like this:

  [translation(semi_functional),theory(abbreviated),domain(constant)]

As mentioned above, "translate/6" is usually to be used in combination with "make_file/4".
"make_file/4" expects a file name as its first argument, a list of skolem symbols as its second argument, a list of theory clauses and a list of theorem clauses as third and fourth argument respectively. However, the skolem symbols and the two clause lists can easily be obtained from a call to "translate/6", thus the two predicates can easily be combined.


Theory

There is not very much to be said about the clause normal form transformation. This is essentially done in the usual naïve way.

Intuitionistic Logic

We are dealing with intuitionistic logic by first translating into the modal logik S4 and then translating the S4 formulae into classical logic.
The translation into S4 works as follows:
     [~a]      = box ~[a]
     [a => b]  = box([a] => [b])
     [a <=> b] = box([a] <=> [b])
     [a and b] = [a] and [b]
     [a or b]  = [a] or [b]
     [p]       = box p    for atomic p
It is known that for any formula: F is intuitionistically valid iff [F] is S4 valid.

Modal Logics

The relational translation is the one based on the usual Kripke-style semantics.
For more information concerning the functional translation have a look at the report MPI-I-93-225.dvi.Z.
Information about the semi-functional translation can be obtained e.g. from MPI-I-92-228.dvi.Z., or from this PhD thesis.

In case of the semi-functional translation there exists a possibility to saturate the background theory which is induced by the logic under consideration. In general this saturation is much simpler than the original theory. We distinguish the two possibilities (by "theory(full)" and "theory(abbreviated)" respectively) in the Option list.

In first-order modal logics it has to be clarified whether the domains of worlds are constant, increasing, decreasing or arbitrarily varying with respect to the accessibility relation. Again this is to be specified in the Option list (by "domain(...)").


Examples

We simplified the output slightly for readability.

Example 1

   | ?- translate(all(x,exists(y,p(x,y)) <=> exists(z,p(x,z))),classic,[],X,Y,Z),
        make_file(test,X,Y,Z).

produces the following output (in file "test"):

   %   Skolemsymbols:  [a,b,c].

   %   Theorem clauses:

   p(a,b),p(a,c).
   p(a,D),p(a,E) -> [].

Example 2

   |? - translate(dia p => box dia p,kd45,
                  [translation(semi_functional),theory(abbreviated)],
                  X,Y,Z),
        make_file('another.test',X,Y,Z).

produces the following output (in file "another.test"):

   %   Skolemsymbols:  [o,a,b].

   %   Theory clauses:

   'R'(A,B::C).
   'Normal'(D).

   %   Theorem clauses:

   'Normal'(o).
   p(o::a).
   'R'(o::b,G),p(G) -> [].

Example 3

   |? - translate(none,kd45,
                  [translation(functional)],
                  A,B,C),
        make_file('third.test',A,B,C).

produces the following output (in file "third.test"):
 
   %   Skolemsymbols:  [o,f,g].
    
   %   Theory clauses:
    
   'R'(A,A::B).
   'R'(C,D),'R'(D,E) -> C::f(E,D,C) = E.
   'R'(G,H),'R'(G,I) -> H::g(I,H,G) = I.
   'Normal'(K).

Andreas Nonnengart
Last modified: Wed Nov 6 15:13:25 MET
Imprint | Data Protection