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

WWW Interface Forms


This page includes explanations and examples from different application areas.

Documentation and Literature


Hans Jürgen Ohlbach
Department of Computer Science, King's College, Strand, London, WC2R 2LS.

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.

Dov M. Gabbay
Department of Computer Science, King's College, Strand, London, WC2R 2LS.

Forms: Basic Form | Correspondences Form | Circumscription Form | Help
Documentation: Theory | Computing Correspondences | Computing Circumscription | The System | Conventions | Syntax | Literature [an error occurred while processing this directive]
Maintained by Last modified: 7 Nov 2000
Copyright © 1995-2000 by Max-Planck-Institut für Informatik. All rights reserved.

Imprint | Data Protection