An integral theorem prover and the role of proof planning (Q1189730)

The paper reflects an effort of the authors to use rule-based systems for computing integrals. The system prover for integration theorem proving is presented. Various types of integrals are admitted such as Riemann, Stieltjes, Lebesgue, Cauchy, but the results achieved are concerning Riemann integrals only. To make the transformation of integration into theorem proving sphere easy a predicate form of integrals is used. Thereby a rule base is available for proving integration theorems. The system prover is implemented in Prolog and represents a proof planning method which substantially reduces the number of steps in the search space. The rule base containing fundamental definitions, functions and theorems as well as the proof method with plan are presented in three appendices. Several instructive examples illustrate the work of the system.