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