Polymorphic lemmas and definitions in Lambda Prolog and Twelf

Andrew W. Appel, Amy P. Felty

Lambda Prolog is known to be well-suited for expressing and implementing logics and inference systems. We show that lemmas and definitions in such logics can be implemented with a…