User Tools

Site Tools


Rule (calculus)

In Logics

In a logical calculus, a rule is given by

with formula in the considered logic. Of course, might depend on any combination of the .

The meaning is this: If you can prove in your calculus, you can also prove . In other terms, a set of rules together with some axioms (rules with ) gives an inductive definition of the set of theorems in your theory.

A rule is correct if and only if is valid if all are valid. That means you can never get an inconsistent theory if you have only correct rules and valid axioms.

In Isabelle/HOL

In Isabelle/HOL, rules are theorems in PURE logics. They are denoted as

which is equivalent to above definition.

The nice things about Isabelle/HOL is that you can use your own theorems as rules if they have this format. You can tell Isabelle to transform a theorem into this form (if possible) by using the rule_format directive.

reference/rule_calculus.txt · Last modified: 2011/06/13 22:05 by