Important Convention (Prolog Variable Name Convention): The parameters in all operator definitions, which are not nested terms are always interpreted as constants. In nested parameters names starting with capital letters are interpreted as variables. Capitals that are to be interpreted as constants, they have to be enclosed in quotes.
For example
belief('John')
'John'
as constant, whereas
belief(John)
John
as variable, just like the
X
in belief(X)
.
Besides the operators listed as defaults in the operators field, a few
more are predefined (you can just cut and paste the following operator
declarations and edit its parameters).
quantifier(all,all).
quantifier(exists,exists).
quantifier(all,all,ex,->).
quantifier(exists,exists,ex,&).
box(bx,John,'R').
diamond(dia,John,'R').
John
is NOT a variable.
box(bx,belief(X),R).
diamond(dia,belief(X),R).
X
and R
are variables.
boxf(bx,app).
diamondf(dia,app).
boxf(bx,app,de).
diamondf(dia,app,de).
boxfp(bx,John,app).
diamondfp(dia,John,app).
boxfp(bx,John,app,de).
diamondfp(dia,John,app,de).
intuitionistic_implication(=>,r).
relevant_implication(=>,r).
C
:
comp(o,'C').
F
:
conv(c,'F').
id
) need not be defined as an operator. The correct
translation is implicit in the translation of any proposition, namely
u
say, is also translated according
to this scheme.
Use also the assumption:
universal(u).
r,s
):
((r o s) c) -> ((s c) o (r c))
(id o r) -> r
(r o ( -((r c) o (- s)))) -> s
until(U,F).
since(S,F).
rewrite(<=,->).
xor(xor).
ops(b,w |= b(Phi) <-> (exists u (n(w,u) & (all v (r(u,v) -> v |=
Phi))))).
with rewrite rule:
op(900,xfy,).
opr(,(A B) -> -(A <-> B)).
Conventions: If you are not sure whether the formulae can be parsed by a normal Prolog parser, enclose them in quotes.
All operator definitions may be preceded by a precedence declaration.
Some simple assumptions are predefined in the operators library. The corresponding instantiations are for example:
reflexivity(r).
symmetry(r).
transitivity(r).
ass
' function.
ass('all x y (r(x,y) <-> (s(x,y) & t(x,y)))').
r
as the intersection of s
and t
.
These two are predefined in the operators library. The corresponding instantiations are for example:
assignment_restriction(p,r).
assignment_restriction(p,r,0).
locality(p,ex)
Besides the instantiations of predefined qualifications, there is a
possibility to define new ones with the `qual
' function.
The locality qualification could for example be defined as:
qual('all w x (p(w,x) -> ex(w,x))').