http://wiki.huihoo.com/wiki/?action=history&feed=atom&title=Formal_verification 2026-06-25T00:33:09Z 本wiki的该页面的版本历史 MediaWiki 1.19.2 http://wiki.huihoo.com/wiki/?title=Formal_verification&diff=167240&oldid=prev 2025-01-07T08:42:27Z

<p>‎<span dir="auto"><span class="autocomment">项目</span></span></p> <table class='diff diff-contentalign-left'> <col class='diff-marker' /> <col class='diff-content' /> <col class='diff-marker' /> <col class='diff-content' /> <tr valign='top'> <td colspan='2' style="background-color: white; color:black;">←上一版本</td> <td colspan='2' style="background-color: white; color:black;">2025年1月7日 (二) 08:42的版本</td> </tr><tr><td colspan="2" class="diff-lineno">第103行：</td> <td colspan="2" class="diff-lineno">第103行：</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>[[文件:vellvm-logo.jpg|right|Vellvm]]</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>[[文件:vellvm-logo.jpg|right|Vellvm]]</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>[[文件:key-logo.png|right|KeY]]</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>[[文件:key-logo.png|right|KeY]]</div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins style="color: red; font-weight: bold; text-decoration: none;">*[https://github.com/ElNiak/awesome-formal-verification Awesome Formal Verification] [[文件:awesome.png]]</ins></div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://github.com/awesomo4000/awesome-provable Provably Awesome] [[文件:awesome.png]] &#160;</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://github.com/awesomo4000/awesome-provable Provably Awesome] [[文件:awesome.png]] &#160;</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://awesomeopensource.com/projects/proof-assistant Proof Assistant Open Source Projects on Github]</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://awesomeopensource.com/projects/proof-assistant Proof Assistant Open Source Projects on Github]</div></td></tr> </table>

Allen http://wiki.huihoo.com/wiki/?title=Formal_verification&diff=166918&oldid=prev 2023-08-03T23:57:42Z

<p>‎<span dir="auto"><span class="autocomment">语言</span></span></p> <table class='diff diff-contentalign-left'> <col class='diff-marker' /> <col class='diff-content' /> <col class='diff-marker' /> <col class='diff-content' /> <tr valign='top'> <td colspan='2' style="background-color: white; color:black;">←上一版本</td> <td colspan='2' style="background-color: white; color:black;">2023年8月3日 (四) 23:57的版本</td> </tr><tr><td colspan="2" class="diff-lineno">第83行：</td> <td colspan="2" class="diff-lineno">第83行：</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>[[文件:FStarLang-logo.png|right|FStarLang]]</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>[[文件:FStarLang-logo.png|right|FStarLang]]</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*在数学、逻辑和计算机科学中，形式语言（[[Formal language]]）是用精确的数学或机器可处理的公式定义的语言。</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*在数学、逻辑和计算机科学中，形式语言（[[Formal language]]）是用精确的数学或机器可处理的公式定义的语言。</div></td></tr> <tr><td class='diff-marker'>−</td><td style="background: #ffa; color:black; font-size: smaller;"><div>*[[F*]]</div></td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div>*[[F*]<ins class="diffchange diffchange-inline">] [https://github.com/dafny-lang/dafny Dafny</ins>]</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[[Haskell]] [[Agda]] [[Idris]] 具有“证明即程序、命题为类型”的特征。[https://github.com/plclub/hs-to-coq hs-to-coq] import [[Haskell]] to Coq, [https://github.com/nick8325/jukebox/ jukebox] A theorem prover</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[[Haskell]] [[Agda]] [[Idris]] 具有“证明即程序、命题为类型”的特征。[https://github.com/plclub/hs-to-coq hs-to-coq] import [[Haskell]] to Coq, [https://github.com/nick8325/jukebox/ jukebox] A theorem prover</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[[OCaml]] [[Coq]] [https://github.com/formal-land/coq-of-ocaml coq-of-ocaml] 可做两件事：1、do formal proofs on OCaml programs; 2、port OCaml projects to Coq.</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[[OCaml]] [[Coq]] [https://github.com/formal-land/coq-of-ocaml coq-of-ocaml] 可做两件事：1、do formal proofs on OCaml programs; 2、port OCaml projects to Coq.</div></td></tr> </table>

Allen http://wiki.huihoo.com/wiki/?title=Formal_verification&diff=166306&oldid=prev 2022-10-28T03:24:11Z

<p>‎<span dir="auto"><span class="autocomment">语言</span></span></p> <table class='diff diff-contentalign-left'> <col class='diff-marker' /> <col class='diff-content' /> <col class='diff-marker' /> <col class='diff-content' /> <tr valign='top'> <td colspan='2' style="background-color: white; color:black;">←上一版本</td> <td colspan='2' style="background-color: white; color:black;">2022年10月28日 (五) 03:24的版本</td> </tr><tr><td colspan="2" class="diff-lineno">第82行：</td> <td colspan="2" class="diff-lineno">第82行：</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>[[文件:purely-functional-programming.png]]</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>[[文件:purely-functional-programming.png]]</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>[[文件:FStarLang-logo.png|right|FStarLang]]</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>[[文件:FStarLang-logo.png|right|FStarLang]]</div></td></tr> <tr><td class='diff-marker'>−</td><td style="background: #ffa; color:black; font-size: smaller;"><div>*在数学、逻辑和计算机科学中，形式语言（[<del class="diffchange diffchange-inline">https://en.wikipedia.org/wiki/Formal_language </del>Formal language]）是用精确的数学或机器可处理的公式定义的语言。</div></td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div>*在数学、逻辑和计算机科学中，形式语言（[<ins class="diffchange diffchange-inline">[</ins>Formal language<ins class="diffchange diffchange-inline">]</ins>]）是用精确的数学或机器可处理的公式定义的语言。</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[[F*]]</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[[F*]]</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[[Haskell]] [[Agda]] [[Idris]] 具有“证明即程序、命题为类型”的特征。[https://github.com/plclub/hs-to-coq hs-to-coq] import [[Haskell]] to Coq, [https://github.com/nick8325/jukebox/ jukebox] A theorem prover</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[[Haskell]] [[Agda]] [[Idris]] 具有“证明即程序、命题为类型”的特征。[https://github.com/plclub/hs-to-coq hs-to-coq] import [[Haskell]] to Coq, [https://github.com/nick8325/jukebox/ jukebox] A theorem prover</div></td></tr> </table>

Allen http://wiki.huihoo.com/wiki/?title=Formal_verification&diff=166286&oldid=prev 2022-10-26T15:39:26Z

<p>‎<span dir="auto"><span class="autocomment">机器证明</span></span></p> <table class='diff diff-contentalign-left'> <col class='diff-marker' /> <col class='diff-content' /> <col class='diff-marker' /> <col class='diff-content' /> <tr valign='top'> <td colspan='2' style="background-color: white; color:black;">←上一版本</td> <td colspan='2' style="background-color: white; color:black;">2022年10月26日 (三) 15:39的版本</td> </tr><tr><td colspan="2" class="diff-lineno">第27行：</td> <td colspan="2" class="diff-lineno">第27行：</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>《王者之路 机器证明及其应用》吴文俊等</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>《王者之路 机器证明及其应用》吴文俊等</div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins style="color: red; font-weight: bold; text-decoration: none;"></ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins style="color: red; font-weight: bold; text-decoration: none;">吴氏方法的基本思想是，先把几何问题化为代数问题，再把代数问题化为代数恒等式的检验问题。代数恒等式的检验是机械的，问题的转化过程也是机械的，整个问题也就机械化了。《数学与哲学》张景中，p.156</ins></div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>==新闻==</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>==新闻==</div></td></tr> </table>

Allen http://wiki.huihoo.com/wiki/?title=Formal_verification&diff=166215&oldid=prev 2022-10-19T06:52:30Z

<p>‎<span dir="auto"><span class="autocomment">图集</span></span></p> <table class='diff diff-contentalign-left'> <col class='diff-marker' /> <col class='diff-content' /> <col class='diff-marker' /> <col class='diff-content' /> <tr valign='top'> <td colspan='2' style="background-color: white; color:black;">←上一版本</td> <td colspan='2' style="background-color: white; color:black;">2022年10月19日 (三) 06:52的版本</td> </tr><tr><td colspan="2" class="diff-lineno">第214行：</td> <td colspan="2" class="diff-lineno">第214行：</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>image:KeY-Symbolic-Execution-Debugger-SED.png|KeY SED</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>image:KeY-Symbolic-Execution-Debugger-SED.png|KeY SED</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>image:Formal-verification-VLSI-design.png|VLSI设计形式化验证</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>image:Formal-verification-VLSI-design.png|VLSI设计形式化验证</div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins style="color: red; font-weight: bold; text-decoration: none;">image:A-Multipurpose-Formal-RISC-V-Specification.png|RISC-V形式化验证</ins></div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>&lt;/gallery&gt;</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>&lt;/gallery&gt;</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"></td></tr> </table>

Allen http://wiki.huihoo.com/wiki/?title=Formal_verification&diff=166133&oldid=prev 2022-10-15T05:05:36Z

<p>‎<span dir="auto"><span class="autocomment">图集</span></span></p> <table class='diff diff-contentalign-left'> <col class='diff-marker' /> <col class='diff-content' /> <col class='diff-marker' /> <col class='diff-content' /> <tr valign='top'> <td colspan='2' style="background-color: white; color:black;">←上一版本</td> <td colspan='2' style="background-color: white; color:black;">2022年10月15日 (六) 05:05的版本</td> </tr><tr><td colspan="2" class="diff-lineno">第205行：</td> <td colspan="2" class="diff-lineno">第205行：</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>image:truth-table.png|真值表</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>image:truth-table.png|真值表</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>image:syntax-of-propositional-logic.png|命题逻辑的符号</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>image:syntax-of-propositional-logic.png|命题逻辑的符号</div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins style="color: red; font-weight: bold; text-decoration: none;">image:ITP-Common-Terms-and-Types.png|常见Terms和Types</ins></div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>image:HOL-family-tree.png|HOL家族</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>image:HOL-family-tree.png|HOL家族</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>image:HOL4-Emacs.png|HOL4 Emacs</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>image:HOL4-Emacs.png|HOL4 Emacs</div></td></tr> </table>

Allen http://wiki.huihoo.com/wiki/?title=Formal_verification&diff=166126&oldid=prev 2022-10-15T00:36:58Z

<p>‎<span dir="auto"><span class="autocomment">文档</span></span></p> <table class='diff diff-contentalign-left'> <col class='diff-marker' /> <col class='diff-content' /> <col class='diff-marker' /> <col class='diff-content' /> <tr valign='top'> <td colspan='2' style="background-color: white; color:black;">←上一版本</td> <td colspan='2' style="background-color: white; color:black;">2022年10月15日 (六) 00:36的版本</td> </tr><tr><td colspan="2" class="diff-lineno">第173行：</td> <td colspan="2" class="diff-lineno">第173行：</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://fm.csl.sri.com/SSFT14/rosette-lecture.pdf Programming for Everyone: From Solvers to Solver-Aided Languages and Beyond]</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://fm.csl.sri.com/SSFT14/rosette-lecture.pdf Programming for Everyone: From Solvers to Solver-Aided Languages and Beyond]</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://bblanche.gitlabpages.inria.fr/CryptoVerif/tutorial/cryptoverif.pdf CryptoVerif: Mechanizing Game-Based Proofs]</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://bblanche.gitlabpages.inria.fr/CryptoVerif/tutorial/cryptoverif.pdf CryptoVerif: Mechanizing Game-Based Proofs]</div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins style="color: red; font-weight: bold; text-decoration: none;">*[https://www.kth.se/social/files/596318bc56be5bfdc343d436/itp-course.pdf Interactive Theorem Proving (ITP) Course]</ins></div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>==图书==</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>==图书==</div></td></tr> </table>

Allen http://wiki.huihoo.com/wiki/?title=Formal_verification&diff=166120&oldid=prev 2022-10-14T13:20:13Z

<p>‎<span dir="auto"><span class="autocomment">文档</span></span></p> <table class='diff diff-contentalign-left'> <col class='diff-marker' /> <col class='diff-content' /> <col class='diff-marker' /> <col class='diff-content' /> <tr valign='top'> <td colspan='2' style="background-color: white; color:black;">←上一版本</td> <td colspan='2' style="background-color: white; color:black;">2022年10月14日 (五) 13:20的版本</td> </tr><tr><td colspan="2" class="diff-lineno">第172行：</td> <td colspan="2" class="diff-lineno">第172行：</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://fm.csl.sri.com/SSFT19/speaklogicV9.pdf Speaking Logic]</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://fm.csl.sri.com/SSFT19/speaklogicV9.pdf Speaking Logic]</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://fm.csl.sri.com/SSFT14/rosette-lecture.pdf Programming for Everyone: From Solvers to Solver-Aided Languages and Beyond]</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://fm.csl.sri.com/SSFT14/rosette-lecture.pdf Programming for Everyone: From Solvers to Solver-Aided Languages and Beyond]</div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins style="color: red; font-weight: bold; text-decoration: none;">*[https://bblanche.gitlabpages.inria.fr/CryptoVerif/tutorial/cryptoverif.pdf CryptoVerif: Mechanizing Game-Based Proofs]</ins></div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>==图书==</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>==图书==</div></td></tr> </table>

Allen http://wiki.huihoo.com/wiki/?title=Formal_verification&diff=166112&oldid=prev 2022-10-14T09:39:45Z

<p>‎<span dir="auto"><span class="autocomment">语言</span></span></p> <table class='diff diff-contentalign-left'> <col class='diff-marker' /> <col class='diff-content' /> <col class='diff-marker' /> <col class='diff-content' /> <tr valign='top'> <td colspan='2' style="background-color: white; color:black;">←上一版本</td> <td colspan='2' style="background-color: white; color:black;">2022年10月14日 (五) 09:39的版本</td> </tr><tr><td colspan="2" class="diff-lineno">第79行：</td> <td colspan="2" class="diff-lineno">第79行：</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>==语言==</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>==语言==</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>[[文件:purely-functional-programming.png]]</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>[[文件:purely-functional-programming.png]]</div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins style="color: red; font-weight: bold; text-decoration: none;">[[文件:FStarLang-logo.png|right|FStarLang]]</ins></div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*在数学、逻辑和计算机科学中，形式语言（[https://en.wikipedia.org/wiki/Formal_language Formal language]）是用精确的数学或机器可处理的公式定义的语言。</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*在数学、逻辑和计算机科学中，形式语言（[https://en.wikipedia.org/wiki/Formal_language Formal language]）是用精确的数学或机器可处理的公式定义的语言。</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[[F*]]</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[[F*]]</div></td></tr> </table>

Allen http://wiki.huihoo.com/wiki/?title=Formal_verification&diff=166091&oldid=prev 2022-10-13T02:47:04Z

<p>‎<span dir="auto"><span class="autocomment">理论</span></span></p> <table class='diff diff-contentalign-left'> <col class='diff-marker' /> <col class='diff-content' /> <col class='diff-marker' /> <col class='diff-content' /> <tr valign='top'> <td colspan='2' style="background-color: white; color:black;">←上一版本</td> <td colspan='2' style="background-color: white; color:black;">2022年10月13日 (四) 02:47的版本</td> </tr><tr><td colspan="2" class="diff-lineno">第53行：</td> <td colspan="2" class="diff-lineno">第53行：</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://en.wikipedia.org/wiki/Formal_system Formal system] 形式系统 [https://en.wikipedia.org/wiki/Formal_language Formal language] 形式语言 [https://en.wikipedia.org/wiki/Formal_grammar Formal grammar] 形式文法</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://en.wikipedia.org/wiki/Formal_system Formal system] 形式系统 [https://en.wikipedia.org/wiki/Formal_language Formal language] 形式语言 [https://en.wikipedia.org/wiki/Formal_grammar Formal grammar] 形式文法</div></td></tr> <tr><td class='diff-marker'>−</td><td style="background: #ffa; color:black; font-size: smaller;"><div>*[https://en.wikipedia.org/wiki/Satisfiability_modulo_theories satisfiability modulo theories (SMT)] 可满足性模理论 [https://smt-comp.github.io/ SMT-COMP] [https://leodemoura.github.io/files/mpi2009.pdf SMT @ Microsoft] [https://fm.csl.sri.com/SSFT22/piskac-lectures01.pdf SMT-based Verification of Heap-manipulating Programs]</div></td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div>*[https://en.wikipedia.org/wiki/Satisfiability_modulo_theories satisfiability modulo theories (SMT)] 可满足性模理论 [https://smt-comp.github.io/ SMT-COMP] [https://leodemoura.github.io/files/mpi2009.pdf SMT @ Microsoft] [https://fm.csl.sri.com/SSFT22/piskac-lectures01.pdf SMT-based Verification of Heap-manipulating Programs<ins class="diffchange diffchange-inline">] [https://fm.csl.sri.com/SSFT22/lecture2-new.pdf New update</ins>]</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://en.wikipedia.org/wiki/Automated_theorem_proving Automated theorem proving (ATP)] 自动化定理证明</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://en.wikipedia.org/wiki/Automated_theorem_proving Automated theorem proving (ATP)] 自动化定理证明</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://en.wikipedia.org/wiki/First-order_logic First-order logic] 一阶逻辑</div></td><td class='diff-marker'>&#160;</td><td style="background: #eee; color:black; font-size: smaller;"><div>*[https://en.wikipedia.org/wiki/First-order_logic First-order logic] 一阶逻辑</div></td></tr> </table>

Allen