「软件基础 – 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