D.W. LOVELAND [WR1] Wos, L., G. Robinson, D. Carson and L. Shalla. The concept of demodulation in theorem provfng. Jour. Assoc. for Com.put. Jla.ch., 1967, 698-709. [WR2] Wos, L. and G. Robinson. Paramodulation and set of sup- port. Symp. on Automatic Demonstration, Lecture Notes in Math. 125, Springer-Verlag, Berlin, 1970, 276-310. [WW1] Winker, S.K. and L. Wos. Procedure implementation through demodulation and related tricks. Proc. Si.zth Conf. on Auto. Deduction (Loveland, Ed.), Lecture Notes in Comp. Science 138, Springer-Verlag, Berlin, June 1982, 109-131. [WW2] Winker, S., L. Wos and E. Lusk. Semigroups, antiautomor- phisms, and involutions: a computer solution to an open problem. I. Math. of Computation, 1981, 533-545. [WW3] Wos, L., S. Winker and E. Lusk. An automated reasoning sys- tem. AF/PS Conf. Proc.: Natl. Camp. Conf., AFIPS Press, Montvale, 1981, 697-702. [Wu1] Wu, Wen-tsiin. On the decisio.n problem and the mechaniza- tion of theorem-proving in elementary geometry. Scienticl S'inica XXI (2), Mar. -Apr. 1978, 159-172. [YR1] Yates, R.A., B. Raphael and T.P. Hart. Resolution graphs. Artif. /ntell., 1970, 257-289.
Previous Page Next Page