1樓：午時葵
實名反對本答案之前出現的幾乎所有文字，明明啥都不懂還在那一直瞎說。
清華的紫皮爛書嘴裡的「王浩演算法」其實就是sequent calculus系統 ，因為 裡的規則是 invertible 的可以拿來倒著寫做證明搜尋，這事是王浩第乙個說的所以叫王浩演算法。「公式串」的意思和公式是大不一樣的，書上有寫前件大合取後件大析取，別的直觀解釋不知道有沒有寫，書不在手頭沒法確認，那我就給題主解釋一下。
乙個sequent 除了能讀成 之外，更正常的讀法是 裡裝著一堆前提， 裡裝著一堆結論， 代表有乙個證明說只要前提都滿足，結論至少有乙個滿足。更不嚴謹一點的說法是 是在對你的結論提要求， 是在給你的結論提供可能。那乙個空的前件 就是不提任何要求，相當於乙個真命題，整個sequent的意思是沒有前提的情況下 裡有乙個是真的，如果 裡只有乙個命題 那這就是在說 是重言式。
反過來，乙個空的後件 是不給你任何可能的結論，相當於乙個假命題，整個sequent的意思是通過前提 能推出矛盾，也就是 是不一致的意思。
這兩個東西為空的情況是至關重要，且必不可少的，並不是什麼corner case。並且它們不是什麼理論的輸入輸出，而就是sequent calculus推理過程中出現的自然狀態。王浩演算法的意思是你給我乙個sequent作為整體然後我去以它為結論倒著寫證明，如果我要的就是乙個重言式 的證明那翻譯到這個系統裡待證sequent就是 。
當然，說它是單位元是沒問題的，因為乙個翻譯過來是 乙個是 。
sequent calculus還有很多相關的直觀，包括前/後件極性相反變號翻轉之類的，建議題主換一本靠譜的證明論書籍，比如von Plato的Elements of Logical Reasoning，清華這本紫皮爛到令人髮指。
2樓：
空符號串成立只是為了給群加乙個零元而已，這樣定義就完備了。
就像字串型別，如果空字串不是字串，那麼你這個類的定義會很尷尬的。首先它就沒有乙個初始化狀態。
3樓：哲學為何p開頭
1、空符號串也是公式串？
2、我不知道這本書是說哲學還是說數學，當然，對於王浩來說兩者可以同等，但對於漢譯者卻不一定啦！
3、如果漢譯把其作為數理邏輯哲學，「空符號串也是公式串」這話要看原文，否則我只能就我知道的邏輯學原理，或者說西方哲學史的本體論第二階段說這事兒：
4、西方中世紀宗教哲學，波菲力有 V 全稱或 V 謂項之說，到了所謂 r 唯實論 m，他們推論的結果就是OoOoO 這 V 空圈串，大寫O本體實體o小寫；
5、也就是-神間天堂 Paradises 人間天堂-相結合， 在唯名 n 論看來 m，其間應該 dise 實心圓，但 r 唯實論 m 卻推成了空心圓，所以他們表示 dis 小瞧這種本體論。
6、王浩是說這件事麼？不可知也，供參考吧？
4樓：RaySir
至於你問題中與空串無關的部分，我覺得沒得啥子意思；當然也有自己回答不了的原因：那個前AI時代——可能現在的AI時代亦然——留下了太多雞肋理論。現在去拾起，有點自尋煩惱的意味：
比方說這個這個什麼自動證明、自動解析中一大堆基於字串的標記、特徵化，拿起一本《編譯原理》或部分地去實現1個編譯器就可以將它們拋在螢幕後面。
符號系統——使用借助思維理論——可以表明：就1助記功能，而非本徵。或者說，把它們理解為當時的人們理解的那就是邏輯，而不是邏輯就應該是它們VED存在之樣子。
5樓：
瀉藥不懂王浩系統，也不懂自動證明，姑且一答：
既然是自動證明，那麼就需要從機器的角度看問題。對於機器而言，乙個空輸入未必不合法，未必不能返回乙個結果，所以「空串」同樣是機器需要加以處理的「物件」。所謂「自動證明」，就是一套由輸入的符號串（合適公式或者不是合式公式），經過運算，得到輸出結果的演算法，而這個輸出結果是乙個證明或者演繹序列（如果這個證明或演繹存在的話）。
具體到此處王浩的系統，規則中用希臘字母表示的主目都是可以代入空串的。
你可以設想以下，如果「規則」的應用不允許相應的主目（希臘字母所佔的位置）為空串，那麼滿足同樣的演繹功能，需要加多少條規則，數目很可能很大，甚至可能造成表達上的不完全。
符號串，空串這組概念，實際是代數概念，「自由群」，「自由代數」可以適當了解一下。
宇宙是不連續的，那為什麼微積分可以成立？
棄墨 宇宙必然有最小畫素小於蒲朗克尺度一下沒有物理價值 如果宇宙的物質可以無限分割最後會得到乙個什麼東西？肯定不是乙個立體的東西只能像點一樣的基本畫素那你怎麼反向操作才能讓其恢復原樣？點這種沒有維度的東西無論怎麼疊加依舊沒有維度 境者無界 因為數學已經假設線面是連續的了，就跟宇宙是不是連續毫無關係了...
為什麼從緣起性空可以得到諸惡莫作，眾善奉行，是不是法爾如是
普波居士 佛法修行，有很多修行方法和義理。緣起性空是說諸法不可得性。是講的緣起法。諸惡莫作，諸善奉行，自淨其意，是諸佛教。是從善惡因果上來講的。法爾如是是講的諸法如實義。無二是消除我執的分別妄想心。 Matrix 不要忘了佛法的目標，所有的修行努力和方法都是為這個目標服務的，跟做其他事情一樣，不為了...
C語言字元指標（字串）為什麼不可以直接像陣列那樣賦值？
check 777 直接定義乙個指標陣列不就行了，char a 3 tika64208 這個問題好理解，char str申請的是陣列，char p 申請的是乙個指標。而是什麼，是乙個具體的值，或者說3個具體的值，在編譯的時候就已經知道的值。你申請了4個元素的陣列，說裡面要存3個指定的值，叫分別是 a...