謂詞邏輯與歸結原理的一些概念題
答案均取自網絡或是書本的理解修改整理
什么是合取范式和析取范式？
合取范式：僅由有限個簡單析取式構成的合取式稱為合取范式，即單元子句、單元子句的或的與
析取范式：僅由有限個簡單析取式構成的析取式稱為析取范式，即單元子句、單元子句的與的或
關於判斷的話，簡單來說，只要看式子中連接的每一項的連接詞是∧還是∨，連接詞是∧則式子為合取范式，為∨是析取范式
例如：(A∨B∨C)∧(┐A∨┐B∨┐C)∧(A∨┐B∨C)是合取范式，而(A∧B∧C)∨(┐A∧┐B∧┐C)∨(┐A∧B∧C)是析取范式
什么是子句集？子句集的求取過程？
沒有變元的原子公式，即基礎原子公式，簡稱“基原子”，其中，原子公式以及它的否定形式都是文字，不包含變元的文字即基礎文字，可以稱為基文字，文字以及它們的析取，都稱為子句，由子句構成的集合就叫做子句集
子句集的求取過程:
1.將謂詞公式轉換成前束范式
2.消去前束范式中的存在量詞，略去其中的任意量詞，生成Skolem標准型
3.將Skolem標准型中的各個子句提出，表示為集合形式
什么叫歸結？
歸結原理是1965年美國人Robinson提出的一種證明一階謂詞演算中定理的方法
在使用這種方法的時候，我們對任意的一個要證明的永真公式取非后，要想辦法證明它不滿足，為此我們可以先轉化成一種標准型，然后我們對這個標准型不斷的使用單一的推理規則，即實行歸結，直到最后得到矛盾的結果，說白了就是一種證明方式
在命題邏輯中，歸結法的邏輯基礎是什么？
什么是命題？命題就是能判斷真假的陳述句，單個常量或者是變量的命題，稱為合式公式，而由合式公式有限個次數構成的字符串，稱為命題公式
而命題邏輯是指以邏輯運算符結合原子命題來構成代表“命題”的公式，以及允許某些公式構成定理的一套形式證明規則，相對於謂詞邏輯，它是量化的，並且它的原子公式是謂詞函數
歸結方法是1965年提出的一種證明方法，它依賴於一個單一的規則，即如果pVq和～qVr都為真,則pVr為真
此規則可以由真值表證明是正確的，因為依賴於一個單一的、簡單的規則，歸結方法是許多進行推理和證明定理的基礎，歸結原理的理論基礎是Herbrand定理，其基本思想就是將待證明邏輯公式的結論，通過等值公式轉換成附加前提，再證明該邏輯公式是不可滿足的
什么樣的命題可以由歸結法來證明？
感覺需要說到歸結方法的完備性
如果有A→B成立，那么歸結討程將能夠歸結出空子句，因而，可以說歸結方法是完備的
需要注意的是，當邏輯公式中含有等號時，歸結方法的完備性將被破壞
由此可見，完備性是有條件的，那么如果A→B不成立，使用歸結方法得不到任何結論，最終可以認為歸結方法是半完備的
謂詞邏輯和命題邏輯的區別和聯系？
命題邏輯顯然可以看作謂詞邏輯的一個子集，因為謂詞邏輯中一般是允許出現0元謂詞的，全部由0元謂詞的構成的公式就是命題邏輯公式了
當論域為一個大小確定的有限集時，一個謂詞公式可以等價地轉化成一個命題邏輯公式，當不特別說明論域或論域的大小不是一個確定的自然數時，就不存在一般的轉化方法了
簡單地說，謂詞邏輯就是加了"量詞運用規則"的命題邏輯，也就是說，謂詞邏輯，是將命題邏輯表達不出來的邏輯繼續細化以后的結果
怎么才能判斷一個一階謂詞邏輯公式為永真或永假？
一階謂詞邏輯中，使用解釋的方法，就可以判定一個公式的真假
而解釋就是個體詞在個體域中指定是哪個個體，給謂詞指定具體的性質或關系，給量詞指定個體域判定其范圍，那么在確定了個體詞，謂詞，量詞以后，就可以判定真假了
那么可以知道，一個謂詞公式在所有解釋下都是真值，則稱這個謂詞公式是邏輯有效的或是永真的，而一個謂詞公式在所有解釋下都是假值，則稱這個謂詞公式是不一致的或是不可滿足的的（永假）
如果是計算機進行判定，應該怎么進行？
寫個程序？不太清楚
什么叫歸結策略？歸結策略的目的是什么？
通過給出控制策略，以使系統僅選擇合適的子句對其做歸結來避免多余不必要的歸結式的出現，或者說少做一些歸結但仍然導出空子句，提高歸結效率，是很重要的
歸納起來，歸結過程策略控制的要點有:
1.要解決的問題是歸結方法的知識爆炸
2.控制策略的目的是歸結點盡量少
3.控制策略的原則是刪除不必要的子句，或對參加歸結的子句加以限制
4.給出控制策略，以便僅選擇合適的子句對其做歸結，避免多余的、不必要的歸結式出現
總結Herbrand定理和歸結法之間的關系？
Herbrand定理是歸結原理的理論基礎，歸結原理的正確性是通過Herbrand定理來證明的，同時歸結原理是Herbrand定理的具體實現，利用Herbrand定理對公式的證明是通過歸結法來進行的
具體來說就是，Herbrand定理是歸結法的基礎，是歸結原理完備性的保證
雖然Herbrand定理通過構造在H域上的語義樹來判斷一個謂詞邏輯命題是否為永真，從而實現了將謂詞邏輯轉化成為命題邏輯判定問題，為歸結原理提供了實現的塗徑，最終還是歸結原理使Herbrand定理成為現實可用的存在
