「软件基础 - PLF」 18. Theory And Practice Of Automation In Coq Proofs

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

---

• Previous
  「软件基础 - PLF」 17. Tactic Library For Coq: A Gentle Introduction
• Next
  「软件基础 - PLF」 19. Partial Evaluation

---