%theorem

From The Twelf Project

The %theorem declaration acts as the specification of a theorem.

[edit] Use to write statements of metatheorems

Some people find the notation a clearer way of specifying metatheorems; a %theorem declaration used in this style handles the type family declation and the %mode declaration parts of a totality assertion.

[edit] Use with the theorem prover

When using the Twelf theorem prover, a %theorem declaration establishes a proposition that the theorem prover may later attempt to establish. A %theorem declaration is thus somewhat analogous to the three-part specification of a totality assertions, the type family definition, the %mode declaration, and the %worlds declaration.

[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