reference:rule_calculus

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, 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 178.26.109.100