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