A prolog technology theorem prover: Implementation by an extended prolog compiler

1. Andrews, P. B., ‘Theorem proving via general matings’, Journal of the ACM 28, 2 (April 1981) 193–214.

   Google Scholar 

2. Antoniou, G. and Ohlbach, H. J., ‘TERMINATOR’. Proceedings of the Eighth International Joint Conference on Artificial Intelligence, Karlsruhe, West Germany (August 1983) 916–919.

3. Bayerl, S., Kurfess, F., Letz, R., and Schumann, J., ‘PROTHEO/2: sequential PROLOG-like theorem prover based on the connection method’ (1986).

4. Bibel, W., Automated Theorem Proving. Friedr. Vieweg & Sohn, Braunschweig, West Germany (1982).

   Google Scholar 

5. Butler, R., Lusk, E., McCune, W., and Overbeek, R., ‘Paths to high-performance automated theorem proving’. Proceedings of the 8th Conference on Automated Deduction, Oxford, England (July 1986) 588–597.

6. Boyer, R. S. and Moore, J. S., ‘The sharing of structure in theorem-proving programs’. In B.Meltzer and D.Michie (eds.). Machine Intelligence 7. Edinburgh University Press, Edinburgh, Scotland (1972).

   Google Scholar 

7. Bürckert, H. J., Wang, H., and Zheng, R., ‘MKRP: a performance test by working mathematicians’. Memo SEKI-83-1, Institut für Informatik I, Universität Karlsruhe Karlsruhe, West Germany (1983).

   Google Scholar 

8. Chang, C. L. and Lee, R. C. T., Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, New York (1973).

   Google Scholar 

9. Cohen, J., ‘Describing Prolog by its interpretation and compilation’. Communications of the ACM 28, 12 (December 1985) 1311–1324.

   Google Scholar 

10. Colmerauer, A., ‘Prolog and infinite trees’. In Clark, K. L. and Tarnlund, S. A. (eds.). Logic Programming. Academic Press, New York, New York (1982).

    Google Scholar 

11. Eder, G. ‘A PROLOG-like interpreter for non-Horn clauses’. D.A.I. Research Report No. 26, Department of Artificial Intelligence, University of Edinburgh, Edinburgh, Scotland, September (1976).

    Google Scholar 

12. Fleisig, S., Loveland, D., SmileyIII, A. K., and Yarmush, D. L., ‘An implementation of the model climination proof procedure’: Journal of the ACM 21, 1 (January 1974) 124–139.

    Google Scholar 

13. Korf, R. E., Depth-first iterative-deepening: an optimal admissible tree search. Artificial Intelligence 27, 1 (September 1985) 97–109.

    Google Scholar 

14. Kowalski, R. and Kuehner, D., ‘Linear resolution with selection function’. Artificial Intelligence 2 (1971) 227–260.

    Google Scholar 

15. Lawrence, J. D. and Starkey, J. D., ‘Experimental tests of resolution based theorem-proving strategies’. Technical Report. Computer Science Department, Washington State University, Pullman, Washington (April 1974).

    Google Scholar 

16. Loveland, D. W., ‘A simplified format for the model elimination procedure’. Journal of the ACM 16, 3 (July 1969) 349–363.

    Google Scholar 

17. Loveland, D. W., Automated Theorem Proving: A Logical Basis. North-Holland, Amsterdam, the Netherlands (1978)

    Google Scholar 

18. Loveland, D. W., ‘Automated theorem proving: mapping logic into AI’ Proceedings of the International Symposium on Methodologies for Intelligent Systems, Knoxville, Tennessee (October 1986) 214–229.

19. Loveland, D. W., ‘Near-Horn Prolog’. Proceedings of the Fourth International Conference on Logic Programming, Melbourne, Australia (May 1987) 456–469.

20. Loveland, D. W. and Stickel, M. E., ‘The hole in goal trees: some guidance from resolution theory’. IEEE Transactions on Computers C-25, 4 (April 1976) 335–341.

    Google Scholar 

