「SF-PLF」18 UseAuto
Pin Young Lv9
  2021-03-28 00:00:00 2021-03-28 00:00   2023-02-02 13:37:48   36 字  1 分钟  

four proof-search tactics: auto, eauto, iauto and jauto.

How Proof Search Works

Search Depth

Backtracking

Adding Hints

Integration of Automation in Tactics

Example Proofs

Decision Procedures

Omega

Ring

Congurence

  • 本文标题：「SF-PLF」18 UseAuto
  • 本文作者：Pin Young
  • 创建时间：2021-03-28 00:00:00
  • 本文链接：posts/de7c.html
  • 版权声明：本博客所有文章除特别声明外，均采用 BY-NC-SA 许可协议。转载请注明出处！
  1. 1. Basic Features of Proof Search
    1. 1.1. Strength of Proof Search
  2. 2. How Proof Search Works
    1. 2.1. Search Depth
    2. 2.2. Backtracking
    3. 2.3. Adding Hints
    4. 2.4. Integration of Automation in Tactics
  3. 3. Example Proofs
  4. 4. Advanced Topics in Proof Search
    1. 4.1.
  5. 5. Decision Procedures
    1. 5.1. Omega
    2. 5.2. Ring
    3. 5.3. Congurence