LiU Electronic Press
Full-text not available in DiVA
Author:
Szalas, Andrzej (Linköping University, The Institute of Technology) (Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab)
Title:
Towards Incorporating Background Theories into Quantifier Elimination
Department:
Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab
Linköping University, The Institute of Technology
Publication type:
Article in journal (Refereed)
Language:
English
Publisher: Éditions Hermès-Lavoisier
Status:
Published
In:
Journal of applied non-classical logics, ISSN 1166-3081
Volume:
18
Issue:
2-3
Pages:
325-340
Year of publ.:
2008
URI:
urn:nbn:se:liu:diva-44633
Permanent link:
http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-44633
Local ID:
77213
Subject category:
Computer Science
SVEP category:
Computer science
Abstract(en) :

In the paper we present a technique for eliminating quantifiers of arbitrary order, in particular of first-order. Such a uniform treatment of the elimination problem has been problematic up to now, since techniques for eliminating first-order quantifiers do not scale up to higher-order contexts and those for eliminating higher-order quantifiers are usually based on a form of monotonicity w.r.t implication (set inclusion) and are not applicable to the first-order case. We make a shift to arbitrary relations "ordering" the underlying universe. This allows us to incorporate background theories into higher-order quantifier elimination methods which, up to now, has not been achieved. The technique we propose subsumes many other results, including the Ackermann's lemma and various forms of fixpoint approaches when the "ordering" relations are interpreted as implication and reveals the common principle behind these approaches.

Available from:
2009-10-10
Created:
2009-10-10
Last updated:
2014-06-02
Statistics:
16 hits