平面并聯機構的形式化建模與驗證

陳 琦，王國輝，張倩穎，施智平，陳善言，關 永

(高可靠嵌入式系統技術北京市工程研究中心，首都師范大學 信息工程學院，北京 100048)

E-mail：ghwang@cnu.edu.cn

1 引 言

并聯機構是指含有兩個或兩個以上自由度且以并聯方式驅動的一種閉環機構，它的動平臺和靜平臺通過至少兩個獨立的支鏈相連接.常見的并聯機構包括平面并聯機構和空間并聯機構.其中具有三自由度的平面并聯機構在3D打印[1]、數控機床[2]等方面有著廣泛的應用.它能夠完成靈活、精細的抓取操作的同時具有較強的承載力，但這也增加了平面并聯機構的控制難度.平面并聯機構控制算法是為了解決工作空間[3]、奇異位置[4]、校對零位置[5]等問題而被學術界提出的，這些問題的研究基礎是正運動學求解.正運動學求解[6]是指根據支鏈的桿長對動平臺相對靜平臺的位置和姿態進行求解.常用的正運動學求解方法是D-H法，但它存在消元求解技巧性強、計算過程復雜等問題，極易導致求解過程錯誤.為了解決這一問題，學術界基于幾何代數對平面并聯機構進行了研究.例如：張立先[7]提出了基于幾何代數的并聯機構分析，利用旋量和關節速度的幾何表示，研究并聯機構的奇異性，但其表達式不夠簡潔.而相比于幾何代數，共形幾何代數[8](Conformal Geometric Algebra，CGA)具有幾何概念清楚、物理意義明確、表達形式簡單、代數運算方便等優點，便于工程應用中的幾何解釋、問題描述，極大地降低了機器人運動學的研究難度.因此，學術界基于CGA對平面并聯機構進行了研究.例如：倪振松[9]提出了基于CGA的一種平面并聯機構位置正解分析方法，建立了運動學正解模型.它是CGA在平面并聯機構運動學應用的一個初步嘗試.之后，針對3RPR平面并聯機構，張英[10]提出了平面并聯機構正運動學分析的幾何建模和免消元計算，為平面并聯機構運動學求解理論提供了一種新思路.以上算法都是基于特定機構進行研究，而黃昔光[6]提出的基于CGA的平面并聯機構位置正解求解方法，是一種一般性求解方法，普遍適用于所有平面并聯機構，但該方法仍處于數值驗證階段.因此，本文基于CGA對平面并聯機構的正向運動學求解方法進行形式化建模與驗證.

與基于計算機代數系統等傳統方法不同，形式化方法是是建立在嚴格完備的數學基礎上，采用精確數學語義的推理方法[11].它可以根據數學邏輯的嚴密性來提高發現微小錯誤的機率，具有較強的準確性和完備性.目前形式化驗證技術主要有以下兩種：模型檢驗和定理證明.模型檢驗[12]是將系統表達為有限狀態機的自動驗證技術.定理證明[13]是將研究內容建立物理模型，提取屬性性質后轉化成數學模型，根據語言規范和運算變成邏輯模型.與模型檢驗相比，定理證明不僅可以處理大規模的系統，而且可以對無限狀態系統進行推理，擁有更好的靈活性.因此，本文采用定理證明的方法.常見的定理證明器有：ACL2、Mizar、Coq、PVS、HOL等，其中HOL家族中HOL Light[14]是最流行的定理證明器之一，它包含了高效的證明策略和豐富的數學定理庫，如：幾何代數庫、共形幾何代數庫、實分析庫、多維向量庫等，而且使用了更加簡單易懂的邏輯核心，能夠準確檢查定義和定理的形式化表達的正確性，使系統更加輕便、高效、簡潔，為我們接下來的工作提供了重要的保障.本文選擇HOL Light對CGA進行驗證.

目前，幾何代數形式化工作也取得了一些成果，例如：李黎明[11，15]完成了幾何代數庫的搭建，形式化證明了幾何代數結構及基本運算，為我的工作奠定了理論基礎.馬莎[8，16]完成了共形幾何代數庫的搭建，形式化驗證了幾何表示和幾何變換，同時，建立了5-R 串聯機器人位置逆解和串聯機器人抓取算法的模型，但目前并沒有對并聯機構進行形式化建模與驗證.

