SCAN
Quantifier Elimination for Second-Order Predicate Logic
SCAN is an implementation of the algorithm with the same name that was
introduced in Gabbay and Ohlbach (1992).
The algorithm attempts to eliminate second-order quantifiers, that is,
quantifiers over predicate symbols, thereby reducing a second-order formula to
its first-order equivalent.
There are many areas in which SCAN can be applied and is being applied,
for example, for
- automating correspondence theory in non-classical
logics including
modal logic, arrow logic,
temporal logic, relevance logic and
intuitionistic logic.
- computing first-order circumscription
- theorem proving in set theory
- ...
The program may be executed remotely via different WWW
interface forms tailored for specific applications.
If you are a first time user please read the
regulations for remote program execution.
For convience each page has a `toolbar'
at the bottom with links to the most important pages.
These are the forms, the help page and the documentation pages.
SCAN has received a positive review by
Vladimir Lifschitz on the
Page of Positive
Reviews of Research in Logical AI.
This page includes explanations and examples from different application areas.
This page lists the contributors to the development of the SCAN tool and its
website.
- Hans Jürgen Ohlbach
- Department of Computer Science,
King's College,
Strand, London, WC2R 2LS.
- E-mail:
ohlbach@dcs.kcl.ac.uk.
- Thorsten Engel
- MPI für Informatik,
Im Stadtwald, 66123 Saarbrücken, Germany.
- Renate A. Schmidt
- Centre for Agent Research and
Development,
Department of Computing and
Mathematics,
Manchester Metropolitan University
Chester St., Manchester M1 5GD, UK.
- E-mail:
R.A.Schmidt@doc.mmu.ac.uk
- Dov M. Gabbay
- Department of Computer Science,
King's College,
Strand, London, WC2R 2LS.
- E-mail:
dg@dcs.kcl.ac.uk.
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: 05 Aug 13