Proof Analogy in Interactive Theorem Proving: A Method to Express and Use It via Second Order Pattern Matching.

Thierry Boy de la Tour, Ricardo Caferra

Browse the full AAAI paper archive.