# SCAN

## Literature

### Abstracts of Publications about SCAN

In chronological order.

by **Dov M. Gabbay and Hans Jürgen Ohlbach**,
published in *Proc. of KR 92* and in the
*South African Computer Journal*, 1992.
DVI,
PostScript,
BibTeX-Entry
An algorithm is presented which eliminates second-order quantifiers over predicate variables in formulae of type
$\exists P_1 ,..., P_n\ F$ where $F$ is an arbitrary formula of
first--order predicate logic. The resulting formula is equivalent to
the original formula - if the algorithm terminates.
The algorithm can for example be applied to do interpolation, to eliminate the second--order quantifiers in circumscription,
to compute the correlations between structures and power
structures, to compute semantic properties corresponding to Hilbert
axioms in non classical logics and to compute model theoretic
semantics for new logics.

by **Chris Brink and Dov M. Gabbay and Hans Jürgen Ohlbach**,
forthcoming in a special issue.
A longer version is available as Technical Report MPI-I-93-220,
Max-Planck-Institut für Informatik, Saarbrücken,
Germany, 1993.
DVI,
PostScript,
BibTeX-Entry
Dualities between different theories occur frequently inmathematics and logic ---
between syntax and semantics of a logic, between structures and power
structures, between relations and relational algebras, to name just a few.
In this paper we show for the case of structures and power structures
how corresponding properties of the two related structures can be
computed fully automatically
by means of quantifier elimination algorithms and predicate logic
theorem provers.
We illustrate the method with a large number of examples and we give
enough technical hints to enable the reader who has access to the {\sc
Otter} theorem prover
to experiment herself.

by **Andreas Herzig**,
Technical Report MPI-I-96-2-007,
Max-Planck-Institut für Informatik,
Saarbrücken, September 1996.
PostScript,
BibTeX-Entry
The SCAN algorithm has been proposed for second order quantifier
elimination.
In particular it can be applied to find correspondence axioms for
systems of
modal logic.
Up to now, what has been studied are systems with unary modal operators. 17
In this paper we study how SCAN can be applied to various systems
of conditional
logic, which are logical systems with binary modal operators.

by **Hans Jürgen Ohlbach**.
In McRobbie, M. A. and Slaney, J. K. (eds.),
*Automated Deduction: CADE-13*.
Lecture Notes in Artificial Intelligence **1104**, Springer, 161-165, 1996.
HDVI,
PostScript,
BibTeX-Entry
by **Thorsten Engel**.
Diplomarbeit, Fachbereich Informatik, Univ. des Saarlandes,
Saarbrücken, October 1996.
HDVI,
PostScript,
BibTeX-Entry
by **J.-P. Bodeveix and M. Filali**.
Technical Report IRIT-97-44-R, Institut de Recherche en Informatique de
Toulouse, October 1997.
PostScript

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