SCAN

Correspondences Form

This form is the remote program execution form for computing correspondences. You can specify a correspondence theory problem, send it to a server at the Max-Planck Institute, which invokes the SCAN algorithm, computes the answer and sends the result back to you immediately.

Your email address (mandatory) :

Truth Condition (Default = all: the formula must be true in all worlds) :

Operators : Examples | Operator Library

Predicates to be eliminated (separated by ',')

Formula to be translated, for example: b(p) -> b(b(p)).

Assumption(s) : E.g. transitivity(r). (usually not necessary) Help

Qualification(s) : E.g. assignment_restriction(p,r). (usually not nec.) Help

Rewrite system : E.g. ml0_nnf(-,&,'|',->,<->,b,d). (usually not nec.)

General Control Parameters
print resolvents (default = no)
seconds maximal CPU time (maximum: 10)
seconds for checking redundancy of resolvents (1 should do)
seconds for minimizing result (per clause) (1 should do)
negation sign (e.g. -), provided you want the original formulation to be negated, not the translated formulation (default = do not negate first, negate the translated formulation)