[Sil] Sickel, S. Interconnectivity graphs. IEEE 7Tans. on Comput-
[SJ1] Suzuki, N. and D. Jefferson. Verification decidability of
Presburger array programs . . P,.oc. Conf. on 1heor. Comput.
Science, Univ. of Waterloo, Aug. 1977.
[Sll] Slagle, J.R. Automatic theorem proving with built-in
theories of equality, partial order and sets. Jour. Assoc. for
Comput. Mach., 1972, 120-135.
[Sl2] Slagle, J.R. Automated theorem proving for theories with
simplifiers, commutativity and associativity. Jour. Assoc. for
Comput. Mach., 1974, 622-642.
[Stl] Stickel, M.E. A complete unification algorithm for
associative-commutative functions. Proc. Fourth ln.tern.
Joint Conf. on ArtiJ. ln.tell., Tbilisi, USSR, 1975. Also see
Jour. Assoc. for Comput. Mach., 1981, 423:..434.
[SW1] Siekmann, J. and G. Wrightson (Eds.).
Automation of
Reasoning. Vols. I and II, Springer-Verlag, 1983.
[Tu1] Turing, A.M. Computing machinery and intelligence. Mind,
1950, 433-460.
[Wa1) Wang, H. Toward mechanical mathematics. IBM Jour.
Research and .Devel., 1960, 2-22. Also in Logic, Computers
and Sets, Chelsea, New York, 1970.
[Wa2) Wang, H. Proving theorems by pattern recognition, Part I.
Commun. Assoc. for Comput. Mach., 1960, 220-234.
[Wa3] Wang, H. Proving theorems by pattern recognition, Part II.
Bell System Technical Jour., 1961, 1-41.
[WC1] Wos, L., D. Carson and G. Robinson. The unit preference
strategy in theorem proving. AFIPS
Proc. 26, Spartan
Books, Wash., D.C., 1964, 615-621.
[Wo1] Wos, L. Solving open questions with an automated
theorem-proving program. Proc. Sizth Conf. on Auto. Deduc-
tion (Loveland, Ed.), Lecture Notes in Comp. Science 138,
Springer-Verlag, Berlin, June 1982, 1-31.
Previous Page Next Page