%prove

From The Twelf Project

The %prove directive attempts to prove a theorem specified by a %theorem directive using the theorem prover. It is therefore similar to the %establish directive. However, unlike the %establish directive, theorems shown to be true by the %prove directive are considered as potential lemmas when the theorem prover attempts to prove future theorems.

[edit] 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