Inducing theorem provers from proofs
Raul Lopes, Mark Tarver · 2002
A methodology is introduced for the automatic generation of theorem provers from sets of proof examples. As an example, this methodology was used to generate a theorem prover for intuitionistic propositional calculus which proves any theorem for this logic found D. van Dalen's book "Logic and structure" (Springer-Verlag, 1994), using a depth-first search strategy without loop detection.