Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
A New Fast Tableau-Based Decision Procedure for an Unquantified Fragment of Set Theory
| |
|
A New Fast Tableau-Based Decision Procedure for an Unquantified Fragment of Set Theory
Domenico Cantone3  and Calogero G. Zarba4
| (3) |
Dipartimento di Matematica, Università di Catania, Viale A. Doria 6, I-95125 Catania, Italy |
| (4) |
Computer Science Department, Stanford University, Gates Building, Stanford, CA 94305, USA |
Abstract
In this paper we present a new fast tableau-based decision procedure for the ground set-theoretic fragment Multi-Level Syllogistic
with Singleton (in short MLSS) which avoids the interleaving of model checking steps.
The underlying tableau calculus is based upon the system KE.
Work partially supported by the C.N.R. of Italy, coordinated project SETA, by M.U.R.S.T. Project “Tecniche speciali per la
specifica, l’analisi, la verifica, la sintesi e la trasformazione di programmi”, and by project “Deduction in Set Theory:
A Tool for Software Verification” under the 1998 Vigoni Program.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|