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

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

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

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