本文以幾何代數、CGA的高階邏輯表達為基礎，在HOL Light定理證明器中形式化描述了平面并聯機構相關數學理論，通過運動變換等效模型、點運動變換表達式方程、桿長約束方程、位置正解封閉方程組實現平面并聯機構正向運動學的高階邏輯模型的建立，形式化分析與驗證正向運動學的一般性求解算法，驗證位置正解方程與一元六次方程的等價性，從而確保平面并聯機構運動學分析的正確性和分析求解方法的可靠性.

2 基于CGA的剛體運動的形式化

幾何代數是一種用于描述和計算幾何問題的代數語言，實現了高維幾何計算與幾何分析的統一[16]，使其成為連接幾何和代數的統一的描述性語言.幾何代數包括三種重要的運算積：外積、內積和幾何積.外積主要用于幾何體的構建，內積主要用于距離與角度的計算，幾何積主要用于運動的描述.表1是幾何代數的運算符號.

表1 幾何代數的運算符號

內積是一個降維運算，它與向量代數中的標準內積不同.幾何代數的內積運算對象既可以是同維度空間對象也可以是不同維度空間對象，它能表示空間對象的距離、角度等幾何表達.Inner是HOL Light中定義的高階邏輯函數，表示幾何代數的內積運算.

外積是一個升維運算.Outer是HOL Light中定義的高階邏輯函數，表示幾何代數的外積運算.當向量a，b線性相關時，其外積為零.此外，外積也滿足反對稱性.

幾何積是連接內積和外積的混合運算.對于向量來說，幾何積等于其內積和外積之和.

下文是基于CGA的剛體運動的形式化.空間剛體運動主要包括旋轉和平移.

定義1.旋轉算子的旋量可表示為

(1)

可形式化如下：

|-?tmn.Rotation_CGAtmn=cos(t/& 2)%mbasis{}-

sin(t/& 2)/(norm(multivecmoutermultivecn)%

(multivecmoutermultivecn))

其中，t，m，n是變量.“&”是將自然數類型(：num)轉換為實數類型(：real)的運算符.“%”表示向量的數乘.為了保持類型統一，實數與mbasis{}相乘可以把實數類型轉化為向量類型.函數norm是HOL Light中定義的高階邏輯函數，輸入變量是N維向量，輸出結果是N維向量的范數.函數multivec可將向量轉換為對應的多重向量的形式.

定義2.平移算子的旋量可表示為

T=1-(t1e1+t2e2+t3e3)e∞/2

(2)

其中，t=t1e1+t2e+t3e3為平移向量.

可形式化如下：

|-?t.Translation_CGAt=mbasis{}-& 1/& 2%(t＄1%

mbasis{1}+t＄2%mbasis{2}+t＄3%mbasis{3})*null_inf

當運算對象為實數“*”表示數乘.當運算對象為多重向量時表示幾何積.其中mbasis{i}表示靜坐標的基底ei.t＄1%mbasis{1}+t＄2%mbasis{2}+t＄3%mbasis{3}表示平移向量.

定理1.旋轉算子的共軛

旋轉算子R的共軛

(3)

可形式化如下：

|-?tmn.reversion(Rotation_CGAtmn)=cos(t/& 2)%mbasis(t/& 2)/(norm(multivecmoutermultivecn)%(multivecmoutermultivecn))

其中，reversion(Rotation_CGAtmn)表示旋轉的共軛.通過旋轉定義、共軛、幾何積和外積的基本運算性質，結合策略REWRITE_TAC簡化目標，進而利用策略COND_CASES_TAC拆分目標，最后使用向量基本運算性質實現定理1的形式化證明.該定理在剛體運動方程的共軛(定理4)中將被使用到.

定理2.平移算子的共軛

平移算子T的共軛

(4)

可形式化如下：

|-reversion(Translation_CGAt)=mbasis{}+& 1/& 2%

(t＄1%mbasis{1}+t＄2%mbasis{2}+t＄3%mbasis{3})*null_inf

通過平移定義、共軛的基本運算性質，結合有限集合相關定理對不同情況進行分類討論，并使用實數推導策略完成定理2的形式化證明.

