LiU Electronic Press
Full-text not available in DiVA
Author:
Orlowska, Ewa (Institute of Telecommunications Warsaw University)
Szalas, Andrzej (Linköping University, The Institute of Technology) (Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab)
Title:
Quantifier Elimination in Elementary Set Theory
Department:
Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab
Linköping University, The Institute of Technology
Publication type:
Conference paper (Refereed)
Language:
English
In:
Proceedings of the 8th International Conference on Relational Methods in Computer Science (RelMiCS)
Editor:
W. MacCaull, I. Duentsch, M. Winter
Publisher: Springer Berlin/Heidelberg
Series:
Lecture Notes in Computer Science, ISSN 0302-9743; 3929
Pages:
237-248
Year of publ.:
2006
URI:
urn:nbn:se:liu:diva-31858
Permanent link:
http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-31858
Local ID:
17685
Subject category:
Computer Science
SVEP category:
Computer science
Abstract(en) :

In the current paper we provide two methods for quantifier elimination applicable to a large class of formulas of the elementary set theory. The first one adapts the Ackermann method [1] and the second one adapts the fixpoint method of [20]. We show applications of the proposed techniques in the theory of correspondence between modal logics and elementary set theory. The proposed techniques can also be applied in an automated generation of proof rules based on the semantic-based translation of axioms of a given logic into the elementary set theory.

Available from:
2009-10-09
Created:
2009-10-09
Last updated:
2012-02-13
Statistics:
21 hits