Building in axioms and lemmas
Larry M. Hines · 1988
Many programs have built-in axioms and lemmas of various theories. These programs gain their efficiency by restricting and guiding the use of their axioms and lemmas; however, they do not hold their axioms or lemmas in a declarative form. Control and representation issues were intertwined with the encoding of the axioms and lemmas. As a result, the programs cannot be simply combined to form more powerful programs. This paper describes a method of building in such axioms and lemma in a declarative form while still gaining their efficiency. This is attained by utilizing a set of declaratively defined axiom-rules and rule-sequences which not only implement the axioms and lemmas but also hold strategic information concerning how and when to use them. The prover can be easily altered by adding, deleting or modifying rules; moreover, the built-in axiom-rules can also be used as components for building in further axioms and lemmas, resulting in a hierarchy of theorem proving tools. One such tool is hyper-chaining. It is a rule-sequence built upon chaining (transitivity of inequality axiom) which is an axiom-rule that was, in turn, built upon an axiom-rule for the trichotomy of inequality. Using hyper-chaining, the prover has automatically proved a number of theorems including theorems on limits and the intermediate value theorem. This paper describes hyper-chaining, how it was built-in and how it was used to prove the intermediate value theorem.