Employing External Reasoners in Proof Planning
Erica Melis⋆, Volker Sorge · Electronic Notes in Theoretical Computer Science · 1999
This paper describes the integration of computer algebra systems and constraint solvers into proof planners. It shows how efficient external reasoners can be employed in proof planning and how the shortcuts of the external reasoners can be expanded to verifiable natural deduction proofs in the proof planning framework. In particular, these shortcuts simplify and guide the formal proof. The paper illustrates the integration and cooperation of the external reasoners with an example from proof planning limit theorems.