SCAN

Examples, Explanations and Help

The Email Address Field
Operators
Assumptions
Predicate Qualifications

The Email Address Field

Please supply your full email address. Without your email address your job will not be executed. If the limits on the computation resources are relaxed for you, your email address serves as an identifier.

Operators

The `operators' field in the correspondence theory form is for specifying operators, either by instantiating predefined operators from the operators library or by specifying the operators direclty.

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

as parameter of a parametrized modal operator interprets 'John' as constant, whereas


belief(John)

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

Quantifiers with constant-domain assumption

Universal and existential quantification:: quantifier(all,all).; quantifier(exists,exists).

Quantifiers with varying-domain assumption

quantifier(all,all,ex,->).

quantifier(exists,exists,ex,&).

Parameterized modal operators

box(bx,John,'R').

diamond(dia,John,'R').

Note the parameters are fixed, John is NOT a variable.

box(bx,belief(X),R).

diamond(dia,belief(X),R).

Here, X and R are variables.

Modal operators with functional semantics

The serial case, i.e. above KD.: boxf(bx,app).; diamondf(dia,app).
The non-serial case, i.e. above K.: boxf(bx,app,de).; diamondf(dia,app,de).
Parameterized and serial: boxfp(bx,John,app).; diamondfp(dia,John,app).
Parameterized and non-serial: boxfp(bx,John,app,de).; diamondfp(dia,John,app,de).

Weaker implications

intuitionistic_implication(=>,r).

relevant_implication(=>,r).

Arrow logic operators

Composition is a binary infix operator defined by a ternary relation C:: comp(o,'C').
Converse is an unary postfix operator defined by a binary relation F:: conv(c,'F').

The identity (id) need not be defined as an operator. The correct translation is implicit in the translation of any proposition, namely

w |= (id) <-> id(w)

The universal relation, u say, is also translated according to this scheme. Use also the assumption:

universal(u).

Try computing the correspondence properties for (eliminate r,s):

((r o s) c) -> ((s c) o (r c))

(id o r) -> r

(r o ( -((r c) o (- s)))) -> s

Temporal logic operators

until(U,F).

since(S,F).

Miscellaneous

Backward implication can be defined by:: rewrite(<=,->).
exclusive-or, by:: xor(xor).

Operators which are not predefined can be defined as in the following examples:

with semantics definition:

ops(b,w |= b(Phi) <-> (exists u (n(w,u) & (all v (r(u,v) -> v |=
Phi))))).

(modal operator with a kind of strong neighbourhood semantics).

with rewrite rule:

op(900,xfy,).

opr(,(A B) -> -(A <-> B)).

(Antivalence)

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.

Assumptions

Sometimes correspondences are computed in a certain background theory. For example the accessibility relation in intuitionistic logic is always reflexive and transitive. This information may be exploited for simplifying the output of SCAN. Moreover, it might be necessary for stopping infinite, but redundant resolution loops. This is in fact the case for intuitionistic logic. The assignment restriction for intuitionistic logic causes SCAN to loop, and this can only be stopped by exploiting the transitivity of the accessibility relation.

Some simple assumptions are predefined in the operators library. The corresponding instantiations are for example:

reflexivity(r).

symmetry(r).

transitivity(r).

Besides the instantiations of predefined assumptions, there is a possibility to define new ones with the `ass' function.

ass('all x y (r(x,y) <-> (s(x,y) & t(x,y)))').

for example defines r as the intersection of s and t.

Predicate Qualifications

An example for predicate qualifications are assignment restrictions which are necessary in logics below normal propositional logic, in particular in relevance logic and in intuitionistic logic.

These two are predefined in the operators library. The corresponding instantiations are for example:

intutionistic logic: assignment_restriction(p,r).
relevance logic: assignment_restriction(p,r,0).

Another predefined predicate qualification is

locality(p,ex)

which specifies in a varying-domain modal logic context that a predicate holds only in the actual world's domain.

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