指數(shù)函數(shù)多項(xiàng)式的實(shí)根分離算法

葛昕鈺，陳世平，劉忠

（1.中國(guó)科學(xué)院 成都計(jì)算機(jī)應(yīng)用研究所，成都 610041； 2.中國(guó)科學(xué)院大學(xué)，北京 100049；3.四川省貿(mào)易學(xué)校 財(cái)經(jīng)商貿(mào)系，四川 雅安 625107；4.樂山職業(yè)技術(shù)學(xué)院 電子信息工程系，四川 樂山 614000）（?通信作者電子郵箱geeexy@163.com）

指數(shù)函數(shù)多項(xiàng)式的實(shí)根分離算法

葛昕鈺1，2*，陳世平3，劉忠1，4

（1.中國(guó)科學(xué)院 成都計(jì)算機(jī)應(yīng)用研究所，成都 610041； 2.中國(guó)科學(xué)院大學(xué)，北京 100049；3.四川省貿(mào)易學(xué)校 財(cái)經(jīng)商貿(mào)系，四川 雅安 625107；4.樂山職業(yè)技術(shù)學(xué)院 電子信息工程系，四川 樂山 614000）（?通信作者電子郵箱geeexy@163.com）

針對(duì)超越函數(shù)多項(xiàng)式的實(shí)根分離問題，提出了一種指數(shù)函數(shù)多項(xiàng)式的區(qū)間分離算法exRoot，將非多項(xiàng)式型實(shí)函數(shù)的實(shí)根分離問題轉(zhuǎn)化為多項(xiàng)式正負(fù)性判定問題進(jìn)而對(duì)其求解。首先，利用泰勒替換法構(gòu)造目標(biāo)函數(shù)的多項(xiàng)式區(qū)間套；然后，將指數(shù)函數(shù)的求根問題轉(zhuǎn)化為多項(xiàng)式在區(qū)間內(nèi)正負(fù)性的判定問題；最后，給出綜合算法，并且試探性地應(yīng)用于實(shí)特征值線性系統(tǒng)的可達(dá)性判定問題。所提算法在Maple中實(shí)現(xiàn)，輸出的結(jié)果可讀，且高效易行。區(qū)別于HSOLVER和數(shù)值計(jì)算方法fsolve，exRoot回避了直接討論根的存在性問題，理論上具有終止性和完備性，且可達(dá)到任意精度，應(yīng)用于最優(yōu)化問題時(shí)可避免數(shù)值解帶來(lái)的系統(tǒng)誤差。

指數(shù)函數(shù)多項(xiàng)式；實(shí)根分離；泰勒替換法；區(qū)間列；終止性

0 引言

實(shí)根分離算法作為實(shí)代數(shù)的基本算法之一，不僅具有很強(qiáng)的理論意義，還有著廣泛的應(yīng)用前景。除了GCD（Greatest Common Divisor）算法、Sylvester結(jié)式、Descartes符號(hào)法則等經(jīng)典工具外，對(duì)于多項(xiàng)式型函數(shù)實(shí)根分離的研究也有進(jìn)展，例如Becker等［1］提出的Cisolate算法和Mehlhorn等［2］提出的漸進(jìn)方法。而上述多項(xiàng)式型函數(shù)的實(shí)根分離算法對(duì)非多項(xiàng)式型實(shí)函數(shù)的實(shí)根求解問題并不適用，因此仍需進(jìn)一步的研究［3-11］。目前求非多項(xiàng)式型實(shí)函數(shù)近似根的主要方法為迭代法，其過程中可能出現(xiàn)過分依賴初始近似值、迭代后局部收斂的問題，存在多個(gè)根時(shí)可能出現(xiàn)不收斂的情況。

在眾多非多項(xiàng)式型實(shí)函數(shù)中，指數(shù)函數(shù)在機(jī)器人逆運(yùn)動(dòng)學(xué)、分片代數(shù)簇、化學(xué)反應(yīng)器穩(wěn)定性分析等工程問題中有許多應(yīng)用，例如在實(shí)特征值線性系統(tǒng)的可達(dá)性判定中，多項(xiàng)式等式型約束即可轉(zhuǎn)化為指數(shù)函數(shù)的實(shí)根分離。然而，用迭代法解決指數(shù)函數(shù)實(shí)根分離問題的過程同樣會(huì)存在上述問題，并且沒有消除超越因子，因此不能真正解決指數(shù)函數(shù)中的超越問題。由此，指數(shù)函數(shù)實(shí)根分離的自動(dòng)證明和程序開發(fā)也成為人工智能和自動(dòng)推理中重要且具有挑戰(zhàn)的任務(wù)。

近年來(lái)也有學(xué)者對(duì)其自動(dòng)證明算法進(jìn)行研究：文獻(xiàn)［11］中提出了針對(duì)exp-log-arctan型函數(shù)的實(shí)根分離方法，根據(jù)半傅里葉序列（semi-Fourier sequence）符號(hào)的變化數(shù)判定根的存在性，但算法的完備性依賴于尚未證明的Schanuel猜想；文獻(xiàn)［12］中利用羅爾中值定理對(duì)多項(xiàng)式的偽倒數(shù)進(jìn)行判定從而分離其實(shí)根，其方法直接應(yīng)用于超越函數(shù)exp（x）、ln（x）、arctan（x）以解決實(shí)數(shù)范圍的超越函數(shù)實(shí)根分離問題，部分決策過程已在計(jì)算機(jī)邏輯系統(tǒng)Redlog中實(shí)現(xiàn)；文獻(xiàn)［13］中采用連分?jǐn)?shù)構(gòu)造指數(shù)函數(shù)多項(xiàng)式的區(qū)間套，從而估計(jì)指數(shù)函數(shù)多項(xiàng)式在有理點(diǎn)上的值。

為了更好地解決指數(shù)函數(shù)的實(shí)根分離問題，可將其理解為指數(shù)多項(xiàng)式在特定區(qū)間上的正負(fù)性判定問題。文獻(xiàn)［3，14-17］中利用反正切函數(shù)泰勒展開式交錯(cuò)級(jí)數(shù)的特性設(shè)計(jì)了混合三角多項(xiàng)式不等式的泰勒替換法，其核心思想是先確定根所在的區(qū)間，再構(gòu)造其上、下界多項(xiàng)式找到包含非多項(xiàng)式型實(shí)函數(shù)的有理函數(shù)多項(xiàng)式列，從而判定該區(qū)間上三角函數(shù)多項(xiàng)式正負(fù)性，進(jìn)而實(shí)根分離。文獻(xiàn)［3］中根據(jù)該算法已經(jīng)完成了對(duì)三角函數(shù)多項(xiàng)式實(shí)根分離的自動(dòng)求解程序，并在符號(hào)計(jì)算軟件Maple中實(shí)現(xiàn)。延續(xù)在三角函數(shù)上的思想，文獻(xiàn)［17］中提出了指數(shù)多項(xiàng)式不等式的判定方法。本文即在文獻(xiàn)［17］研究的基礎(chǔ)上，以指數(shù)多項(xiàng)式不等式的判定為主要工具，提出了針對(duì)形如f（x，）的指數(shù)函數(shù)的實(shí)根分離算法exRoot，并對(duì)指數(shù)函數(shù)的最優(yōu)化問題進(jìn)行了討論，得到了極值所在的確定區(qū)間。

區(qū)別于文獻(xiàn)［11-12］的方法，本文將非多項(xiàng)式型實(shí)函數(shù)的實(shí)根分離問題轉(zhuǎn)化為多項(xiàng)式判定問題進(jìn)而求解，回避了直接討論根的存在性問題，并應(yīng)用于多項(xiàng)式優(yōu)化問題中。算法exRoot已經(jīng)在Maple中實(shí)現(xiàn)程序，可自動(dòng)輸出含單根的區(qū)間列，且區(qū)間長(zhǎng)度可以滿足任意精度，形成完備且可讀的證明過程。程序在Intel Core i5-6500 Windows x64 Maple2015環(huán)境下對(duì)隨機(jī)生成的實(shí)例運(yùn)行時(shí)長(zhǎng)均未超過15 s。

1 指數(shù)多項(xiàng)式

先給出一些有關(guān)代數(shù)數(shù)和超越數(shù)的基本知識(shí)。

定義1［15］給定一個(gè)數(shù)a，若存在系數(shù)不全為零的整系數(shù)多項(xiàng)式P（x）使得P（a）=0，則稱a是代數(shù)的或a是代數(shù)數(shù)，否則稱a是超越數(shù)。

引理1［15］每一個(gè)代數(shù)數(shù)系數(shù)多項(xiàng)式的根也是代數(shù)數(shù)。

定義2［15］給定二元有理系數(shù)多項(xiàng)式環(huán)Q［x，y］，將其中的變量y用eqx替換（），定義該環(huán)上的一個(gè)映射hom：f（x，y）→f（x，eqx）。二元有理多項(xiàng)式f（x，y）在該映射下的像F（x）=hom（f（x，y））=f（x，eqx）被稱為指數(shù)多項(xiàng)式。記映射后的環(huán)為Q［x，eqx］。

定義3［17］x0稱為實(shí)函數(shù)的重根，如果φ（x0）=φapos;（x0）=0。

引理2［17］若f（x，y）是二元有理多項(xiàng)式，那么指數(shù)多項(xiàng)式f（x，y）=f（x，ex）唯一可能的重根是0。

引理3若f（x，y）?0，則F（x）=hom（f（x，y））?0（此處f（x，y）?0表示f（x，y）不恒等于0，下同）。

下面討論mgt;0且cm（x）?0的情況。假設(shè)f（x，y）?0而F（x）=hom（f（x，y））≡0。由于（e2）n是超越的，而對(duì)有理多項(xiàng)式ci（2）是代數(shù)數(shù)。由定義2，F(xiàn)（e2）=cm（2）（e2）m+（++c0（2） =0說明cm（2）===c0（2）=0，代入則有f（x，y）?0，與假設(shè)矛盾。綜上所述，引理3成立。

定義在［0，+∞）的指數(shù)多項(xiàng)式具有環(huán)的代數(shù)結(jié)構(gòu)，即hom是二元有理系數(shù)多項(xiàng)式環(huán)到指數(shù)多項(xiàng)式環(huán)的一個(gè)映射。由引理2可知映射hom是一對(duì)一的，顯然也是Q［x，y］到Q［x，eqx］滿射，那么存在其逆映射：F（x）=f（x，eqx）→f（x，y）。

引理4F（x）=f（x，ex）在求導(dǎo)運(yùn)算下封閉。

引理5［17］對(duì)給定的二元有理多項(xiàng)式f（x，y），存在，使得指數(shù)多項(xiàng)式的任意正根。若變?cè)蛟O(shè)定為，將f（x，y）按字典序降序排列，當(dāng)xgt;MR時(shí)，若其首系為正，；若其首系為負(fù)，。

根據(jù)文獻(xiàn)［17］中對(duì)引理5的證明過程，有算法1計(jì)算根的上界。

算法1 upBound。

輸入 二元有理多項(xiàng)式f（x，y）；

輸出 有理多項(xiàng)式f（x，y）根的一個(gè)上界MR。

BEGIN

END

其中realroot（f（x），r）是Maple中關(guān)于有理多項(xiàng)式的實(shí)根分離命令：輸入有理多項(xiàng)式f（x）和精度r，返回一個(gè)互不相交的區(qū)間列。整個(gè)列表包含的實(shí)根，每個(gè)區(qū)間只包含一個(gè)實(shí)根，且各區(qū)間長(zhǎng)度均不超過r。