定義3.剛體運動的運動算子

在CGA中，旋轉(定義1)和平移(定義2)在旋量下的復合是簡單的幾何積，所以剛體運動的運動算子

M=RT

(5)

可形式化如下：

|-?tmnl.motor_CGAtmnl=Rotation_CGAtmn*

Translation_CGAl

其中，t，m，n，l表示變量.其中，motor_CGAtmnl表示剛體運動算子.Rotation_CGAtmn表示旋轉算子，它包含三個變量；Translation_CGAl表示平移算子，它包含一個變量.

定義4.剛體運動的運動算子

在CGA中，任意剛體o的剛體運動變化都可以借助幾何積來實現，廣泛適用于CGA中所有剛體的空間運動變換.它的表達式為：

(6)

其中，origid_motion為o變化后的剛體；M為規范化的運動變換算子.

可形式化如下：

|-?xtmnl.geometry_CGAxtmnl=motor_CGAtmnl*

x*reversion(motor_CGAtmnl)

其中，x表示任意剛體，motor_CGAtmnl表示剛體運動的運動算子，reversion(motor_CGAtmnl)表示運動算子的共軛.

3 平面并聯機構的形式化建模與驗證

平面并聯機構正運動學的一般性算法是指根據桿長的約束條件，建立1140種平面并聯機構等效機構模型的普適方法.該算法可以解決實際生產過程中所有平面并聯機構的正運動學問題.研究內容主要分為兩部分：一是對平面并聯機構等效模型的位置正解封閉方程組進行形式化建模；二是驗證平面并聯機構位置正解方程與一元六次方程的等價性.具體步驟如下：

S1：為了將具體的實際問題抽象成為CGA問題，需要建立運動變換等效模型，如圖1所示.這一模型可以代表所有平面并聯機構，通過這一模型就能夠得到剛體運動算子方程.

圖1 平面并聯機構等效模型

S2：基于這個等效模型，建立點運動變換后的表達式方程.接著，通過剛體運動算子方程，得到動平臺的點在靜平臺下的坐標.

S3：將上述步驟求得的點坐標與桿長結合得到桿長約束方程.

S4：通過步驟2、步驟3的運算結果，建立了平面并聯機構等效模型的位置正解封閉方程組.

S5：對封閉方程組的消簡過程進行形式化驗證.也就是驗證平面并聯機構位置正解方程與一元六次方程的等價性.

3.1 建立運動變換等效模型

圖1為平面并聯機構的等效模型，虛線表示連接動平臺、靜平臺的等效運動支鏈，其長度為支鏈的實際長度.它是一個一般性的方法，普遍適用于所有平面并聯機構.

取點P1為靜坐標xoy的坐標原點，P1P2方向為x軸，三個靜平臺點坐標分別為P1(0，0)，P2(P2x，0)，P3(P3x，P3y)；取P4為動坐標x1o1y1的原點，P4P5方向為動坐標x1軸，點在動坐標x1o1y1中的坐標為P4(0，0)，P5(P5x，0)，P6(P6x，P6y).設點P4在靜坐標xoy中的坐標為(Px，Py)，動坐標x1o1y1相對于靜坐標xoy的姿態角為θ.平面并聯機構正運動學的一般性算法就是已知三條等效支鏈的桿長q1(P1P4)、q2(P2P5)、q3(P3P6)，求點P4在靜坐標的坐標(Px，Py)及姿態角θ.

動坐標到靜坐標的運動變換可以看做三個點的變換過程，P4可看作靜坐標中的P1沿x軸平移Px，沿y軸平移Py，再繞z軸旋轉θ角得到，P5、P6也如此，這樣子就可以得到P4、P5、P6在靜坐標下的坐標.通過建立運動變換等效模型，得到剛體運動算子方程.

定義5.橫向平移

靜坐標沿x軸平移Px，即

(7)

可形式化如下：

|-?Px.Translation_CGA_TxPx=mbasis{}-& 1/& 2%Px%mbasis{1}*null_inf

橫向平移表示靜坐標只沿著x軸移動Px.依據定義2平移算子的定義，橫向平移中的mbasis{2}、mbasis{3}分別表示y方向與z方向.橫向平移并未向這兩個方向進行平移，所以它們前面的系數t＄2、t＄3均為零.

定義6.縱向平移

靜坐標沿y軸平移Py，即

(8)

可形式化如下：

|-?Py.Translation_CGA_TyPy=mbasis{}-& 1/& 2%

Py%mbasis{2}*null_inf

同理，定義6也如此.它表示靜坐標沿著y軸平移Py，因此只包括mbasis{2}.

定義7.旋轉公式

靜坐標繞z軸旋轉t，即

Rz=cos(t/2)-(e1∧e2)sin(t/2)

(9)

可形式化如下：

|-?t.Rotation_CGA_Rzt=cos(t/& 2)%mbasis{}-

(mbasis{1}outermbasis{2})*sin(t/& 2)%mbasis{}

旋轉公式表示靜平臺沿著z軸旋轉t.依據旋轉算子、外積的運算性質，可得norm(mbasis{1}outermbasis{2})等于1，可以省略norm(multivecmoutermultivecn)不寫.因此，旋轉算子簡化為上式所示.

定義8.模型的剛體運動算子

該模型的剛體運動算子為

M=TxTyRz

(10)

可形式化如下：

|-?PxPyt.M_CGAPxPyt=Translation_CGA_TxPx*

Translation_CGA_TyPy*Rotation_CGA_Rzt

剛體運動算子就是旋轉和平移的幾何積.本文建立的運動變換等效模型包括兩次平移和一次旋轉，即模型的剛體運動算子表示為它們三者的幾何積.

定理3.剛體運動算子方程

剛體運動算子方程表示如下：

(11)

可形式化如下：

|-?tPxPy.Translation_CGA_TxPx*

Translation_CGA_TyPy*Rotation_CGA_Rxt=

cos(t/& 2)%mbasis{}-

(mbasis{1}*mbasis{2})*sin(t/& 2)%mbasis{}-

(& 1/& 2*Px*cos(t/& 2)+& 1/& 2*Py*

sin(t/& 2))%(mbasis{1}*null_inf)-

(& 1/& 2*Py*cos(t/& 2)-& 1/& 2*

Px*sin(t/& 2))%(mbasis{2}*null_inf)

該式為剛體運動算子方程.通過橫縱向平移、旋轉公式的定義和幾何積等于外積的性質，結合策略SIMP_TAC化簡目標，繼而通過幾何積的自動證明策略CONV_TACGEOM_ARITH自動解算各種積運算的混合表達式實現剛體運動算子方程的證明.

定理4.剛體運動方程的共軛

剛體運動算子方程的共軛表示如下：

(12)

可形式化如下：

|-Reversion(Translation_CGA_TxPx*

Translation_CGA_TyPy*Rotation_CGA_Rxt)=

cos(t/& 2)%mbasis{}+(mbasis{1}*mbasis{2})*

sin(t/& 2)%mbasis{}+(& 1/& 2*Px*cos(t/& 2)+

& 1/& 2*Py*sin(t/& 2))%(mbasis{1}*null_inf)+

