On connections and higher-order logic

1. Andrews, Peter B., ‘Resolution in Type Theory’, Journal of Symbolic Logic 36, 414–432 (1971).

   Google Scholar 

2. Andrews, Peter B., ‘Resolution and the Consistency of Analysis’, Notre Dame Journal of Formal Logic 15, 73–84 (1974).

   Google Scholar 

3. Andrews, Peter B., ‘Refutations by Matings’, IEEE Transactions on Computers C-25, 801–807 (1976).

   Google Scholar 

4. Andrews, Peter B., ‘Transforming Matings into Natural Deduction Proofs,’ in 5th Conference on Automated Deduction. edited by W. Bibel and R. Kowalski, Les Arcs, France, Lecture Notes in Computer Science 87, Springer-Verlag, 1980, pp. 281–292.

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

   Google Scholar 

6. Andrews, Peter B., Miller, Dale A., Cohen, Eve Longini, and Pfenning, Frank, ‘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, pp. 169–192.

7. Andrews, Peter B., An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Academic Press, 1986.

8. Andrews, Peter B., ‘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, pp. 1–4.

9. Bibel Wolfgang, and Schreiber J., §lsProof search in a Gentzen-like system of first-order logic’, in International Computing Symposium 1975, edited by E. Gelenbe and D. Potier Eds, North-Holland, Amsterdam, 1975, pp. 205–212.

   Google Scholar 

10. Bibel, Wolfgang, ‘Tautology Testing with a Generalized Matrix Reduction Method’, Theoretical Computer Science 8, 31–44 (1979).

    Google Scholar 

11. Bibel, Wolfgang, ‘On Matrices with Connections’, Journal of the ACM, 28, 633–645 (1981).

    Google Scholar 

12. Bibel, Wolfgang, Automated Theorem Proving, Vieweg, Braunschweig, 1982.

    Google Scholar 

13. Bibel, Wolfgang, ‘A Comparative Study of Several Proof Procedures’, Artificial Intelligence, 18, 269–293 (1982).

    Google Scholar 

14. Bibel, Wolfgang, ‘Matings in Matrices’, Communications of the ACM, 26, 844–852 (1983).

    Google Scholar 

15. Bibel, Wolfgang, and Buchberger, Bruno, ‘Towards a Connection Machine for Logical Inference’, Future Generations Computer Systems 1, 177–185 (1984–1985).

    Google Scholar 

16. Bledsoe, W. W., ‘A Maximal Method for Set Variables in Automatic Theorem Proving’, in Machine Intelligence 9, Ellis Harwood Ltd., Chichester, and John Wiley & Sons, 1979, pp. 53–100.

    Google Scholar 

17. Bledsoe, W. W., ‘Using Examples to Generate Instantiations of Set Variables’, in Proceedings of IJCAI-83, Karlsruhe, Germany, Aug 8–12, 1983, pp. 892–901.

18. Church, Alonzo, ‘A formulation of the Simple Theory of Types’, Journal of Symbolic Logic 5, 56–68 (1940).

    Google Scholar 

19. Davis, Martin, ‘Eliminating the Irrelevant from Mechanical Proofs’, in Experimental Arithmetic, High Speed Computing and Mathematics, Proceedings of Symposia in Applied Mathematics XV, American Mathematical Society, 1963, pp. 15–30.

20. Dreben, Burton, Andrews, Peter, and Aanderaa, Stal, ‘False Lemmas in Herbrand’, Bulletin of the American Mathematical Society, 69, 699–706 (1963).

    Google Scholar 

21. Dreben, Burton and Denton, John, ‘A Supplement to Herbrand’, Journal of Symbolic Logic 31, 393–398 (1966).

    Google Scholar 

22. Huet, Gérard P., ‘A Mechanization of Type Theory’, in Proceedings of the Third International Joint Conference on Artificial Intelligence, IJCAI, 1973, pp. 139–146.

23. Huet, Gérard P., ‘A Unification Algorithm for Typed λ-Calculus’, Theoretical Computer Science 1, 27–57 (1975).

    Google Scholar 

24. Jensen, D. C., and Pietrzykowski, T., ‘Mechanizing ω-Order Type Theory Through Unification’, Theoretical Computer Science 3, 123–171 (1976).

    Google Scholar 

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

26. Miller, Dale A., ‘Expansion Tree Proofs and Their Conversion to Natural Deduction 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, pp. 375–393.

27. Miller, Dale A., ‘A Compact Representation of Proofs’, Studia Logica 46, 347–370 (1987).

    Google Scholar 

28. Pfenning, Frank, ‘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, pp. 394–413.

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

30. Prawitz, Dag, ‘Advances and Problems in Mechanical Proof Procedures’, in Machine Intelligence 4, Edinburgh University Press, 1969, pp. 59–71.

31. Prawitz, Dag, ‘A proof procedure with matrix reduction’, in Symposium on Automatic Demonstration, Versailles, France, edited by M. Laudet, D. Lacombe, L. Nolin, and M. Schutzenberger, Lecture Notes in Mathematics 125, Springer-Verlag, 1970, pp. 207–214.

32. Shostak, Robert E., ‘Refutation Graphs’, Artificial Intelligence 7, 51–64 (1976).

    Google Scholar 

Download references