liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Towards Incorporating Background Theories into Quantifier Elimination
Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab.
2008 (English)In: Journal of applied non-classical logics, ISSN 1166-3081, Vol. 18, no 2-3, p. 325-340Article in journal (Refereed) Published
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.

Place, publisher, year, edition, pages
Éditions Hermès-Lavoisier , 2008. Vol. 18, no 2-3, p. 325-340
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:liu:diva-44633DOI: 10.3166/jancl.18.325-340Local ID: 77213OAI: oai:DiVA.org:liu-44633DiVA, id: diva2:265495
Available from: 2009-10-10 Created: 2009-10-10 Last updated: 2018-01-12

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Authority records

Szalas, Andrzej

Search in DiVA

By author/editor
Szalas, Andrzej
By organisation
The Institute of TechnologyKPLAB - Knowledge Processing Lab
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 154 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf