基于高階邏輯的交叉算子的形式化研究.pdf

1、隨著計(jì)算機(jī)系統(tǒng)規(guī)模的迅速增大，系統(tǒng)設(shè)計(jì)實(shí)現(xiàn)的正確性問(wèn)題越來(lái)越嚴(yán)峻。形式化方法的出現(xiàn)，成為了解決該問(wèn)題的一個(gè)重要手段。它運(yùn)用數(shù)學(xué)方法的特點(diǎn)相比于傳統(tǒng)的模擬和測(cè)試具有更高的可靠性和良好的完備性。其中，定理證明的方法因其既能驗(yàn)證系統(tǒng)規(guī)范又不受系統(tǒng)規(guī)模的限制而備受關(guān)注。遺傳算法被越來(lái)越多的應(yīng)用在安全性要求較高的領(lǐng)域，然而定理證明器中還未有形式化的遺傳算法，這就限制了形式化方法在相關(guān)領(lǐng)域的應(yīng)用。因此，將遺傳算法形式化在HOL4系統(tǒng)中對(duì)擴(kuò)展定理證明

2、方法的應(yīng)用領(lǐng)域具有重要的研究意義和實(shí)用價(jià)值。
　　眾所周知，遺傳算法的求解能力取決于最關(guān)鍵的操作——交叉算子。因此，本文對(duì)應(yīng)用最多的單點(diǎn)交叉和多點(diǎn)交叉進(jìn)行了形式化。首先，本文采用高階邏輯的方法對(duì)交叉算子進(jìn)行了形式化分析，從而定義交叉算子生成子代的過(guò)程為交叉操作。通過(guò)對(duì)交叉操作的形式化抽象，提取了交叉操作的基本組成元素。這些基本元素組成了交叉操作的一般化模型，并使用高階邏輯表示基本組成元素。基于一般化結(jié)構(gòu)模型，使用雙遞歸的方法提出了

3、交叉操作的形式化模型，并用數(shù)學(xué)的方法描述了此模型。然后，使用形式化的交叉操作分別完成了單點(diǎn)交叉算子和多點(diǎn)交叉算子的形式化，并使用支持高級(jí)證明步驟、重寫(xiě)對(duì)策和自動(dòng)推理證明了交叉算子的性質(zhì)。同時(shí)，交叉算子性質(zhì)的證明充分保證了本文形式化的交叉算子的正確性。最后，為了說(shuō)明形式化的交叉算子的實(shí)用性，用形式化的交叉算子設(shè)計(jì)了一個(gè)遺傳算法，用來(lái)求解機(jī)器人在運(yùn)動(dòng)空間的最優(yōu)避碰路徑。此應(yīng)用為HOL4中設(shè)計(jì)遺傳算法程序提供了一個(gè)有效的實(shí)例。
　　將交