The TPS theorem proving system

1. Peter B. Andrews, Theorem Proving via General Matings, Journal of the ACM 28 (1981), 193–214.

   Article  Google Scholar 

2. Peter B. Andrews, Dale A. Miller, Eve Longini Cohen, Frank Pfenning, "Automating Higher-Order Logic," in Automated Theorem Proving: After 25 Years, edited by W. W. Bledsoe and D. W. Loveland, Contemporary Mathematics series, vol. 29, American Mathematical Society, 1984, 169–192.

   Google Scholar 

3. Peter B. Andrews, "Connections and Higher-Order Logic," in 8th International Conference on Automated Deduction, edited by Jorg H. Siekmann, Oxford, England, Lecture Notes in Computer Science 230, Springer-Verlag, 1986, 1–4.

   Google Scholar 

4. Gerard P. Huet, A Unification Algorithm for Typed λ-Calculus, Theoretical Computer Science 1 (1975), 27–57.

   Article  Google Scholar 

5. Dale A. Miller. Proofs in Higher-Order Logic, Ph.D. Thesis, Carnegie Mellon University, 1983. 81 pp.

   Google Scholar 

6. Dale A. Miller, A Compact Representation of Proofs, Studia Logica 46 (1987), 345–368.

   Article  Google Scholar 

7. Frank Pfenning, "Analytic and Non-analytic Proofs," in 7th International Conference on Automated Deduction, edited by R. E. Shostak, Napa, California, USA, Lecture Notes in Computer Science 170, Springer-Verlag, 1984, 394–413.

   Google Scholar 

8. Frank Pfenning. Proof Transformations in Higher-Order Logic, Ph.D. Thesis, Carnegie Mellon University, 1987. 156 pp.

   Google Scholar 

Download references