Theory links in semantic graphs

1. Andrews, P.B. Theorem proving via general matings. JACM 28,2 (April 1981), 193–214.

   Article  Google Scholar 

2. Bibel, W. On matrices with connections. JACM 28,4 (Oct. 1981), 633–645.

   Article  Google Scholar 

3. Brachman, R.J., Gilbert, V. Pigman, and Levesque, H.J. An essential hybrid reasoning system: Knowledge and symbol level accounts of KRYPTON. Proceedings of The 9^th International Joint Conference on Artificial Intelligence, Los Angeles, CA, August 18–24, 1985, 532–539.

   Google Scholar 

4. Cohn, A.G. On the solution of Schubert's Steamroller in many sorted logic. Proceedings of the 9^th International Joint Conference on Artificial Intelligence, Los Angeles, CA, August 1985, 1169–1174.

   Google Scholar 

5. Haas, N. and Hendrix, G.G. An approach to acquiring and applying knowledge. Proceedings of the AAAI-80 National Conference on Artificial Intelligence, Stanford, CA, August 1980, 235–239.

   Google Scholar 

6. Kowalski, R. A proof procedure using connection graphs. J.ACM 22,4 (Oct. 1975), 572–595.

   Article  Google Scholar 

7. Manna, Z. and Waldinger, R. Special relations in automated deduction. J.ACM 33,1 (Jan. 1986), 1–59.

   Article  Google Scholar 

8. Murray, N.V., and Rosenthal, E. Path resolution and semantic graphs. Proceedings of EUROCAL '85, Linz Austria, April 1–3, 1985. In Lecture Notes in Computer Science, Springer-Verlag, vol. 204, 50–63.

   Google Scholar 

9. Murray, N.V., and Rosenthal, E. Inference with path resolution and semantic graphs. Submitted, June 1985.

   Google Scholar 

10. Murray, N.V., and Rosenthal, E. On deleting links in semantic graphs. To appear in the proceedings of The Third International Conference on Applied Algebra, Algebraic algorithms, Symbolic Computation and Error Correcting Codes, Grenoble, France, July 15–19, 1985.

    Google Scholar 

11. Murray, N.V., and Rosenthal, E. Improved link deletion and inference: proper path resolution. Submitted, August 1985.

    Google Scholar 

12. Murray, N.V., and Rosenthal, E. Theory links: applications to automated theorem proving. Submitted, March 1986.

    Google Scholar 

13. Nilsson, N.J. A production system for automatic deduction. Technical Note 148, SRI International, 1977.

    Google Scholar 

14. Pigman, V. The interaction between assertional and terminological knowledge in KRYPTON. Proceedings of the IEEE Workshop on Principles of Knowledge-Based Systems, Denver, Colorado, December 1984.

    Google Scholar 

15. Prawitz, D. An improved proof procedure. Theoria 26 (1960), 102–139.

    Google Scholar 

16. Robinson, J.A. A machine oriented logic based on the resolution principle. J.ACM 12,1 (1965), 23–41.

    Article  Google Scholar 

17. Robinson, J.A. An overview of mechanical theorem proving. Theoretical Approaches to Non-Numerical Problem Solving, Springer-Verlag, New York, Inc., 1970, 2–20.

    Google Scholar 

18. Shostak, R.E. DEciding combinations of theories. Proc. Sixth Conf. on Automated Deduction, New York, New York, June 1982, 209–222.

    Google Scholar 

19. Stickel, M.E. Theory resolution: building in nonequational theories. Proc. of the Nat. Conf. on A.I., Washington, D.C., Aug. 1983.

    Google Scholar 

20. Stickel, M.E. Automated deduction by theory resolution. Technical Note 340, SRI International, Oct. 1984.

    Google Scholar 

21. Stickel, M.E. Automated deduction by theory resolution. Proc. of the 9^th International Joint Conf. on Artificial Intelligence, Los Angeles, CA, August 18–24, 1985, 1181–1186.

    Google Scholar 

22. Walther, C. A mechanical solution of Schubert's Steamroller by many-sorted resolution. Proceedings of the AAAI-84 National Conference on Artificial Intelligence, Austin, Texas, August 1984, 330–334.

    Google Scholar 

Download references