AUTOMATED THEOREM PROVING 41

[Sil] Sickel, S. Interconnectivity graphs. IEEE 7Tans. on Comput-

ers

C-25,

1976.

[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.).

1he

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

Con/.

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.