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)

SCAN Home
Forms: Basic Form | Correspondences Form | Circumscription Form | Help
Documentation: Theory | Computing Correspondences | Computing Circumscription | The System | Conventions | Syntax | Literature

Maintained by schmidt@cs.man.ac.uk. Last modified: 7 Nov 2000
Copyright © 1995-2000 by Max-Planck-Institut für Informatik. All rights reserved.

Imprint | Data Protection