Solid Intuition/Unification

From SE Wiki
Revision as of 15:37, 22 December 2010 by 128.100.4.130 (Talk)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Instantiation of Laws

In order to make proving a pure point-and-click activity, instantiation of laws has to be done automatically. Fortunately, given a focus expression and one side of a law, it is a purely automatic process to match those two expressions and instantiate the ∀-quantified variables in the law. This is what unification does! In instantiating quantified variables the law of generalisation is implicitly applied. In formal on-paper proofs this application of the law is never mentioned and taking for granted (especially since the laws are often not even written in quantified form).

Instantiation of Variables in the Focus

To use the Specialisation and The laws Unification is also used when we want to apply