SCAN

Quantifier Elimination for Second-Order Predicate Logic

• Introduction
• WWW Interface Forms
• Help
• Documentation and Literature
• Authors

Introduction

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

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

• Basic Form: Remote program execution for basic SCAN.
• Correspondences Form: Remote program execution for computing correspondences.
• Circumscription Form: Remote program execution for computing first-order circumscription.

Help

Documentation and Literature

• The Theory
• Computing Correspondences
• Computing Circumscription
• The System
• Conventions and Notation
• Syntax of Formulae
• Literature

Authors

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.