「SF-PLF」18 UseAuto

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