Title :
Inducing theorem provers from proofs
Author :
Lopes, Raul H C ; Tarver, Mark
Author_Institution :
Sch. of Comput. Studies, Leeds Univ., UK
Abstract :
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
Keywords :
formal logic; generalisation (artificial intelligence); inference mechanisms; learning by example; theorem proving; tree searching; automatic theorem prover generation; depth-first search strategy; inductive generalization; intuitionistic propositional calculus; loop detection; machine learning; proof examples; theorem prover induction; Application software; Automatic logic units; Calculus; Character generation; Displays; Expert systems; Formal languages; Inference algorithms; Problem-solving;
Conference_Titel :
Tools with Artificial Intelligence, 1997. Proceedings., Ninth IEEE International Conference on
Conference_Location :
Newport Beach, CA
Print_ISBN :
0-8186-8203-5
DOI :
10.1109/TAI.1997.632250
