Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal

Details:

   
TitleDeciding polynomial-transcendental problems
Author(s) Scott McCallum, Volker Weispfenning
TypeArticle in Journal
AbstractThis paper presents a decision procedure for a certain class of sentences of first order logic involving integral polynomials and a certain specific analytic transcendental function trans ( x ) in which the variables range over the real numbers. The list of transcendental functions to which our decision method directly applies includes exp ( x ) , the exponential function with respect to base e , ln ( x ) , the natural logarithm of x , and arctan ( x ) , the inverse tangent function. The inputs to the decision procedure are prenex sentences in which only the outermost quantified variable can occur in the transcendental function. In the case trans ( x ) = exp ( x ) , the decision procedure has been implemented in the computer logic system REDLOG. It is shown how to transform a sentence involving a transcendental function from a much wider collection of functions (such as hyperbolic and Gaussian functions, and trigonometric functions on a certain bounded interval) into a sentence to which our decision method directly applies. Closely related work is reported by Anai and Weispfenning (2000), Collins (1998), Maignan (1998), Richardson (1991), Strzebonski (in press) and Weispfenning (2000).
KeywordsDecision procedure, Exponential polynomials
ISSN0747-7171
URL http://www.sciencedirect.com/science/article/pii/S0747717111001167
LanguageEnglish
JournalJournal of Symbolic Computation
Volume47
Number1
Pages16 - 31
Year2012
Edition0
Translation No
Refereed No
Webmaster