SCAN

Basic Form

This form is the remote program execution form for basic SCAN. You can specify a quantifier elimination task, send it to a server at the Max-Planck Institute, which invokes the SCAN algorithm, computes the answer and sends the result back immediately.

Your email address (mandatory) :

Predicates to be eliminated (separated by ',') :

Functions to be eliminated (in the form f(_) or f(_,_)) :

Formula(e): in formula syntax clause syntax (default = formula syntax)
If you use clause syntax: specify with Prolog style variables (default = without)
Example: (p(a) | s) & (-p(b) | r).

General Control Parameters:
immediate Execution (default = yes)
unskolemize at end (default = yes)
negate unskolemized result (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)
maximal number of resolvents
very verbose protocol (default = no)