Deciding polynomial-exponential problems

Melanie Achatz; Scott McCallum; Volker Weispfenning

doi:10.1145/1390768.1390799

Deciding polynomial-exponential problems

Melanie Achatz^*, Scott McCallum, Volker Weispfenning

^*Corresponding author for this work

School of Computing

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

32 Citations (Scopus)

Abstract

This paper presents a decision procedure for a certain class of sentences of first order logic involving integral polynomials and the exponential function in which the variables range over the real numbers. The inputs to the decision procedure are prenex sentences in which only the outermost quantified variable can occur in the exponential function. The decision procedure has been implemented in the computer logic system REDLOG. Closely related work is reported in [2, 7, 16, 20, 24].

Original language	English
Title of host publication	ISSAC'08: Proceedings of the 21st International Symposium on Symbolic and Algebraic Computation 2008
Editors	David Jeffrey
Place of Publication	New York
Publisher	Association for Computing Machinery
Pages	215-222
Number of pages	8
ISBN (Print)	9781595939043
DOIs	https://doi.org/10.1145/1390768.1390799
Publication status	Published - 2008
Event	21st Annual Meeting of the International Symposium on Symbolic Computation, ISSAC 2008 - Linz, Hagenberg, Austria Duration: 20 Jul 2008 → 23 Jul 2008

Other

Other	21st Annual Meeting of the International Symposium on Symbolic Computation, ISSAC 2008
Country/Territory	Austria
City	Linz, Hagenberg
Period	20/07/08 → 23/07/08

Access to Document

10.1145/1390768.1390799

Cite this

@inproceedings{11ff1eae8fc04ea997c70a2cdd5e886b,

title = "Deciding polynomial-exponential problems",

abstract = "This paper presents a decision procedure for a certain class of sentences of first order logic involving integral polynomials and the exponential function in which the variables range over the real numbers. The inputs to the decision procedure are prenex sentences in which only the outermost quantified variable can occur in the exponential function. The decision procedure has been implemented in the computer logic system REDLOG. Closely related work is reported in [2, 7, 16, 20, 24].",

author = "Melanie Achatz and Scott McCallum and Volker Weispfenning",

year = "2008",

doi = "10.1145/1390768.1390799",

language = "English",

isbn = "9781595939043",

pages = "215--222",

editor = "David Jeffrey",

booktitle = "ISSAC'08: Proceedings of the 21st International Symposium on Symbolic and Algebraic Computation 2008",

publisher = "Association for Computing Machinery",

note = "21st Annual Meeting of the International Symposium on Symbolic Computation, ISSAC 2008 ; Conference date: 20-07-2008 Through 23-07-2008",

}

Achatz, M, McCallum, S & Weispfenning, V 2008, Deciding polynomial-exponential problems. in D Jeffrey (ed.), ISSAC'08: Proceedings of the 21st International Symposium on Symbolic and Algebraic Computation 2008. Association for Computing Machinery, New York, pp. 215-222, 21st Annual Meeting of the International Symposium on Symbolic Computation, ISSAC 2008, Linz, Hagenberg, Austria, 20/07/08. https://doi.org/10.1145/1390768.1390799

Deciding polynomial-exponential problems. / Achatz, Melanie; McCallum, Scott; Weispfenning, Volker.
ISSAC'08: Proceedings of the 21st International Symposium on Symbolic and Algebraic Computation 2008. ed. / David Jeffrey. New York: Association for Computing Machinery, 2008. p. 215-222.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - Deciding polynomial-exponential problems

AU - Achatz, Melanie

AU - McCallum, Scott

AU - Weispfenning, Volker

PY - 2008

Y1 - 2008

N2 - This paper presents a decision procedure for a certain class of sentences of first order logic involving integral polynomials and the exponential function in which the variables range over the real numbers. The inputs to the decision procedure are prenex sentences in which only the outermost quantified variable can occur in the exponential function. The decision procedure has been implemented in the computer logic system REDLOG. Closely related work is reported in [2, 7, 16, 20, 24].

AB - This paper presents a decision procedure for a certain class of sentences of first order logic involving integral polynomials and the exponential function in which the variables range over the real numbers. The inputs to the decision procedure are prenex sentences in which only the outermost quantified variable can occur in the exponential function. The decision procedure has been implemented in the computer logic system REDLOG. Closely related work is reported in [2, 7, 16, 20, 24].

UR - https://www.scopus.com/pages/publications/57449091282

U2 - 10.1145/1390768.1390799

DO - 10.1145/1390768.1390799

M3 - Conference proceeding contribution

AN - SCOPUS:57449091282

SN - 9781595939043

SP - 215

EP - 222

BT - ISSAC'08: Proceedings of the 21st International Symposium on Symbolic and Algebraic Computation 2008

A2 - Jeffrey, David

PB - Association for Computing Machinery

CY - New York

T2 - 21st Annual Meeting of the International Symposium on Symbolic Computation, ISSAC 2008

Y2 - 20 July 2008 through 23 July 2008

ER -

Deciding polynomial-exponential problems

Abstract

Other

Access to Document

Other files and links

Fingerprint

Cite this