求真百科歡迎當事人提供第一手真實資料,洗刷冤屈,終結網路霸凌。

合式公式檢視原始碼討論檢視歷史

事實揭露 揭密真相
前往: 導覽搜尋
合式公式
圖片來自人人網圖片

合式公式,又稱謂詞公式,是一種形式語言表達式,即形式系統中按一定規則構成的表達式。按照模型論中一種通行習慣,語言F中的合式公式定義如下:1.原子公式是合式公式; 2.若φ和ψ是合式公式,則(φ∧ψ)及(ᒣφ)是合式公式; 3.若φ是合式公式,而x是變元,則(ᗄx)φ是合式公式;4.有限次地應用1—3所得到的符號序列是合式公式。合式公式有時簡稱公式,如果一個公式φ中的自由變元都屬於集合{x₁,x₂,…,xₑ},則φ也可以記為φ(x₁,x₂,…,xₑ),不含量詞、自由變元的合式公式,分別稱為開公式和閉公式,後者又稱語句,例如R(x,y)為開公式,ᗄxR(x)是一個語句,由原子公式及聯結詞∧,∨,ᗄ,∃構成語句 稱為正語句。

什麼是合式公式?

(1)原子命題常項或變項是合式公式;

(2)如果A是合式公式,則(-A)也是合式公式(- 表示非);

(3)如果A,B是合式公式,則(A*B)、(A+B)、(A < B)、( A ~ B)也是合式公式;(此處 * 合取 + 析取 < 代表條件 ~ 代表雙條件)

(4)只有有限次地應用(1)~(3)所包含的命題變元,聯結詞和括號的符號串才是合式公式。

個人思路QAQ:

用字符串輸入(注意輸入格式:在字符串首尾手動加括號),依次掃描字符串,遇到「非法」字符跳出循環,字符串能夠掃描完則為真

時間複雜度:O(n) 數據不大時,可以在1秒內完成

「非法」字符

(1)(*P) (+P) (<P) (~P)

(2) (P-)

(3) RT (兩個大寫字母)

(4) 括號不匹配

程序中可能會有bug,希望大佬們多多指教

這道題用遞歸的話,應該會更好,但我不會用,只能暴力判斷了[1]

一階邏輯中合式公式,被遞歸定義如下:

(1)原子是合式公式;

(2)若A是合式公式,則(

)也是合式公式;

(3)若A,B是合式公式,則

也是合式公式;

(4)若A是合式公式,也是合式公式;

(5)只有限次地使用(1)~(4)所生成的符號串才是合式公式。

合式公式,也稱謂詞公式,簡稱為公式,為簡便起見,公式的最外層括號可以省去。對於一個謂詞,如果其中每一個變量都在一個量詞作用之下,則它就不再是命題函數,而是一個命題了。但是,這種命題和命題邏輯中的命題還是有區別的,因為這種命題中畢竟還有變量,儘管這種變量和命題函數中的變量有所不同,因此,有必要區分這些變量。

相關知識

為了使一階邏輯中命題符號化更準確和規範,以便正確進行謂詞演算和推理,引進一階邏輯中合式公式的概念.

在形式化中,將使用以下四類符號。

(1)常量符號:當論域D給出時,它可以是D中的某個元素;

(2)變量符號:當論域D給出時,它可以是D中的任何一個元素;

(3)函數符號::的任意一個映射;

(4)謂詞符號:到{1,0}的任意一個謂詞。

定義1一階邏輯中的項(item),被遞歸定義如下:

(1)常量符號是項;

(2)變量符號是項;

(3)若是項;

(4)只有有限次地使用(1)、(2)、(3)所生成的符號串才是項。

例如a,b,x,y是項,也是項。

定義2設為原子公式,或簡稱原子。

約束變量和自由變量

在一個謂詞公式中,變量的出現是約束的(bound),當且僅當它出現在使用這個變量的量詞作用範圍(稱為作用域)之內;變量的出現是自由的(free),當且僅當它的出現不是約束的;至少有一次約束出現的變量稱為約束變量(bound variable),至少有一次自由出現的變量稱為自由變量(free variable)。

例如,公式中的x的出現是約束的。而謂詞R(x)中x的出現是自由的。另外,公式中y和z的出現也是自由,因此,x既是約束變量,又是自由變量,而y,z僅僅是自由變量。由此可知,公式中的某個變量既可以是約束變量,同時也可以是自由變量。此外,顯然有

也即,一階邏輯中命題的真值,與其約束變量的記號無關。

為了避免公式中有些變量既可以約束出現,又可自由出現的情形,我們可採用以下兩條規則。

改名規則:將謂詞公式中出現的約束變量改為另一個約束變量,這種改名必須在量詞作用域內各處以及該量詞符號中進行,並且改成的新約束變量要有別於改名區域中的所有其他變量。

代替規則:對公式中某變量的所有自由出現,用另一個與原公式中的其他變量符號均不同的變量符號去代替。

例如,對於公式,可使用改名規則,將約束出現的x改成u,得

或者使用代替規則,將自由出現的x用u代替,得

這樣,對一階邏輯中的任何公式,總可以通過改名規則或代替規則,使該公式中不出現某變量既是約束變量又是自由變量的情形。

由謂詞公式的定義可知,若不對其中的常量符號、變量符號、函數符號和謂詞符號給以具體解釋,則公式是沒有實在意義的。

公式解釋

定義 在一階邏輯中,公式G的一個解釋

,是由非空論域D和對G中常量符號、函數符號、謂詞符號按下列規則進行一組指定所組成:

(1)對每個常量符號,指定D中的一個元素;

(2)對每個n元函數符號,指定一個函數,即指定一個

到D的映射;

(3)對每個n元謂詞符號,指定一個謂詞,即指定一個

到{0,1}上的一個映射。

為統一起見,對所討論的公式作如下規定:公式中無自由變量,或者將自由變量看作常量。於是,每個公式在任何具體解釋下總表示一個命題。

公式分類

設G是一個謂詞公式,

(1)如果存在解釋是可滿足的;

(2)如果所有解釋為恆假的,或不可滿足的;

(3)如果為恆真的。

如果一階邏輯中的恆真(恆假)公式,要求所有解釋依賴一個非空個體集合D,又集合D可以是無窮集合,而集合D的「數目」也可以有無窮多個,因此,所謂公式的「所有」解釋,實際上是很難考慮的,這就使得一階邏輯中公式的恆真、恆假性的判定異常困難。Church和Turing分別於1936年獨立地證明了:對於一階邏輯,判定問題是不可解的,即不存在一個統一的算法A,該算法與謂詞公式無關,使得對一階邏輯中的任何謂詞公式G,A能夠在有限步內判定公式G的類型。

但是,一階邏輯是半可判定的,即如果謂詞公式G是恆真的,有算法在有限步內檢驗出G的恆真性。

參考來源