(& 1/& 2*Py*cos(t/& 2)

該式剛體運動算子方程的共軛.該定理的證明步驟與定理1、定理2的證明步驟類似.

3.2 建立點運動變換后的表達式方程

首先，先定義平面上的點坐標，即P1、P2、P3在靜坐標下的坐標，P4、P5、P6在動坐標下的坐標；接著，定義點變換的表達式方程，這里會涉及剛體運動算子方程、剛體運動算子方程的共軛.通過點變換的表達式方程，可以得到P4、P5、P6在靜坐標下的坐標.

定義9.平面點坐標方程

在CGA中，點可以寫成

S=s+s2e∞/2+e0

(13)

其中，s=s1e1+s2e2+s3e3，s1、s2、s3為三維歐式空間點的坐標.

可形式化如下：

|-P.point_planeP=P$1%mbasis{1}+P$2%mbasis{2}+(& 1/& 2*(PdotP)%null_inf+null_zero)

該式為平面點的表達式方程.S＄1表示x軸上的系數，即s1；S＄2表示y軸上的系數，即s2.在平面中，點坐標是二維的，只包括x軸和y軸，所以平面中的點只包括mbasis{1}和mbasis{2}.其中，dot是HOLLight中定義的高階邏輯函數，表示向量的點積.

pow是HOLLight中定義的高階邏輯函數，輸入變量是兩個實數x、y，輸出結果是xy，P1、P2、P3在靜坐標中的表示如表2所示，P4、P5、P6在動坐標中的表示如表3所示.

表2 P1、P2、P3在靜坐標中的表達式

定義10.動坐標的點P4、P5、P6在靜坐標xoy的坐標

可形式化如下：

|-?pM_CGA.point_transpM_CGA=M_CGA*p*

(reversionM_CGA)

該式是把動坐標的點轉化為靜坐標下.運用3.1中的剛體運動算子方程M_CGA可以得到動坐標的點P4、P5、P6在靜坐標下所對應的坐標.

表3 P4、P5、P6在動坐標中的表達式

3.3 建立桿長約束方程

上面已經得到了每個點在靜坐標下所對應的坐標.接下來需要根據各支鏈的桿長約束方程，建立點與點的約束方程，把點與點建立關系.

定義11.桿長約束方程

內積與距離的表達式方程：

P·S=-(s-p)2/2

(14)

可形式化如下：

|-get_square_qab=-& 2%(ainnerb)

根據2個點P、S的內積與距離的關系，建立桿長約束方程，該方程表示2個點P、S的內積與距離的關系.這里的get_square_qab指的是a與b兩點實際距離的平方.

定義12.P1、P4約束方程

可形式化如下：

|-?PxPy.-& 2%

(point_plane_P1innerpoint_plane_P4PxPy)=

get_square_qpoint_plane_P1(point_plane_P4PxPy)

定義13.P2、P5約束方程

可形式化如下：

|-?tPxPyP2xP5x.-&2%(point_plane_P2P2x)inner

(point_trans(point_plane_P5P5x)(M_CGAPxPyt))=

get_square_q(point_plane_P2P2x)(point_trans

(point_plane_P5P5x)(M_CGAPxPyt))

定義14.P3、P6約束方程

可形式化如下：

|-?tPxPyP3xP6xP3yP6y.-& 2%

(point_plane_P3P3xP3yinner(point_trans

(point_plane_P6(P6x：real)(P6y：real))

(M_CGA(Px：real)(Py：real)(t：real))))=

get_square_q(point_plane_P3P3xP3y)

(point_trans(point_plane_P6P6xP6y)

(M_CGAPxPyt))

3.4 建立位置正解封閉方程組

結合點運動變換后的表達式方程和桿長約束方程，建立位置正解封閉方程組.

(Px)2+(Py)2=(q1)2

(15)

(Px)2+(Py)2+(P2x)2+(P5x)2-2(P2xP5x-PxP5x)cosθ+2P5xPysinθ-2PxP2x=(q2)2

(16)

(Px)2+(Py)2+(P3x)2+(P3y)2+(P6x)2+(P6y)2+

2(PyP6y+PxP6x-P3xP6x-P3yP6y)cosθ+

2(PyP6x-P3yP6x-PxP6y+P3xP6y)sinθ-

2PyP3y-2PxP3x=(q3)2

(17)

定理5.P1、P4封閉方程

可形式化如下：

|-?PxPy.Pxpow2%mbasis{}+Pypow2%mbasis{}=

get_square_qpoint_plane_P1(point_plane_P4PxPy)

定理6.P2、P5封閉方程

可形式化如下：

|-?tPxPyP2xP5x.Pxpow2%mbasis{}+Pypow2%mbasis{}+P2xpow2%mbasis{}+P5xpow2%mbasis{}-

& 2%(P2x*P5x-Px*P5x)%cost%mbasis{}+

& 2%P5x%Py%sint%mbasis{}-

& 2%(Px*P2x)%mbasis{}=

get_square_q(point_plane_P2P2x)

(point_trans(point_plane_P5P5x)(M_CGAPxPyt))

定理7.P3、P6封閉方程

可形式化如下：

|-?tPxPyP3P6P3xP6xP3yP6y.Pxpow2%mbasis{}+

Pypow2%mbasis{}+P3xpow2%mbasis{}+

P3ypow2%mbasis{}+P6xpow2%mbasis{}+

P6ypow2 %mbasis{}+& 2%(Py*P6y+

Px*P6x-P3x*P6x-P3y*P6y)%cost%mbasis{}+

& 2% (Py*P6x-P3y*P6x-Px*P6y+P3x*P6y)%

sint%mbasis{}-& 2%(Py*P3y)%mbasis{}-

& 2%(Px*P3x)%mbasis{}=

get_square_q(point_plane_P3P3xP3y)

(point_trans(point_plane_P6P6xP6y)(M_CGAPxPyt))

定理5-定理7是平面并聯機構等效模型的位置正解封閉方程組，其中t，Px，Py為待求量，其余變量都為已知機構參數.利用約束方程替換封閉方程，繼而使用策略將點的表達式方程重寫，通過化簡得到位置正解封閉方程組，實現封閉方程組到二元一次方程組的變換，進而推導出一元六次方程.

3.5 封閉方程組的消簡過程的形式化驗證

驗證平面并聯機構位置正解方程與一元六次方程的等價性證明.結合P1、P4封閉方程、P2、P5封閉方程、P3、P6封閉方程得到Px、Py的二元一次方程組.

APx+BPy+D=0EPx+CPy+G=0

(18)

其中，

A=2P5xcosθ-2P2x

B=2P5xsinθ

C=2P6ycosθ+2P6xsinθ-2P3y

D=(q1)2-(q2)2+(P2x)2+(P5x)2-2P2xP5xcosθ

E=2P6xcosθ-2P6ysinθ-2P3x

G=(q1)2-(q3)2+(P3x)2+(P3y)2+(P6x)2+(P6y)2-2(P3xP6x+P3yP6y) cosθ+2(P3xP6y-P3yP6x) sinθ

為了簡化后面代碼的形式化描述，A～G的形式化表示如下：

A=& 2*P5x*cost-& 2*P2x∧

B=& 2*P5x*sint∧

C=& 2*P6y*cost+& 2*P6x*sint-& 2*P3y∧

D=get_square_qpoint_plane_P1(point_plane_P4Px

Py)-get_square_q(point_plane_P2P2x)

(point_trans(point_plane_P5P5x)(M_CGAPxPyt))+

P2xpow2%mbasis{}+P5xpow2%mbasis{}-

(& 2*P2x*P5x*cost)%mbasis{}∧

E=& 2*P6x*cost-& 2*P6y*sint-& 2*P3x∧

G=get_square_qpoint_plane_P1

(point_plane_P4PxPy)-get_square_q

(point_plane_P3P3xP3y)

(point_trans(point_plane_P6P6xP6y)(M_CGAPxPyt))+(P3xpow2+P3ypow2+P6xpow2+P6ypow2-& 2*(P3x*P6x+P3y*P6y)*cost+& 2*

(P3x*P6y-P3y*P6x)*sint)%mbasis{}

定理8.關于Px、Py方程組

可形式化如下：

|-?PxPyABD.

(A*Px)%mbasis{}+(B*Py)%mbasis{}+D=vec0

|-?PxPyCEG.

(E*Px)%mbasis{}+(C*Py)%mbasis{}+G=vec0

其中，vec0表示的是零向量.上式是Px、Py的二元一次方程組.結合封閉方程的定義square_q1、square_q2、square_q3，得到Px、Py的二元一次方程組.

Px、Py關于t的表達式如下：

(19)

定理9.Px關于t的表達式

可形式化如下：

|-?ABCDEG.

((A*C-B*E)*Px)%mbasis{}=B%G-C%D

該式為Px關于t的表達式方程.對二元一次方程組進行消元，消去Py，得到定理9.利用移項化簡實現邏輯推理.

定理10.Py關于t的表達式

可形式化如下：

|-?ABCDEG.

((A*C-B*E)*Py)%mbasis{}=E%D-A%G

同理，消去Px，得到Py關于t的表達式.該定理的證明步驟與定理9的證明步驟類似.當A*C-B*E等于零時，表示該機構為退化構型，而本文討論的是非退化構型，也就是本文只討論A*C-B*E不為零的情況.

定理11.一元三次方程

其數學描述如下：

r1(cosθ)3+r2sinθ(cosθ)2+r3(cosθ)2+r4(sinθcosθ)+r5cosθ+r6sinθ+r7=0

(20)

可形式化如下：

|-?r1r2r3r4r5r6r7ABDECG.

～(A*C-B*E=& 0)?r1=E1∧r2=E2∧

r3=E3∧r4=E4∧r5=E5∧r6=E6∧r7=E7

?(r1*costpow3+r2*sint*costpow2)%mbasis{}+

costpow2%r3+(sint*cost)%r4+cost%r5+

sint%r6+r7=vec0

r1～r7是與機構參數相關的常數，它是通過Maple16編程軟件實現的.系數特別復雜因此很難使用傳統的方法進行驗證.該式是關于θ的方程，包含sinθ和cosθ.結合策略把Px關于t的方程、Py關于t的方程重寫到P1、P4封閉方程square_q1中.在運算過程中，等號右邊出現了cos4θ和sinθcos3θ，而等式左邊不包含這兩項，因此需要驗證cos4θ和sinθcos3θ前面的系數為0，進而消去這兩項.

引理1.a與其倒數相乘等于1(a不等于0)

可形式化如下：

|-?t.inv(& 1+tan(t*inv(& 2))*tan(t*inv(& 2)))

*(& 1+tan(t*inv(& 2))*tan(t*inv(& 2)))=& 1

其中，inv是HOL Light中定義的高階邏輯函數，函數的輸入變量是實數，輸出結果是該實數的倒數，且定義0的倒數仍然為0.當a不等于0時，它與其倒數相乘等于1.這里a=&1+tan(t*inv(& 2))*tan(t*inv(& 2))，因為a不等于零，所以它與其倒數相乘才等于1.為了證明定理12，需要結合該引理輔助證明.

定理12.一元六次方程

其數學描述如下：

w6t6+w5t5+w4t4+w3t3+w2t2+w1t+w0=0

(21)

式中，w0=r1+r3+r5+r7w1=2(r2+r4+r6)

w2=-3r1-r3+r5+3r7w3=4(-r2+r6)

w4=3r1-r3-r5+3r7w5=2(r2-r4+r6)

w6=-r1+r3-r5+r7

可形式化如下：

|-?tr1r2r3r4r5r6r7E1E2E3E4E5E6E7

w1w2w3w4w5w6w0.

r1=E1∧r2=E2∧r3=E3∧r4=E4∧

r5=E5∧r6=E6∧r7=E7

?

w1=& 2%(r2%mbasis{}+r4+r6)∧

w2=(-& 3*r1)%mbasis{}-r3+r5+& 3%r7∧

w3=& 4%(-r2%mbasis{}+r6)∧

w4=(& 3*r1)%mbasis{}-r3-r5+& 3%r7∧

w5=& 2 %(r2%mbasis{}-r4+r6)∧

w6=-r1%mbasis{}+r3-r5+r7∧

w0=r1%mbasis{}+r3+r5+r7∧

～(cos(t/& 2)=& 0)

?

tan(t/& 2)pow6%w6+tan(t/& 2)pow5%w5+

tan(t/& 2)pow4%w4+tan(t/& 2)pow3%w3+

tan(t/& 2)pow2%w2+tan(t/& 2)%w1+

w0=vec0

4 總 結

平面并聯機構是機構運動學研究的一部分，它的分析、求解一直廣受學者們的關注.在平面并聯機器人的求解過程中，CGA方法具有幾何概念清楚、物理意義清晰、表達形式簡潔的優點，極大地降低了機器人運動學研究的難度.本文以幾何代數、CGA為數學基礎，在高階邏輯定理證明器HOL Light中，對平面并聯機構建立模型并進行形式化驗證，從而確保了算法的安全性和可靠性.本文中的形式化工作，不僅能填補驗證在并聯機構中的空白，而且為我們以后的相關工作奠定了基礎，也為以后算法的驗證積累了豐富的經驗.此外，并聯機構不僅包括平面并聯機構，還包括空間并聯機構.因此下一步工作將圍繞基于共形幾何代數理論的空間并聯機構的形式化建模與驗證展開.