Inducing theorem provers from proofs

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