Introduction | Getting Started | Usage | Theory | Examples |
Operator | Semantics | Associativity |
---|---|---|
and | logical and | yfx |
or | logical or | yfx |
<=> | equivalent | xfx |
=> | implies | xfy |
~ | not | fy |
dia | modal diamond | fy |
box | modal box | fy |
:: | internal function | yfx |
^^ | internal function | xfx |
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] ? yesI.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.
Function | Argument |
---|---|
translation | relational |
semi_functional | |
functional | |
theory | full |
abbreviated | |
domain | constant |
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.
[~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 pIt is known that for any formula: F is intuitionistically valid iff [F] is S4 valid.
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).