Algorithm-Supported Mathematical Theory Exploration: A Personal View and Strategy - Artificial Intelligence and Symbolic Computation - page 247

This rule is amazingly powerful as demonstrated by the above nontrivial
algorithm synthesis. The invention of failing proof analysis and requirements
generation techniques is an important future research topic.

7 Meta-programming

Meta-programming is a subtle and not widely available language feature. How-
ever, we think that it will be of utmost practical importance for the future
acceptance of algorithm-supported mathematical theory exploration systems. In
meta-programming, one wants to use the logic language both as an object and a
meta-language. In fact, in one exploration session, the language level may change
several times and we need to provide means for governing this change in future
systems. For example, in an exploration session, we may first want to define (by
applying the divide-and-conquer scheme) a sorting algorithm

sort [ x ]= x .

⇐ is-short-tuple [ x ]

∀ x

merge [ x, sort [ left [ x ]] ,sort [ right [ x ]]] ⇐ otherwise

Then we may want to apply one of the provers in the system to prove the
algorithm correct, i.e. we want to prove

is-sorted [ sort [ x ]]
contain-the-same-elements [ x, sort [ x ]]

∀ x

by calling, say, a prover tuple-induction
∀ x tuple-induction is-sorted [ sort [ x ]]

,

,K 0

contain-the-same-elements [ x, sort [ x ]]

and checking whether the result is the constant 'proved', where K 0 is the knowl-
edge base containing the definition of sort and is-sorted and definitions and
propositions on the auxiliary operations.
Now, tuple-induction itself is an algorithm which the user may want to define
himself or, at least, he might want to inspect and modify the algorithm available
in the prover library. This algorithm will have the following structure

tuple-induction [ ∀ x F, K ]=

and [ tuple-induction [ F x← ,K ] ,
tuple-induction [ F x←x 0 ,y 0 , append [ K, F x←y 0 ]] ,

is substitution and x 0 and y 0 are “arbitrary but fixed” constants (that
must be generated from x , F ,and K ).
Also, tuple-induction itself needs a proof that could proceed, roughly, by
calling a general predicate logic prover in the following way

←

where

general-prover

∀ x F , ∀ x,F,K tuple-induction ∀ x F, K =“ proved ” ⇒ append [ ind, K ]

| =

where ind are the induction axioms for tuples and denotes logic consequence.