%establish

The %establish directive attempts to prove a theorem specified by a %theorem directive using the theorem prover. It is therefore similar to the %prove directive. However, unlike the %prove directive, theorems shown to be true by the %establish directive are not used to prove other theorems.

See also

• Theorem prover
• Theorem Prover in the User's Guide

Twelf keywords

---

%. %abbrev %assert %block %clause %covers %define %deterministic %establish %freeze %infix %prefix %postfix %mode %name %prove %query %querytabled %reduces %solve %subord %tabled %terminates %thaw %theorem %total %trustme %unique %use %worlds