VVbuys Blog

standalone Linux lover

  • Home
  • Tags
  • Archives
  • Sitemap
  • Commonweal 404
  • Table of Contents
  • Overview
  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

vvbuys

Share some post and some issue for linux program
265 posts
36 categories
36 tags

「SF-PLF」18 UseAuto

Posted on 2024-02-02

Basic Features of Proof Search

Strength of Proof Search

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


Advanced Topics in Proof Search


Decision Procedures

Omega

Ring

Congurence

# 笔记 # SF (软件基础) # Coq # PLF (编程语言基础)
Data Representation - Integer
「SF-PLF」17 UseTactics
© 2024 vvbuys
Powered by Hexo & NexT.Muse
0%