「SF-PLF」18 UseAuto

Programming Language Foundations - Theory And Practice Of Automation In Coq Proofs

Posted by Hux on March 18, 2019

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