21. Lusk, E. L., McCune, W. W., and Overbeek, R. A., Logic Machine Architecture: kernel functions’. Proceedings of the 6th Conference on Automated Deduction, New York, New York (June 1982) 70–84.

22. Lusk, E. L., McCune, W. W., and Overbeek, R. A., ‘Logic Machine Architecture: inference mechanisms’. Proceedings of the 6th Conference on Automated Deduction, New York, New York (June 1982) 85–108.

23. Lusk, E. L. and Overbeek, R. A., ‘A portable environment for research in automated reasoning’. Proceedings of the 7th Conference on Automated Deduction, Napa, California (May 1984) 43–52.

24. Malachi, Y., Nonclausal Logic Programming. Ph.D. Dissertation, Department of Computer Science, Stanford University, March 1986.

25. Michie, D., Ross, R., and Shannan, G. J., ‘G-deduction’. In B.Meltzer and D.Michie (eds.). Machine Intelligence 7. John Wiley and Sons, New York, New York (1972) pp. 141–165.

    Google Scholar 

26. Nilsson, N. J., Principles of Artificial Intelligence. Tioga Publishing Co., Palo Alto, California (1980).

    Google Scholar 

27. Plaised, D. A., ‘A simplified problem reduction format’. Artificial Intelligence 18, 2 (March 1982) 227–261.

    Google Scholar 

28. Plaisted, D. A., ‘Non-Horn clause logic programming without contrapositives’ (1987).

29. Rao, V. N., Kumar, V., and Ramesh, K., ‘A parallel implementation of iterative-deepening A^*’. Proceedings of the AAAI-87 National Conference on Artificial Intelligence, Seattle, Washington (July 1987) 178–181.

30. Raph, Karl Mark G., ‘The Markgraf Karl Refutation Procedure’. Memo SEKI-MK-84-01, Fachbereich Informatik, Universität Kaiserslautern, Kaiserslautern, West Germany (January 1984).

    Google Scholar 

31. Reboh, R., Raphael, B., Yates, R. A., Kling, R. E., and Verlarde, C., ‘Study of automatic theoremproving programs’. Technical Note, 75, Artificial Intelligence Center, Stanford Research Institute, Menlo Park, California (November 1972).

    Google Scholar 

32. Shostak, R. E., ‘Refutation graphs’. Artificial Intelligence 7, 1 (Spring 1976) 51–64.

    Google Scholar 

33. Slate, D. J., and Atkin, L. R., ‘CHESS 4.5 — The Northwestern University chess program’. In Frey, P. W. (ed.), Chess Skill in Man and Machine, Springer-Verlag, New York, New York (1977) 82–118.

    Google Scholar 

34. Stickel, M. E., ‘A Prolog technology theorem prover’. New Generation Computing 2, 4 (1984) 371–383.

    Google Scholar 

35. Stickel, M. E. and Tyson, W. M., ‘An analysis of consecutively bounded depth-first search with applications in automated deduction’. Proceedings of the Ninth International Joint Conference on Artificial Intelligence, Los Angeles, California (August 1985) 1073–1075.

36. Umrigar, Z. D. and Pitchumani, V., ‘An experiment in programming with full first-order logic’. Proceedings of the 1985 Symposium on Logic Programming, Boston, Massachusetts (July 1985) 40–47.

37. Warren, D. H. D., ‘An abstract Prolog instruction set’. Technical Note 309, Artificial Intelligence Center, SRI International Menlo Park, California (October 1983).

    Google Scholar 

38. Wilkins, D. E., ‘QUEST: a non-clausal theorem proving system’. M.Sc. Thesis, University of Essex, Essex, England, 1973.

39. Wilson, G. A. and Minker, J., ‘Resolution, refinements, and search strategies: a comparative study’. IEEE Transactions on Computers C-25, 8 (August 1976) 782–801.

    Google Scholar 

40. Wos, L., Veroff, R., Smith, B., and McCune, W., ‘The linked inference principle, II: the user's viewpoint’. Proceedings of the 7th International Conference on Automated Deduction, Napa, California (May 1984) 316–332.

41. Wos, L. T., Unpublished notes, Argonne National Laboratory (about 1965).

Download references