引理6［16］對(duì)二元有理多項(xiàng)式f（x，y），F(xiàn)（x）=f（x，ex）在（0，+∞）內(nèi)至多有有限個(gè)不同實(shí)根（重根只記一次）。

記G（x）在0點(diǎn)Taylor展開式的前n項(xiàng)之和為，例如，?？梢?，展開各項(xiàng)依次交錯(cuò)，對(duì)此構(gòu)造其多項(xiàng)式列，進(jìn)而實(shí)現(xiàn)指數(shù)函數(shù)的多項(xiàng)式型放縮。

定義4記，，記，對(duì)hom：y=ex有。當(dāng)時(shí)，記，否則。記Fd（x）=hom（fd（x，y））。

顯然f（x，y）=fd（x，y）·yn，那么對(duì)，有。

以下若未作特殊說明，均假設(shè)x∈（0，+∞）（對(duì)的討論可作變量替換）。

定義5若在區(qū)間（0，T］（）內(nèi)滿足1）～3），則常數(shù)稱為T的臨界值，稱在區(qū)間上可規(guī)范展開。

1）F（x）gt;0；

引理7［17］假設(shè)多項(xiàng)式T1（x）gt;0，T2（x）gt;0且，則。

引理8［17］當(dāng)時(shí)，對(duì)任意有：

3）當(dāng)n→∞ 時(shí)，。

定義6對(duì)任意，記為Fd（x）的一個(gè)上界多項(xiàng)式，記為Fd（x）的一個(gè)下界多項(xiàng)式。

引理9［17］對(duì)任意，當(dāng)時(shí)，有：

1）Tmax（x，n，F(xiàn)d（x））gt;F（x）gt;Tmin（x，n，F(xiàn)d（x））；

3）當(dāng)n→∞時(shí)，Tmax（x，n，F(xiàn)d（x））→Fd（x），Tmin（x，n，。

對(duì)關(guān)于x的單變量多項(xiàng)式，有以下性質(zhì)：

定理1［17］任意x∈（0，T］，F(xiàn)d（x）=f（x，e-x）gt;0成立當(dāng)且僅當(dāng)。

定理2［17］任意x∈（0，T］，F(xiàn)d（x）=f（x，e-x）lt;0成立當(dāng)且僅當(dāng)Tmax（x，n，F(xiàn)d（x））≤0。

定理1和定理2說明函數(shù)在區(qū)間（0，T］上任意一有理點(diǎn)的正負(fù)性是可判定的。在此基礎(chǔ)上本文設(shè)計(jì)了算法2，用來(lái)判定函數(shù)F（x）=f（x，ex）在區(qū)間（a，b）∈（0，T）上的值域與0的大小關(guān)系。具體思路如下：1）判定上界多項(xiàng)式是否在該范圍內(nèi)恒小于0，如果是，那么該段上函數(shù)值均為負(fù)，判定結(jié)果記為；2）判定下界多項(xiàng)式是否在該范圍內(nèi)恒大于0，如果是，那么該段上函數(shù)值均為正，判定結(jié)果記為1；3）判定在該范圍內(nèi)下界多項(xiàng)式小于0、上界多項(xiàng)式大于0，如果是，那么函數(shù)在該段正負(fù)性不確定，判定結(jié)果記為0；4）如果上述情況均不符合，則遞歸進(jìn)行其項(xiàng)展開繼續(xù)判定，直至得出判定結(jié)果。

由于區(qū)間端點(diǎn)均為有理數(shù)，因此端點(diǎn)值不會(huì)是非多項(xiàng)式型實(shí)函數(shù)的根，故在如下討論中不考慮端點(diǎn)，均使用開區(qū)間。

算法2 determination。

輸入 1）Fd（x）=f（x，），2）a（），3）b（）；

輸出sgn。 #返回值sgn表示在區(qū)間（a，b）上的值域與0的關(guān)系：表示函數(shù)在該區(qū)間內(nèi)值域下界大于0，表示函數(shù)在該區(qū)間內(nèi)值域上界小于0；表示在該區(qū)間內(nèi)值域包含0。

BEGIN

#該段函數(shù)值為正，算法結(jié)束

#該段正負(fù)性不定，算法結(jié)束

END

其中，prove（ineq，（a，b））表示對(duì)不等式ineq在區(qū)間（a，b）上的判定，ineq在（a，b）上成立則返回true，否則返回false。可通過Maple的不等式證明程序包Bottema中的判定工具xprove（ineq，［xgt;a，xlt;b］）實(shí)現(xiàn)。

定理3［17］對(duì)不可約二元有理多項(xiàng)式，算法2必然終止。

根據(jù)算法1和算法2有對(duì)應(yīng)程序upBound（expr）、determination（expr，a，b）。

2 指數(shù)多項(xiàng)式的實(shí)根分離

2.1 指數(shù)多項(xiàng)式的實(shí)根分離算法

而判定fd（x，y）在區(qū)間（0，MR）內(nèi)根的存在性的基本思路是：對(duì)不可約多項(xiàng)式fd（x，y），fd（x，y）在（a，b）上恒大于0或恒小于0，則在（a，b）上無(wú)實(shí)根；否則對(duì)fapos;d（x，y）進(jìn)行判定，若在（a，b）上單調(diào)，則有唯一實(shí)根；若fd（x，y）在（a，b）上既不恒大于0，也不恒小于0，在（a，b）上也不單調(diào)，那么采用二分法分離區(qū)間，再遞歸進(jìn)行判定。根據(jù)以上說明，本文構(gòu)造了算法3用于實(shí)根分離。

算法3 isolation。

BEGIN

END

定理4若f（x，y）為不可約二元有理多項(xiàng)式，算法3必然終止。

證明f（x，y）在區(qū)間（0，T）上任意一有理點(diǎn)的正負(fù)性總是可判定的，并由引理6可知，f（x，y）最多有有限個(gè)根，那么判定過程必然是有限步的。過程采用二分法，保證各區(qū)間不相交。那么，算法3必然終止。

對(duì)已有但不滿足精度要求的區(qū)間列，可用二分法分割區(qū)間直至滿足精度要求（算法4）。

算法4 accuracy。

輸入 1）Fd（x），2）Fd（x）的單根區(qū)間（a，b），3）給定精度r（rgt;0）；

輸出 （c，d）。#F（x）在（c，d）內(nèi)有唯一根且

BEGIN

END

綜上所述，本文提出綜合算法5對(duì)多項(xiàng)式進(jìn)行轉(zhuǎn)化和判定：輸入（此時(shí)）求出MR后，同除y的最高次冪將多項(xiàng)式變形為，運(yùn)行算法3對(duì)其實(shí)根分離，得到區(qū)間列后采用算法4提升精度，輸出滿足設(shè)置精度的、互不相交的區(qū)間列，每個(gè)區(qū)間內(nèi)有且只有一個(gè)根。

輸入 1）二元有理多項(xiàng)式f（x，y），2）；

BEGIN

END

根據(jù)算法3、算法4和算法5有對(duì)應(yīng)程序isolation（expr，a，b）、accuracy（expr，a，b，r）和exRoot（expr，r）。

例1，。

利用算法5求解該例過程如下：

c）輸出區(qū)間列｛（0，1）｝。

4）運(yùn)行accuracy（Fd（x），0，1，2，1/10），二分法求精度，結(jié)果為（11/16，3/4）。

2.2 實(shí)根分離算法應(yīng)用實(shí)例

例2［13］指數(shù)函數(shù)多項(xiàng)式，考慮φ（x）的根。

對(duì)不可約多項(xiàng)式φ（x）有。

例4［18］對(duì)線性非齊次系統(tǒng)：

運(yùn)行程序exRoot（f（x，y），1/4），得到結(jié)果為｛（3/4，1）｝。也就是說，該系統(tǒng)在內(nèi)可達(dá)。

上述實(shí)例已在Intel Core i5-6500，Windows 7 x64， Maple2015環(huán)境下進(jìn)行驗(yàn)證，運(yùn)行時(shí)間如表1所示。其中，fsolve為Maple中實(shí)根隔離的數(shù)值工具，每次只能隔離出一個(gè)實(shí)根。同時(shí)，相較HSOLVER，exRoot對(duì)例4的計(jì)算時(shí)間明顯較短，且例2的計(jì)算結(jié)果與fsolve一致。

表1 實(shí)例運(yùn)行時(shí)間Tab. 1 Running times of examples

3 最優(yōu)化問題

3.1 最優(yōu)化算法

同時(shí)，實(shí)根分離算法還可用于最優(yōu)化問題。

定理5 對(duì)有理多項(xiàng)式F（x）有。

根據(jù)定理5可以由各極值比較得出最值點(diǎn)所在的區(qū)間。算法6（算法7）是比較兩個(gè)極值區(qū)間中較大（?。┑臉O值點(diǎn)所在的區(qū)間，這樣可以通過算法8得到最值點(diǎn)所在的區(qū)間。

算法6 comparisonMax。

輸入 1）F（x），2）極大值點(diǎn)（a1，b1），3）極大值點(diǎn)（a2，b2），4）n0；

BEGIN

END

算法7 comparisonMin。

輸入 1）F（x），2）極小值點(diǎn)，3）極小值點(diǎn)，4）n0；

BEGIN

END

得到最值點(diǎn)區(qū)間后進(jìn)而求出最值區(qū)間，同樣利用定理5進(jìn)行進(jìn)一步放縮。

對(duì)最大值點(diǎn)所在區(qū)間（amax，bmax），有。

將F（x）的上、下界多項(xiàng)式代入，進(jìn)一步得到。

對(duì)值域不滿足精度要求的結(jié)果，可進(jìn)一步通過算法4操作使其達(dá)到精度限制。

算法8 optimization。

輸入 1）F（x），2）F（x）的駐點(diǎn)區(qū)間列，3）n0；

BEGIN

END

3.2 最優(yōu)化算法應(yīng)用實(shí)例

求解過程如下：

運(yùn)行產(chǎn)生的分子分母大整數(shù)的分?jǐn)?shù)會(huì)降低結(jié)果的可讀性，可采取如下簡(jiǎn)化策略：將分?jǐn)?shù)的分子分母從個(gè)位開始同時(shí)去掉若干位數(shù)（分母保留的位數(shù)不得低于，否則無(wú)法達(dá)到指定精度r），再將區(qū)間左端點(diǎn)的分母加1，右端點(diǎn)的分子加1，這樣得到的區(qū)間是端點(diǎn)的分子分母的位數(shù)可以小于給定數(shù)且包含原區(qū)間的最小區(qū)間［3］。通過如上放縮后區(qū)間簡(jiǎn)化為，即F（x）最小值所在區(qū)間為。最優(yōu)化過程在Intel Core i5-6500，Windows 7 x64操作系統(tǒng)，Maple2015環(huán)境下運(yùn)行時(shí)間0.87 s。

4 結(jié)語(yǔ)

本文在指數(shù)函數(shù)多項(xiàng)式判定算法的基礎(chǔ)上，將指數(shù)函數(shù)的實(shí)根分離問題轉(zhuǎn)化為多項(xiàng)式判定問題進(jìn)而求解，實(shí)現(xiàn)了指數(shù)函數(shù)實(shí)根分離的完全算法exRoot。該算法回避了根的存在性問題，找出了包含全部實(shí)根且區(qū)間互不相交的區(qū)間列（每個(gè)區(qū)間有且僅有一個(gè)實(shí)根），區(qū)間長(zhǎng)度可達(dá)到任意精度。然后將其應(yīng)用于多項(xiàng)式優(yōu)化問題中，通過對(duì)指數(shù)多項(xiàng)式導(dǎo)數(shù)的實(shí)根分離得到駐點(diǎn)存在的區(qū)間，最終得到極值的確定范圍。本文解決了一類超越函數(shù)解的問題，簡(jiǎn)單易行，十分高效。

[1] BECKER R， SAGRALOFF M， SHARMA V， et al. A near-optimal subdivision algorithm for complex root isolation based on the Pellet test and Newton iteration ［J］. Journal of Symbolic Computation， 2018， 86： 51-96.

[2] MEHLHORN K， SAGRALOFF M， WANG P M. From approximate factorization to root isolation with application to cylindrical algebraic decomposition ［J］. Journal of Symbolic Computation， 2015， 66：34-69.

[3] 陳世平，劉忠.三角函數(shù)多項(xiàng)式的實(shí)根分離［J］.汕頭大學(xué)學(xué)報(bào)（自然科學(xué)版），2016，31（3）：25-39.（CHEN S P， LIU Z. Real root isolation of trigonometric function polynomial ［J］. Journal of Shantou University （Natural Science Edition）， 2016， 31（3）：25-39.）

[4] 楊路，夏壁燦.不等式機(jī)器證明與自動(dòng)發(fā)現(xiàn)［M］.北京：科學(xué)出版社，2008：126-130.（YANG L， XIA B C. Inequality Machanical Proving and Automatic Discovery ［M］. Beijing： Science Press， 2008： 126-130.）

[5] ACHATZ M， McCALLUM S， WEISPFENNING V. Deciding polynomial-exponential problems ［C］// Proceedings of the 2008 21st International Symposium on Symbolic and Algebraic Computation. New York： ACM， 2008： 215-222.

[6] WU W T. Basic principles of mechanical theorem proving in elementary geometries ［J］. Journal of Automated Reasoning， 1986， 2（3）： 221-252.

[7] BUCHBERGER B， COLLINSS G E， KUTZLER B. Algebraic methods for geometric reasoning ［J］. Annual Review of Computer Science， 1988， 3： 85-119.

[8] YANG L， ZHANG J. A practical program of automated proving for a class of geometric inequalities ［C］// Proceedings of the 2000 International Workshop on Automated Deduction in Geometry， LNCS 2061. Berlin： Springer， 2000： 41-57.

[9] 陸征一，何碧，羅勇.多項(xiàng)式系統(tǒng)的實(shí)根分離算法及其應(yīng)用［M］.北京：科學(xué)出版社，2004：34-44. （LU Z Y， HE B， LUO Y， Real Root Isolation Algorithm of Polynomial System and Its Applications ［M］. Beijing： Science Press， 2004： 34-44.）

[10] DAI L Y， FAN Z， XIA B C， et al. Logcf： an efficient tool for real root isolation ［J］. Journal of Systems Science and Complexity，2019， 32（6）： 1767-1782.

[11] STRZEBO?SKI A. Real root isolation for exp-log-arctan functions ［J］. Journal of Symbolic Computation， 2012， 47（3）： 282-314.

[12] MCCALLUM S， WEISPFENNING V. Deciding polynomial-transcendental problems ［J］. Journal of Symbolic Computation， 2012， 47（1）： 16-31.

[13] 徐鳴.程序驗(yàn)證與系統(tǒng)分析中的若干符號(hào)問題［D］.上海：華東師范大學(xué)，2010：11-20.（XU M. Some symbolic computation issues in program verification and system analysis ［D］. Shanghai： East China Normal University， 2010： 11-20.）

[14] CHEN S P， LIU Z. Automated proof of mixed trigonometric-polynomial inequalities ［J］. Journal of Symbolic Computation， 2020， 101： 318-329.

[15] 陳世平，劉忠.一類超越函數(shù)多項(xiàng)式不等式的自動(dòng)證明［J］.系統(tǒng)科學(xué)與數(shù)學(xué)，2019，39（5）：804-822.（CHEN S P， LIU Z. Automated proving for a class of transcendental-polynomial inequalities ［J］. Journal of Systems Science and Mathematical Sciences， 2019， 39（5）： 804-822.）

[16] 陳世平，劉忠.三角函數(shù)多項(xiàng)式不等式的自動(dòng)證明［J］.汕頭大學(xué)學(xué)報(bào)（自然科學(xué)版），2015，30（3）：43-55.（CHEN S P， LIU Z. Automated proving of trigonometric function polynomial inequalities ［J］. Journal of Shantou University （Natural Science Edition）， 2015， 30（3）： 43-55.）

[17] 陳世平，劉忠.指數(shù)多項(xiàng)式不等式的自動(dòng)證明［J］.系統(tǒng)科學(xué)與數(shù)學(xué)，2017，37（7）：1692-1703.（CHEN S P， LIU Z. Automated proving of exponent polynomial inequalities ［J］. Journal of Systems Science and Mathematical Sciences， 2017， 37（7）： 1692-1703.）

[18] XU M， CHEN L Y， ZENG Z B， et al. Reachability analysis of rational eigenvalue linear systems ［J］. International Journal of Systems Science，2010， 41（12）： 1411-1419.

Real root isolation algorithm for exponential function polynomials

GE Xinyu1，2*， CHEN Shiping3， LIU Zhong1，4

（1.Chengdu Institute of Computer Application，Chinese Academy of Sciences，Chengdu Sichuan610041，China；2.University of Chinese Academy of Sciences，Beijing100049，China；3.Department of Finance and Commerce，Sichuan Trade School，Ya’an Sichuan625107，China；4.Department of Electronic Information Engineer ing，Leshan Vocational and Technical College，Leshan Sichuan614000，China）

For addressing real root isolation problem of transcendental function polynomials， an interval isolation algorithm for exponential function polynomials named exRoot was proposed. In the algorithm， the real root isolation problem of non-polynomial real functions was transformed into sign determination problem of polynomial， then was solved. Firstly， the Taylor substitution method was used to construct the polynomial nested interval of the objective function. Then， the problem of finding the root of the exponential function was transformed into the problem of determining the positivity and negativity of the polynomial in the intervals. Finally， a comprehensive algorithm was given and applied to determine the reachability of rational eigenvalue linear system tentatively. The proposed algorithm was implemented in Maple efficiently and easily with readable output results. Different from HSOLVERand numerical calculation method fsolve，exRoot avoids discussing the existence of roots directly， and theoretically has termination and completeness. It can reach any precision and can avoid the systematic error brought by numerical solution when being applied into the optimization problem.

exponential function polynomial; real root isolation; Taylor substitution method; sequence of intervals; termination

TP181

A

1001-9081（2022）05-1524-07

10.11772/j.issn.1001-9081.2021030440

2021?03?22；

2021?07?14；

2021?07?14。

四川省科學(xué)技術(shù)廳科技計(jì)劃項(xiàng)目（2016GFW0048）。

葛昕鈺（1995—），女，河南安陽(yáng)人，博士研究生，CCF會(huì)員，主要研究方向：自動(dòng)推理、機(jī)器證明； 陳世平（1970—），男，四川遂寧人，高級(jí)講師，博士，主要研究方向：機(jī)器證明、符號(hào)計(jì)算； 劉忠（1968—），男，四川樂山人，教授，博士，主要研究方向：自動(dòng)推理、機(jī)器證明。

This work is partially supported by Scientific and Technological Program of Science and Technology Department of Sichuan Province （2016GFW0048）.

GE Xinyu， born in 1995， Ph. D. candidate. Her research interests include automated reasoning， mechanical proving.

CHEN Shiping， born in 1970， Ph. D.， senior lecturer. His research interests include mechanical proving，symbolic computation.

LIU Zhong， born in 1968， Ph. D.， professor. His research interests include automated reasoning，mechanical proving.