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

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

  | ?- logic_list(List).

  List = [classic,intuitionistic,k,kd,kd45,s4,s42,s5] ? 
  yes

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.

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.

Intuitionistic Logic

     [~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

Modal Logics

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(...)").

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).