The 'LCF design' inherited by the HOL theorem prover [1] allows users to write ML functions encoding arbitrary patterns of logical deduction. Such ML functions are called derived rules, because the only way that they can create theorems is by composing a sequence of existing rules. The initial rules, implemented in a small logical kernel, are the primitive inference rules of higher-order logic. This design philosophy is called fully-expansive proof, because every derived rule can be 'fully expanded' to a (long) sequence of primitive inferences.
展开▼
