ORA Canada Bibliography of Automated Deduction: Authors S to T

*[Sacca 1989] D. Sacca, C. Zaniolo, Rule transformation methods in the implementation of logic based languages, In: Resolution of Equations in Algebraic Structures: Vol 1, Algebraic Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 411-444.

[Sacerdoti 1974] E. Sacerdoti, Planning in a hierarchy of abstraction spaces, Artificial Intelligence 5(1974):115-135.

[Sacks 1987a] E. Sacks, Hierarchical inequality reasoning, TM 312, Massachussetts Institute of Technology, Laboratory for Computer Science, 545 Technology Square, Cambridge, MA 02139, 1987.

*[Sacks 1987b] E. Sacks, Hierarchical reasoning about inequalities, Proc. 6th Natl Conf. on Artificial Intelligence (AAAI 87), Seattle, Washington, 13-17 July 1987, Vol. 2, pp. 649-654.

*[Sacks 1987c] E. Sacks, Piecewise linear reasoning, Proc. 6th Natl Conf. on Artificial Intelligence (AAAI 87), Seattle, Washington, 13-17 July 1987, Vol. 2, pp. 655-659.

*[Sacks 1989] E. Sacks, An approximate solver for symbolic equations, Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 431-434.

[Sakai 1984] K. Sakai, An ordering method for term rewriting systems, Proc. 1st Intl. Conf. on Future Generations Computer Systems, Tokyo, Japan, November 1984.

*[Saletore 1990] V.A. Saletore, L.V. Kale, Consistent linear speedups to a first solution in parallel state-space search, Proc. 8th National Conf. on Artificial Intelligence (AAAI-90, July 29-August 3, 1990), AAAI Press/MIT Press, 1990, pp. 227-233.

[Samet 1980] H. Samet, Efficient on-line proofs of equalities and inequalities of formulas, IEEE Trans. on Computers C-29(1):28-30, January 1980.

[Sandewall 1969] E.J. Sandewall, A property-list representation for certain formulas in predicate calculus, Report No. 18, Uppsala Univ., Computer Sciences Dept., Uppsala, Sweden, January 1969.

[Sandford 1977a] D.M. Sandford, The BSUT-minimal refinement: A forbidden substitution refinement, DCS-TM-10, Dept. of Computer Sci., Rutgers Univ., June 1977.

[Sandford 1977b] D.M. Sandford, Formal specifications of models for semantic theorem proving strategies, ARPA SOSAP-TR-32, Dept. of Computer Sci., Rutgers Univ., 1977.

[Sandford 1977c] D.M. Sandford, Hereditary-lock resolution: A resolution refinement combining a strong model strategy with lock resolution, ARPA SOSAP-TR-30, Dept. of Computer Sci., Rutgers Univ., February 1977.

[Sandford 1980a] D.M. Sandford, Using sophisticated models in resolution theorem proving, LNCS 90, ed. G. Goos and J. Hartmanis, Springer-Verlag, NY, 1980.

[Sandford 1980b] D.M. Sandford, A mechanism for resolution refinements based on back substitutions, DCS-TR-77, Dept. of Computer Sci., Rutgers Univ., December 1980.

[Sannella 1983] D.T. Sannella, R.M. Burstall, Structured theories in LCF, Internal Report, CSR-129-83, Univ. of Edinburgh, Dept. of Computer Sci., Edinburgh, February 1983.

*[Sarkar 1989] D. Sarkar, S.C. De Sarkar, Some inference rules for integer arithmetic for verification of flowchart programs on integers, Software Engineering 15(1):1-9, January 1989. *[Sasaki 1986] T. Sasaki, Simplification of algebraic expression by multiterm rewriting rules, Proc. 1986 ACM-SIGSAM Symp. on Symbolic and Algebraic Computation (SYMSAC '86, Univ. of Waterloo, Waterloo, Ontario, 21-23 July 1986), ed. B.W. Char, ACM, New York, NY, 1986, pp. 115-119.

*[Satz 1990] R.W. Satz, EXPERT THINKER: An adaptation of F-Prolog to microcomputers (abstract), Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 671-672.

[Saya 1977] H. Saya, R. Caferra, A structure sharing technique for matrices and substitutions in Prawitz' theorem proving program, Rapport No. 101, Univ. of Grenoble, 1977.

[Scales 1986] D.J. Scales, Efficient matching algorithms for the SOAR/OPS5 production system, STAN-CS-86-1124, Stanford Univ. Computer Science, June 1986.

*[Schagrin 1985] M.L. Schagrin, W.J. Rapaport, R.R. Dipert, Logic: A Computer Approach, McGraw-Hill Book Company, New York, 1985.

*[Scheidhauer 1988] R. Scheidhauer, G. Seul, A test environment for unification algorithms, SEKI Working Paper SWP-88-03, Universitat Kaiserslautern, 1988.

*[Schemmel 1987] K.-P. Schemmel, An extension of Buchberger's algorithm to compute all reduced Grobner bases of a polynomial ideal, Proc. European Conf. on Computer Algebra (EUROCAL '87, Leipzig, GDR, 2-5 June 1987), ed. J.H. Davenport, LNCS 378, Springer-Verlag, Berlin, 1989, pp. 300-310.

*[Schmerl 1987] R. U. Schmerl, Resolution on formula trees, Proc. 11th German Workshop on Artificial Intelligence (GWAI-87, Geseke, September 28-October 2, 1987), ed. K. Morik, Springer-Verlag, Berlin, 1987, pp. 211-220; also Acta Informatica 25(4):425-438, 1988.

*[Schmid 1989] R. Schmid, H.-A. Schneider, T. Filkorn, Using an extended Prolog to solve the lion and unicorn puzzle, J. Automated Reasoning 5(3):403-408, September 1989.

[Schmidt 1983a] D. Schmidt, A programming notation for tactical reasoning, Internal Report, CSR-141-83, Univ. of Edinburgh, Dept. of Computer Sci., Edinburgh, September 1983; also Proc. 7th Conf. on Automated Deduction, ed. R.E. Shostak, Springer-Verlag, LNCS 170, 1984, pp. 445-459.

*[Schmidt 1983b] D. Schmidt, Natural deduction theorem proving in set theory, Internal Report, CSR-142-83, Univ. of Edinburgh, Dept. of Computer Sci., Edinburgh, September 1983.

[Schmidt 1984] D.A. Schmidt, A programming notation for tactical reasoning, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 445-459.

[Schmidt-Schauss 1985a] M. Schmidt-Schauss, Mechanical generation of sorts in clause sets, Interner Bericht MK-85-6, Fachber, Informatik, Universitat Kaiserslautern, 1985.

[Schmidt-Schauss 1985b] M.A. Schmidt-Schauss, A many-sorted calculus with polymorphic functions based on resolution and paramodulation, Internal Report Memo SEKI-85-II-KL, Fachbereich Informatik, Universitat Kaiserslautern, 1985; also Proc. 9th IJCAI, Los Angeles, CA, August 1985, pp. 1162-1168.

[Schmidt-Schauss 1985c] M.A. Schmidt-Schauss, Unification in a many-sorted calculus with declarations, Proc. GWAI-85, 9th German Workshop on Artificial Intelligence (Dassel/Solling, FRG, 23-27 September 1985), Informatik-Fachberichte 118, ed. H. Stoyan, Springer-Verlag, Berlin, 1985, pp. 118-132.

[Schmidt-Schauss 1986a] M. Schmidt-Schauss, Unification under associativity and idempotence is of type nullary, J. of Automated Reasoning 2(3):277-281, September 1986.

[Schmidt-Schauss 1986b] M. Schmidt-Schauss, Unification in many-sorted equational theories, Interner Bericht, Institut fur Informatik, Universitat Kaiserslautern; also Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 538-552.

*[Schmidt-Schauss 1986c] M. Schmidt-Schauss, Unification properties of idempotent semigroups, SEKI Report SR-86-07, Universitat Kaiserslautern, 1986.

*[Schmidt-Schauss 1986d] M. Schmidt-Schauss, Some undecidable classes of clause sets, SEKI Report SR-86-08, Universitat Kaiserslautern, 1986.

*[Schmidt-Schauss 1987a] M. Schmidt-Schauss, Unification in permutative equational theories is undecidable, SEKI Report SR-87-03, Fachbereich Informatik, Universitat Kaiserslautern, 1987.

*[Schmidt-Schauss 1987b] M. Schmidt-Schauss, Unification in a combination of arbitrary disjoint equational theories, SEKI Report SR-87-16, Universitat Kaiserslautern, 1987; also Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 378-396; also in J. of Symbolic Computation 8:51-99, 1989.

*[Schmidt-Schauss 1988a] M. Schmidt-Schauss, J.H. Siekmann, Unification algebras: An axiomatic approach to unification, equation solving and constraint solving, SEKI Report SR-88-23, Universitat Kaiserslautern, 1988.

*[Schmidt-Schauss 1988b] M. Schmidt-Schauss, Computational aspects of an order-sorted logic with term declarations, PhD thesis SEKI Report SR-88-10, FB Informatik, Universitat Kaiserslautern, FRG, 1988; also Lecture Notes in Artificial Intelligence 395, Springer-Verlag, Berlin, 1989.

[Schmidt-Schauss 1988c] M.J. Schmidt-Schauss, Two problems in unification theory, Bulletin of the EATCS 34(February 1988):273.

[Schmidt-Schauss 1988d] M. Schmidt-Schauss, Implication of clauses is undecidable, J. Theoretical Computer Science 59(1988):287-296.

[Schmidt-Schauss 1989] M. Schmidt-Schauss, Combination of unification n algorithms, J. Symbolic Computation 8(1 and 2):51-100, 1989 (special issue on unification, part 2).

[Schmitt 1986] P.H. Schmitt, Computation aspects of three-valued logic, Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 190-198.

[Schneider 1986a] H-A. Schneider, An improvement of deduction plans: refutation plans, Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 377-383.

[Schneider 1986b] H-A. Schneider, Refutation plans: Definition, soundness, and completeness, Interner Bericht, Universitat Kaiserslautern, Fachbereich Informatik, in preparation.

*[Schneider 1992a] K. Schneider, R. Kumar, T. Kropf, The FAUST-prover, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 766-770.

[Schneider 1992b] K. Schneider, R. Kumar, T. Kropf, Efficient representation and computation of tableau proofs, In Proc. International Workshop on Higher Order Logic Theorem Proving and its Applications, ed. L. Claesen and M. Gordon, Elsevier Science Publishers, IFIP/TC10/WG10.2, Leuven, Belgium, September 1992, pp. 471-492.

[Schneider 1993] K. Schneider, R. Kumar, T. Kropf, Accelerating tableaux proofs using compact representations, J. of Formal Methods in System Design, 1993.

*[Schoenfeld 1985] A.H. Schoenfeld, Mathematical problem solving, Academic Press, Inc., Orlando, Florida, 1985.

[Schonfield 1967] J.R. Schonfield, Mathematical Logic, Addison-Wesley, Reading, Massachusetts, 1967.

[Schonfeld 1983] W. Schonfeld, Proof search for unprovable formulas, Proc. GWAI-83, 7th German Workshop on Artificial Intelligence, Dassel/Solling (September 1983), Informatik-Fachberichte 76, Springer-Verlag, Berlin, 1983, pp. 207-215.

[Schonfeld 1985] W. Schonfeld, Prolog extensions based on Tableau Calculus, Proc. 9th IJCAI, Los Angeles, CA, 1985, pp. 730-732.

[Schorre 1980] V. Schorre, J. Stein, The interactive theorem prover user manual, TM-6889/000/01, System Development Co., Santa Monica, CA, November 1980.

*[Schreye 1991] D. de Schreye, B. Martens, G. Sablon, M. Bruynooghe, Compiling bottom-up and mixed derivations into top-down executable logic programs, J. Automated Reasoning 7(3):337-358, September 1991.

[Schroeder-Heister 1984] P. Schroeder-Heister, A natural extension of natural deduction, J. of Symbolic Logic 49(4), December 1984.

[Schumann 1989] J. Schumann, N. Trapp, and M. van der Koelen, SETHEO: User's Manual. Tech. report, ATP-report, Technische Universitat Munchen, 1989.

*[Schumann 1990a] J. Schumann, R. Letz, PARTHEO: A high-performance parallel theorem prover, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 40-56.

*[Schumann 1990b] J. Schumann, R. Letz, F. Kurfess, High-performance theorem provers: Efficient implementation and parallelisation (tutorial abstract), Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, p. 683.

*[Schumann 1992] J.M.Ph Schumann, KPROP - an AND-parallel theorem prover for proporsitional logic implemented in KL1, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 740-742.

[Schwartz 1978] J.T. Schwartz, Instantiation and decision procedures for certain classes of quantified set-theoretic formulas, Rept. No. 78-10, Inst. for Computer Applications in Science and Engineering, NASA Langley Research Center, Hampton, Virginia, 1978.

*[Schwind 1990] C.B. Schwind, A tableaux-based theorem prover for a decidable subset of default logic, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 528-542.

[Seidenberg 1954] A. Seidenberg, A new decision method for elementary algebra, Annals of Mathematics 60(2):365-374, September 1954.

*[Sekar 1989] R.C. Sekar, S. Pawagi, I.V. Ramakrishnan, Transforming strongly sequential rewrite systems with constructors for efficient parallel execution, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 403-418.

*[Sekar 1990] R.C. Sekar, I.V. Ramakrishnan, Programming in equational logic: beyond strong sequentiality, Proc. 5th Annual IEEE Symp. on Logic Computer Science (Philadelphia, PA, 4-7 June 1990), IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 230-241.

*[Sekar 1992] R.C. Sekar, I.V. Ramakrishnan, Programming with equations: A framework for lazy parallel evaluation, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 618-632.

[Seki 1985] H. Seki, Incorporating Generalization Heuristics into Verification of Prolog Programs, Proc. 9th IJCAI, Vol. 2, Los Angeles, CA, 18-23 August 1985, pp. 737-741.

[Sethi 1974] R. Sethi, Testing for the Church-Rosser property, JACM 21(4):671-679, October 1974.

*[Seul 1988] S. Seul, A test environment for unification algorithms, SEKI Working Paper SWP-88-03, Universitat Kaiserslautern, 1988.

[Shanin 1965] N.A. Shanin, G.V. Davydov, S. Yu Maslov, G.E. Mints, V.P. Orevkov, A.O. Slisenko, An algorithm for a machine search of a natural logical deduction in a propositional calculus, Izdat. "Nauka", Moscow, 1965; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 424-483.

[Shankar 1984] N. Shankar, Towards mechanical metamathematics, Tech. Report 43, Institute for Computing Science, Univ. of Texas at Austin, 1984; also J. of Automated Reasoning 1(4):407-434, D. Reidel Publ. Co., Dordrecht, Holland, 1985.

*[Shankar 1985] N. Shankar, A mechanical proof of the Church-Rosser theorem, Tech. Report ICSCA-CMP-45, Institute for Computing Science, Univ. of Texas at Austin, 1985; also in JACM 35 (3):475-522, July 1988.

[Shankar 1986a] N. Shankar, Checking the proof of Godel's incompleteness theorem, Tech. Report, Institute for Computing Science, Univ. of Texas at Austin, 1986.

[Shankar 1986b] N. Shankar, Proof-checking metamathematics, PhD dissertation, Dept. of CS, Univ. of Texas at Austin, Austin, TX, 1986.

[Shankar 1987] N. Shankar, A machine-checked proof of Godel's incompleteness theorem, Proc. 8th Intl. Conf. of Logic, Methodology and Philosophy Computer Science Congress, to appear.

*[Shankar 1988] N. Shankar, Observations on the use of computers in proof checking, Notices of the American Mathematical Society 35(6):804-805, July/August 1988.

*[Shankar 1992] N. Shankar, Proof search in the intuitionistic sequent calculus, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 522-536.

[Shapiro 1980] S. Shapiro, D. McKay, Inference with recursive rules, Proc. Natl Conf. on Artificial Intelligence, Stanford Univ., 1980.

[Shapiro 1981] E.Y. Shapiro, An algorithm that infers theories from facts, Proc. 7th IJCAI, Vancouver, Canada, 1981, pp. 446-451.

*[Shensa 1989] M.J. Shensa, A computational structure for the propositional calculus, Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 384-388.

[Shieber 1984] S. Shieber, L. Karttunen, F. Pereira, Notes from the unification underground, Tech. Report, SRI International TN327, 1984.

[Shimada 1974] K. Shimada, A theorem-prover for intuitionistic propositional logic, J. of Tsuda College 6:39-44, 1974. (In Japanese).

[Shimada 1978] Y. Shimada, Survey of theorem proving by computer, Denshi Gijutsu Sogo Kenkujo Chosa Hokoku, Report 195, 1978.

[Shimura 1979] M. Shimura, Resolution in a new modal logic, Proc. 6th IJCAI, Tokyo, August 1979, pp. 809-814.

[Shostak 1974] R.E. Shostak, Refutation graphs and resolution theorem proving, Harvard Univ., 1974.

[Shostak 1975] R.S. Shostak, On the completeness of the SUP-INF method, Stanford Research Inst. Rep., 1975.

[Shostak 1976] R.E. Shostak, Refutation graphs, Artificial Intelligence 7(1):51-64, 1976.

[Shostak 1977a] R.E. Shostak, On the role of unification in mechanical theorem proving, Acta Informatica 7(3):319-323, 1977.

[Shostak 1977b] R.E. Shostak, An algorithm for reasoning about equality, Proc. 5th IJCAI, MIT, Cambridge, MA, 1977, pp. 526-527; also CACM 21(7):583-585, July 1978.

[Shostak 1977c] R.E. Shostak, On the SUP-INF method for proving Presburger formulas, JACM 24(4):529-543, October 1977.

[Shostak 1977d] R.E. Shostak, An efficient decision procedure for arithmetic with function symbols, SRI Report CSL-65, Stanford Research Institute, CA, 1977.

[Shostak 1979a] R.E. Shostak, Deciding linear inequalities by computing loop residues, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979; also in JACM 28(4):769-779.

[Shostak 1979b] R. Shostak, A practical decision procedure for arithmetic with function symbols, JACM 26(2):351-360, April 1979.

[Shostak 1979c] R.E. Shostak, A graph-theoretic view of resolution theorem-proving, Report SRI International, Menlo Park, CA, 1979.

[Shostak 1981] R.E. Shostak, P.M. Melliar-Smith, Techniques for automatic deduction, AFOSR-TR-81-0853, SRI International, Menlo Park, 1981.

[Shostak 1982a] R.E. Shostak, R. Schwartz, P.M. Melliar-Smith, STP: a mechanized logic for specification and verification, Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982, pp. 32-49.

[Shostak 1982b] R.E. Shostak, Deciding combinations of theories, Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982, pp. 209-222; also JACM 31(1), 1984.

[Shostak 1984] R.E. Shostak, ed., Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), LNCS 170, Springer-Verlag, NY, 1984.

[Sibert 1969] E.E. Sibert, A machine-oriented logic incorporating the equality relation, Machine Intelligence 4, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, Edinburgh, 1969, pp. 103-133.

[Sickel 1974] S. Sickel, Growth limitations for automatic theorem proving, Board of Studies in Information Sciences, Univ. of California, Santa Cruz, CA, 1974.

[Sickel 1976a] S. Sickel, Interconnectivity graphs, IEEE Trans. on Computers C-25(6), 1976.

[Sickel 1976b] S. Sickel, A linguistic approach to automatic theorem proving, California Inst. of Information Sci., Tech. Report, August 1976.

[Sickel 1976c] S. Sickel, A search technique for clause interconnectivity graphs, IEEE Trans. on Computers C-25(8):823-835, 1976.

[Sickel 1977a] S. Sickel, Formal grammars as models of logic derivations, Proc. 5th IJCAI, MIT, Cambridge, MA, 1977, pp. 544-551.

[Sickel 1977b] S. Sickel, Automatic theorem proving, Final Progress Report, California Univ. Santa Cruz Information Sciences, May 1977.

[Sickel 1977c] S. Sickel, Variable range restrictions in resolution theorem proving, Machine Intelligence 8, ed. Elcock and Michie, Ellis Harwood Ltd., Sussex, England, 1977.

[Siekmann 1975] J. Siekmann, String unification, Memo CSM-7, Univ. of Essex, 1975.

[Siekmann 1976a] J. Siekmann, Unification of commutative terms, Memo SEKI-76-IV, Institut fur Informatik I, Universitat Karlsruhe, W. Germany, 1976.

[Siekmann 1976b] J. Siekmann, W. Stephan, Completeness and soundness of the connection graph procedure, Interner Bericht 7/76, Inst. fur Informatik I, Universitat Karlsruhe, FRG, 1976.

[Siekmann 1976c] J. Siekmann, T-unification, part I. Unification of commutative terms, Interner Bericht N. 4/76, Institut fur Informatik I, Universitat Karlsruhe, Karlsruhe, W. Germany, 1976.

[Siekmann 1978] J. Siekmann, Unification and matching problems, PhD thesis, Memo CSM-4-78, Univ. of Essex, 1978.

[Siekmann 1980] J. Siekmann, G. Wrightson, Paramodulated connection graphs, Acta Informatica 13(1980):67-86.

[Siekmann 1981a] J. Siekmann, P. Szabo, Universal unification and regular equational ACFM theories, Memo SEKI-81-III, Institut fur Informatik I, Universitat Karlsruhe, W. Germany, 1981; also Proc. 7th IJCAI, Univ. of British Columbia, Vancouver, Canada, August 1981, pp. 532-538.

[Siekmann 1981b] J. Siekmann, P. Szabo, Universal unification and a classification of equational theories, Interner Bericht 7/82, Memo SEKI-81-II, Institut fur Informatik I, Universitat Karlsruhe, W. Germany, 1981; also Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982, pp. 369-389.

[Siekmann 1981c] J. Siekmann, P. Szabo, A Noetherian rewrite system for idempotent semigroups, Proc. GWAI-81, Informatik-Fachberichte 47, ed. Siekmann, Springer-Verlag, Berlin, 1981, pp. 235-245.

[Siekmann 1981d] J. Siekmann, G. Smolka, Selection heuristics, deletion strategies and N-level terminator configurations for the connection graph, Proc. GWAI-81, Informatik-Fachberichte 47, ed. Siekmann, Springer-Verlag, Berlin, 1981, pp. 199-200.

[Siekmann 1982a] J. Siekmann, P. Szabo, A minimal unification algorithm for idempotent functions, Universitat Karlsruhe, 1982.

[Siekmann 1982b] J. Siekmann, P. Szabo, Universal unification: A survey, Proc. GWAI-82, Informatik-Fachberichte 58, ed. Wahlster, Springer-Verlag, Berlin, 1982, pp. 102-141.

[Siekmann 1982c] J. Siekmann, P. Szabo, A Noetherian and confluent rewrite system for idempotent semigroups, Semigroup Forum 25, pp. 83-100, 1982.

[Siekmann 1983a] J. Siekmann, G. Wrightson, eds., Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, Springer-Verlag, Berlin, 1983.

[Siekmann 1983b] J. Siekmann, G. Wrightson, eds., Automation of Reasoning - Classical Papers on Computational Logic, Vol. II, 1967-1970, Springer-Verlag, Berlin, 1983.

[Siekmann 1984] J.H. Siekmann, Universal unification, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 1-42.

[Siekmann 1986a] J.H. Siekmann, ed., Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), LNCS 230, Springer-Verlag, Berlin, 1986.

*[Siekmann 1986b] J.H. Siekmann, Unification theory, Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, p. vi-xxxv; also Proc. 7th European Conf. on Artificial Intelligence (ECAI-86, Brighton, UK, 20-25 July 1986), In: Advances in Artificial Intelligence -- II, ed. B. du Boulay, D. Hogg, and L. Steels, North-Holland, Amsterdam, 1987, pp. 365-400; also available from Automated Reasoning Project, Australian National Univ., Canberra, ACT.2601, Australia, 1988; also J. of Symbolic Computation 7(3,4):207-274, 1989 (special issue on unification, part one).

*[Siekmann 1986c] J. Siekmann, P. Szabo, The undecidability of the DA-unification problem, SEKI Report SR-86-19, Universitat Kaiserslautern, 1986; also available from Automated Reasoning Project, Australian National Univ., Canberra, ACT.2601, Australia.

*[Siekmann 1990] J.H. Siekmann, An introduction to unification theory, In Formal Techniques in Artificial Intelligence: A Sourcebook, ed. R.B. Banerji, Elsevier Science Publishers, Amsterdam, 1990, pp. 369-424.

[Siklossy 1971] L. Siklossy, V. Marinor, Heuristic search vs exhaustive search, Proc. 2nd IJCAI, Imperial College, London, 1971, pp. 601-607.

[Siklossy 1973] L. Siklossy, J. Roach, Proving the impossible is impossible is possible: disproofs based on hereditary partitions, Proc. 3rd IJCAI, Stanford Univ., Stanford, 1973, pp. 383-387.

[Silbert 1969] E.E. Silbert, A machine-oriented logic incorporating the equality relation, Machine Intelligence 4, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, 1969.

[Siltere 1969] M. Ya Siltere, Mechanical deduction of arithmetical identities, in Automatics and Telemechanics 6(1969):110-114.

[Silver 1986] B. Silver, Meta-Level Inference: Representing and Learning Control Information in Artificial Intelligence, Studies in Computer Science and Artificial Intelligence, North-Holland, Amsterdam, 1986, 222pp (revised version of the author's PhD thesis, DAI 1984).

[Simon 1984] D. Simon, A linear time algorithm for a subcase of second-order instantiation, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 200-223.

*[Simon 1988] D. Simon, Checking natural language proofs, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 141-150.

*[Singhal 1989] A. Singhal, Y. Patt, Unification parallelism: How much can we exploit?, Logic Programming: Proc. of the North American Conf., 1989, Vol. 2, ed. E.L. Lusk, R.A. Overbeek, MIT Press, 1989, pp. 1135-1147.

[Slagle 1965a] J.R. Slagle, A multipurpose theorem proving heuristic program that learns, Proc. IFIP Congr. 1965, 2, pp. 323-328.

[Slagle 1965b] J.R. Slagle, A proposed preference strategy using sufficiency resolution for answering questions, UCRL-14361, Lawrence Radiation Lab., Livermore, CA, 1965.

[Slagle 1965c] J.R. Slagle, Experiments with a deductive question-answering program, CACM 8(1965):792-798.

[Slagle 1967] J.R. Slagle, Automatic theorem proving with renamable and semantic resolution, JACM 14(4):687-697, October 1967; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 55-65.

[Slagle 1968] J.R. Slagle, P. Bursky, Experiments with a multipurpose theorem-proving heuristic program, JACM 15(1):85-99, 1968.

[Slagle 1969] J.R. Slagle, C.L. Chang, R.C.T. Lee, Completeness theorems for semantic resolution in consequence finding, Proc. 1st IJCAI, Washington, D.C., 1969, pp. 281-285.

[Slagle 1970a] J.R. Slagle, Interpolation theorem for resolution in lower predicate calculus, JACM 17(3):535-542, 1970.

[Slagle 1970b] J.R. Slagle, Heuristic search programs, in Theoretical Approaches to Non-numerical Problem Solving, ed. R. Banerji and M. Mesavoric, Springer-Verlag, NY, 1970, pp. 246-273.

[Slagle 1970c] J.R. Slagle, C.L. Change, R.C.T. Lee, A new algorithm for generating prime implicants, IEEE Trans. on Comp. 19(4):304-310, 1970.

[Slagle 1971a] J. Slagle, Artificial Intelligence: The Heuristic Programming Approach, McGraw-Hill, NY, 1971.

[Slagle 1971b] J.R. Slagle, D. Koniver, Finding resolution proofs and using duplicate goals in and/or trees, Information Sci. 4(3):315-342, 1971.

[Slagle 1971c] J.R. Slagle, L. Norton, Experiments with an automated theorem prover having partial ordering inference rules, Div. of Comput. Res. and Tech., Nat. Inst. of Health, Bethesda, Maryland, 1971; also CACM 16(November 1973):682-688.

[Slagle 1971d] J.R. Slagle, Automatic theorem-proving for the theories of partial and total ordering, Div. of Comput. Res and Tech. Nat. Inst. of Health, Bethesda, Maryland, 1971.

*[Slagle 1972a] J.R. Slagle, Automatic theorem proving with built-in theories including equality, partial ordering and sets, JACM 19(1):120-135, January 1972.

[Slagle 1972b] J.R. Slagle, An approach for finding c-linear complete inference systems, JACM 19(July 1972):496-516.

[Slagle 1974] J.R. Slagle, Automated theorem proving for theories with simplifiers, commutativity and associativity, JACM 21(4):622-642, October 1974.

[Slagle 1975] J.R. Slagle, L.M. Norton, Automatic theorem-proving for the theories of partial and total ordering, Comput. J. 18(February 1975):49-54.

[Slaney 1980] J.K. Slaney, Computers and relevant logic: A project in computing matrix model structures for propositional logics, Doctoral dissertation, unpublished, Australian National University, Canberra, 1980.

[Slaney 1988] J. Slaney, General Logic, available from the Automated Reasoning Project, Australian National Univ., Canberra, ACT.2601, Australia.

*[Slaney 1990] J.K. Slaney, E.L. Lusk, Parallelizing the closure computation in automated deduction, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 28-39.

*[Slaney 1991] J.K. Slaney, The Ackermann constant theorem: A computer-assisted investigation, J. Automated Reasoning 7(4):453-474, December 1991.

*[Slaney 1993] J. Slaney, SCOTT: A model-guided theorem prover, Proc. 13th IJCAI (Chambery, France, 28 August-3 September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 109-115.

[Smith 1975] R.L. Smith, W.H. Graves, L.H. Blaine, V.G. Marinov, Computer-Assisted Axiomatic Mathematics: Informal Rigor, In Computers in Education, ed. O. Lecarme and R. Lewis, North-Holland/American Elsevier, 1975, pp. 803-809.

[Smith 1981] D.R. Smith, A design for an automatic programming system, Proc. 7th IJCAI, Vancouver, B.C., Canada, 1981, pp. 1024-1027.

[Smith 1985a] D.E. Smith, Controlling inference, PhD thesis, Stanford Univ. Stanford, CA, 1985.

[Smith 1985b] D.E. Smith, M.R. Genesereth, Ordering conjunctive queries, Artificial Intelligence 26(2):171-215, 1985.

[Smith 1986a] D.E. Smith, M.R. Genesereth, M.L. Ginsberg, Controlling recursive inference, Artificial Intelligence 30(1986):343-389.

[Smith 1986b] D.E. Smith, Controlling backward inference, Knowledge Systems Laboratory Rept. Stanford Univ., Stanford, CA, 1986.

*[Smith 1988a] B.T. Smith, D.W. Loveland, An nH-Prolog implementation, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 766-767.

[Smith 1988b] B. Smith, Reference manual for the environmental theorem prover, an incarnation of AURA, Tech. report ANL-88-2, Argonne National Laboratory, Argonne, Illinois, 1998.

[Smith 1990] A. Smith, Which theorem prover? (A survey of four theorem provers), RSRE Memo 4430, Royal Signals and Radar Establishment, October 1990.

[Smolka 1982a] G. Smolka, Completeness of the connection graph proof procedure for unit-refutable clause sets, Proc. GWAI-82, 6th German Workshop on Artificial Intelligence, Bad Honnef (September 1982), Informatik-Fachberichte 58, ed. Wahlster, Springer-Verlag, Berlin, 1982, pp. 191-204.

[Smolka 1982b] G. Smolka, Completeness of the connection graph proof procedure for unit-refutable clause sets, Proc. GWAI-82, Informatik-Fachberichte 58, ed. Wahlster, Springer-Verlag, Berlin, 1982, pp. 191-204.

[Smolka 1982c] G. Smolka, Completeness and confluence properties of Kowalski's clause graph calculus, Interner Bericht 31/82, Memo SEKI-82-III, Institut fur Informatik I, Universitat Karlsruhe, W. Germany, December 1982.

*[Smolka 1986] G. Smolka, Order-sorted Horn logic: semantics and deduction, SEKI Report SR-86-17, Universitat Kaiserslautern, W. Germany, September 1986.

*[Smolka 1987] G. Smolka, W. Nutt, J. Meseguer, J.A. Goguen, Order-sorted equational computation, SEKI Report SR-87-14, Universitat Kaiserslautern, 1987; In: Resolution of Equations in Algebraic Structures: Vol 2, Rewriting Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 297-367.

[Smullyan 1963] R.M. Smullyan, A unifying principal in quantification theory, Proc. Nat. Acad. Sci. 49(1963):828-832.

[Smullyan 1968] R.M. Smullyan, First-Order Logic, Springer-Verlag, NY, 1968.

[Smullyan 1985] R.M. Smullyan, To Mock a Mockingbird, Alfred Knopf, NY, 1985.

*[Smullyan 1992] R.M. Smullyan, Puzzles and paradoxes (abstract), Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, p. 208.

[Snyder 1988] W. Snyder, J.H. Gallier, Higher-order unification revisited: complete sets of transformations, Dept. of Computer and Information Science, Univ. of Pennsylvania, 1987; also in J. of Symbolic Computation 8(1 and 2):101-140, 1989; reprinted in [Kirchner 1990c], pp. 565-604.

*[Snyder 1989a] W. Snyder, Efficient ground completion: An 0(n log n) algorithm for generating reduced sets of ground rewrite rules equivalent to a set of ground equations E, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 419-433.

[Snyder 1989b] W. Snyder, J.H. Gallier, Complete sets of transformations for general E-unification, Theoretical Computer Science 67(1989):203-260.

*[Snyder 1990] W. Snyder, Higher order E-unification, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 573-587.

*[Snyder 1991] W. Snyder, A Proof Theory for General Unification, Birkhauser, Boston, 1991.

*[Socher 1987a] R. Socher, Boolean simplification of first order formulae, SEKI Report SR-87-04, Universitat Kaiserslautern, June 1987.

*[Socher 1987b] R. Socher, An optimized transformation into conjunctive (or disjunctive) normal forms, SEKI Report SR-87-13, Universitat Kaiserslautern, December 1987; note this report has also been distributed as ``Optimized transformation between conjunctive and disjunctive normal forms.''

[Socher 1988] R. Socher, A subsumption algorithm based on characteristic matrices, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 573-581.

*[Socher 1991] R. Socher, Optimizing the clausal normal form transformation, J. Automated Reasoning 7(3):325-336, September 1991.

*[Socher-Ambrosius 1988] R. Socher-Ambrosius, Using theory resolution to simplify interpreted formulae, SEKI Report SR-88-16, Universitat Kaiserslautern, 1988; also Proc. Kunstliche Intelligenz (GWAI-88, 12. Jahrestagung, Eringerfeld, 19-23 September 1988), Informatik-Fachberichte 181, ed. W. Hoeppener, Springer-Verlag, Berlin, pp. 179-185.

[Socher-Ambrosius 1989a] R. Socher-Ambrosius, Reducing the derivation of redundant clauses in reasoning systems, SEKI Report SR-89-04, Fachbereich Informatik, Universitat Kaiserslautern, Kaiserslautern, 1989; also Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 401-406.

[Socher-Ambrosius 1989b] R. Socher-Ambrosius, Another technique for proving completeness of resolution, SEKI Report SR-89-05, Fachbereich Informatik, Universitat Kaiserslautern, Kaiserslautern, 1989.

*[Socher-Ambrosius 1989c] R. Socher-Ambrosius, Detecting redundancy caused by congruent links in clause graphs, SEKI Report SR-88-06, Universitat Kaiserslautern; also Proc. 13 German Workshop on Artificial Intelligence (GWAI-89, Eringerfeld, 18-22 September 1989), ed. D. Metzing, Springer-Verlag, Berlin, 1989, pp. 74-82.

[Soddy 1982] J.S. Soddy, On the application of relevance measures in mechanical deduction, Michigan State Univ., 94 pp., 1982.

[Sokolowski 1983a] S. Sokolowski, A note on tactics in LCF, Internal Report, CSR-140-83, Dept. of Computer Sci., Univ. of Edinburgh, Edinburgh, August 1983.

[Sokolowski 1983b] S. Sokolowski, An LCF proof of soundness of Hoare's Logic - A paper without a happy ending, Internal Report CSR-146-83, Univ. of Edinburgh, Dept. of Computer Sci., Edinburgh, 1983; also to appear in ACM Trans. Program. Languages and Systems,

[Sopena 1987] E. Sopena, Combinatorial hypermap rewriting, Proc. 2nd Intl. Conf. on Rewriting Techniques and Applications (Bordeaux, France, 25-27 May 1987), ed. P. Lescanne, LNCS 256, Springer-Verlag, Berlin, 1987, pp. 62-73.

[Soria 1984] M. Soria, J.M. Steyaert, Average efficiency of pattern matching on Lisp expressions, Proc. CAAP 84 Conf.; also LRI Report no 178, May 1984.

*[Spencer 1990] B. Spencer, Avoiding duplicate proofs, Logic Programming: Proc. of the 1990 North American Conf., ed. S. Debray and M. Hermenegildo, MIT Press, Cambridge, MA, 1990, pp. 567-584.

*[Sperschneider 1991] V. Sperschneider, G. Antoniou, Logic: A foundation for Computer Science, Addison-Wesley Publishing Company, Wokingham, England, 1991.

[Sridhar 1986] S. Sridhar, An implementation of OBJ2: an object-oriented language for abstract program specification, Proc. 6th Conf. on Foundations of Software Technology and Theoretical Computer Science, LNCS 241, ed. K.V. Nori, Springer-Verlag, 1986, pp. 81-95.

[Srinivasan 1976] C.V. Srinivasan, Theorem proving in the meta description system, ARPA SOSAP-TR-20, Dept. of Computer Sci., Rutgers Univ., 1976.

[Srivas 1984] M. Srivas, Rewrite rule based program transformation, Proc. of an NSF Workshop on the Rewrite Rule Laboratory (September 1983), ed. J.V. Guttag, D. Kapur, and D.R. Musser, General Electric, Information Systems Laboratory, Schenectady, NY, No. 84GEN008, April 1984, pp. 319-336.

*[Stabler 1993] E.P. Stabler, Jr, Parsing as non-Horn deduction, Artificial Intelligence 63(1-2):225-264, October 1993.

*[Stachniak 1990] M. Stachniak, Resolution proof systems with weak transformation rules, Proc. ISSAC '90 (Tokyo, Japan, 20-24 August 1990), ACM, NY, NY, 1990, p. 38-43.

[Stanfield 1986] C. Stanfield, D. Waltz, Toward memory-based reasoning, Thinking Machines Report, 1986.

[Staples 1980a] J. Staples, A graph-like lambda calculus for which leftmost-outermost reduction is optimal, Proc. Int. Workshop on Graph Grammars and their Applications to Computer Science and Biology, ed. V. Claus, H. Ehrig, and G. Rosenberg, LNCS 73, 1980, pp. 440-455.

[Staples 1980b] J. Staples, Computation on graph-like expresions, Theor. Comp. Sci 10(1980):171-185.

[Staples 1981] J. Staples, Efficient lazy evaluation of lambda expressions: a stack-based approach, Univ. of Queensland Dept. of Comp. Sci. Tech. Report No. 26, March 1981.

[Staples 1982] J. Staples, A new strategy for lazy evaluation of lambda expressions, Aust. Comp. Sci. Commun. 4, 1982, pp. 277-285.

[Staples 1988] J. Staples, P.J. Robinson, Efficient unification of quantified terms, J. Logic Programming 5(1988):133-149.

*[Staples 1990] J. Staples, P.J. Robinson, Structure sharing for quantified terms: Fundamentals, J. of Automated Reasoning 6(2):115-145, June 1990.

[Statman 1978] R. Statman, Bounds for proof-search and speed-up in the predicate calculus, Annals of Mathematical Logic 15:225-287, 1978.

[Statman 1980] R. Statman, Worst case exponential lower bounds for input resolution with paramodulation, SIAM J. Computing 9(1):104-110, February 1980.

*[Steinbach 1988a] J. Steinbach, Comparison of simplification orderings, SEKI Report SR-88-02, Artificial Intelligence Laboratories, Dept. of Computer Science, Universitat Kaiserslautern, W. Germany, February 1988.

*[Steinbach 1988b] J. Steinbach, Term ordering with status, SEKI Report SR-88-12, Artificial Intelligence Laboratories, Dept. of Computer Science, Universitat Kaiserslautern, W. Germany, September 1988.

*[Steinbach 1989a] J. Steinbach, Extensions and comparison of simplification orderings, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 434-448.

[Steinbach 1989b] J. Steinbach, Proving termination of associative-commutative term rewriting systems using the Knuth-Bendix ordering, SEKI Report SR-89-13, Artificial Intelligence Laboratories, Dept. of Computer Science, Universitat Kaiserslautern, W. Germany, 1989.

[Steinbach 1989c] J. Steinbach, Path and decomposition orderings for proving AC-termination, SEKI Report, Artificial Intelligence Laboratories, Dept. of Computer Science, Universitat Kaiserslautern, W. Germany, 1989.

*[Steinbach 1990] J. Steinbach, Improving associative path orderings, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 411-425.

[Stenlund 1972] S. Stenlund, Combinators, lambda-terms, and proof theory, D. Reidel, Dordrecht, The Netherlands, 1972.

[Stephan 1976] W. Stephan, J. Siekmann, Completeness and soundness of the connection graph proof procedure, Interner Bericht 7/76, Inst. f. Informatik, Univ. Karlsruhe, 1976; also Proc. AISB/GI Conf. on Artificial Intelligence (Hamburg, 18-20 July 1978), ed. C. Sleeman, Leeds Univ. Press, 1978, pp. 340-344.

[Sterling 1982a] L. Sterling, A. Bundy, L. Byrd, R. O'Keefe, and B. Silver, Solving symbolic equations with PRESS, Research Paper 171, Univ. of Edinburgh, Dept. of Artificial Intelligence, January 1982; also Proc. EUROCAM 82, LNCS 144, ed. J. Calmet, Springer-Verlag, 1982, pp. 109-116.

[Sterling 1982b] L. Sterling, A. Bundy, Meta-level inference and program verification, Research Paper 168, Univ. of Edinburgh, Dept. of Artificial Intelligence, also Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982, pp. 144-150.

[Sterling 1983] L. Sterling, IMPRESS - Meta-level concepts in theorem proving, Working Paper 119, Dept. of Artificial Intelligence, Univ. of Edinburgh, 1983.

[Sterling 1984] L. Sterling, Implementing problem-solving strategies using the meta-level. DAI Research Paper 209, Dept. of Artificial Intelligence, University of Edinburgh, 1984.

[Sterling 1987] L. Sterling, Mathematical Reasoning: A prolog program uses heuristic to solve equations, Byte 12(11):177-180, October 1987.

[Stevens 1987a] A. Stevens, A rational reconstruction of Boyer and Moore's technique for constructing induction formulas, DAI Research Paper 360, Dept. of Artificial Intelligence, Edinburgh, 1987; also Proc. 8th ECAI-88, ed. Y. Kodratoff, pp. 565-570, 1988.

[Stevens 1987b] R.L. Stevens, Some experiments in nonassociative ring theory with an automated theorem prover, J. of Automated Reasoning 3(2):211-221, June 1987.

*[Stevens 1988a] R. L. Stevens, Challenge problems for nonassociative rings for theorem provers, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 730-734.

*[Stevens 1988b] A. Stevens, A rational reconstruction of Boyer and Moore's technique for constructing induction formulaes, Proc. 8th ECAI, Institut fur Informatik der Technischen Universitat Munchen, 1-5 August 1988, pp. 565-570.

[Stickel 1974] M.E. Stickel, The programmable strategy theorem prover: an implementation of the linear MESON procedure, Tech. Report, Carnegie-Mellon Univ. Comput. Sci. Dept., June 1974.

[Stickel 1975] M.E. Stickel, A complete unification algorithm for associative-commutative functions, Proc. 4th IJCAI, Tbilisi, Georgia, USSR, 1975, pp. 71-76; also JACM 28(3):423-434, 1981.

[Stickel 1976] M.E. Stickel, Unification algorithms for artificial intelligence languages, PhD thesis, Carnegie-Mellon Univ., 1976.

[Stickel 1977] M.E. Stickel, Mechanical theorem proving and artificial intelligence languages, PhD thesis, Carnegie-Mellon Univ., Pittsburgh, 1977.

[Stickel 1981] M.E. Stickel, A complete unification algorithm for associative-commutative functions, JACM 28(3):423-434, July 1981.

[Stickel 1982] M.E. Stickel, A nonclausal connection-graph resolution theorem-proving program, Tech. Note 268, SRI International, Artificial Intelligence Center, Menlo Park, CA, 1982; also Proc. AAAI-82, Natl Conf. on Artificial Intelligence (Pittsburgh, PA, Carnegie-Mellon Univ., August 1982), Morgan Kaufmann Publishers, Los Altos, CA, 1982, pp. 229-233.

[Stickel 1983a] M.E. Stickel, A note on leftmost-innermost term reduction, ACM SIGSAM Bulletin 17(3&4), issue no. 67 & 68, August and November 1983, pp. 19-20.

[Stickel 1983b] M.E. Stickel, Theory resolution: Building in nonequational theories, Proc. 3rd Natl Conf. on Artificial Intelligence, Washington, D.C., American Association for Artificial Intelligence, August 1983, pp. 391-397.

[Stickel 1984a] M.E. Stickel, A case study of theorem proving by the Knuth-Bendix method discovering that (x cubed = x) implies ring commutativity, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 248-258.

[Stickel 1984b] M.E. Stickel, A Prolog technology theorem prover, New Generation Computing 2(4):371-383, 1984; also 1984 Intl. Symp. on Logic Programming, Atlantic City, New Jersey, 6-9 February 1984, pp. 211-217.

[Stickel 1985a] M.E. Stickel, Automated deduction by theory resolution, J. of Automated Reasoning 1(4):333-355, D. Reidel Publ. Co., Dordrecht, Holland, 1985; also Proc. 9th IJCAI, Vol. 2, Los Angeles, CA, 18-23 August 1985, pp. 1181-1186.

*[Stickel 1985b] M.E. Stickel, W.M. Tyson, An analysis of consecutively bounded depth-first search with applications in automated deduction, Proc. 9th IJCAI, Los Angeles, CA, 1985, pp. 1073-1075.

[Stickel 1986a] M.E. Stickel, Schubert's steamroller problem: formulations and solutions, J. of Automated Reasoning 2(1):89-101, D. Reidel Publ. Co., Dordrecht, Holland, 1986.

[Stickel 1986b] M.E. Stickel, A Prolog technology theorem prover: Implementation by an extended PROLOG compiler, Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 573-587.

[Stickel 1986c] M.E. Stickel, The KLAUS Automated Theorem Proving System, Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 703-704.

*[Stickel 1986d] M.E. Stickel, An introduction to automated deduction, In Fundamentals of Artificial Intelligence, ed. W. Bibel and Ph. Jorrand, LNCS 232, Springer-Verlag, Berlin, 1986, pp. 75-132.

[Stickel 1987] M.E. Stickel, A comparison of the variable-abstraction and constant-abstraction methods for associative-commutative unification, J. of Automated Reasoning 3(3):285-289, September 1987.

*[Stickel 1988a] M.E. Stickel, The KLAUS automated deduction system, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 750-751.

*[Stickel 1988b] M.E. Stickel, A Prolog Technology Theorem Prover, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 752-753.

*[Stickel 1988c] M.E. Stickel, A Prolog Technology Theorem Prover: Implementation by an extended Prolog compiler, J. Automated Reasoning 4(4):353-380, December 1988.

*[Stickel 1988d] M.E. Stickel, Resolution theorem proving, Annual Review of Computer Science 3, ed. J.F. Traub, B.J. Grosz, B.W. Lampson, and N.H. Nilsson, Annual Reviews Inc., 1988, pp. 285-316.

[Stickel 1989a] M.E. Stickel, A Prolog technology theorem prover: A new exposition and implementation in Prolog, Tech. Note 464, Artificial Intelligence Center, SRI International, Menlo Park, CA, June 1989.

[Stickel 1989b] M.E. Stickel, The path-indexing method for indexing terms, Tech. Note 473, Artificial Intelligence Center, SRI International, 1989 (check date).

*[Stickel 1990a] M.E. Stickel, A Prolog technology theorem prover (abstract), Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 673-674.

*[Stickel 1990b] M.E. Stickel, A Prolog technology theorem prover: A new exposition and implementation in Prolog, Proc. Intl. Symp. on Design and Implementation of Symbolic Computation Systems (DISCO '90, Capri, Italy 10-12 April 1990), LNCS 429, ed. A Miola, Springer-Verlag, 1990, pp. 154-163.

[Stillman 1972] R.B. Stillman, Associative processing techniques for theorem proving, RADC-TR-72-56, Rome Air Dev. Center, NY, April 1972.

[Stillman 1973] R.B. Stillman, The concept of weak substitution in theorem proving, JACM 20(4):648-667, October 1973.

*[Stokes 1990] T. Stokes, Grobner bases in exterior algebra, J. of Automated Reasoning 6(3):233-250, September 1990.

[Strandh 1987] R. Strandh, Optimizing equational programs, Proc. 2nd Intl. Conf. on Rewriting Techniques and Applications (Bordeaux, France, 25-27 May 1987), ed. P. Lescanne, LNCS 256, Springer-Verlag, Berlin, 1987, pp. 13-24.

[Strandh 1988] R.I. Strandh, Compiling equational programs into efficient machine code, PhD thesis, The Johns Hopkins Univ., Dept. of Computer Science, Baltimore, Maryland, 1988.

*[Strandh 1989] R.I. Strandh, Classes of equational programs that compile into efficient machine code, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 449-461.

*[Subrahmanian 1988a] V.S. Subrahmanian, Query processing in quantitative logic programming, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 81-100.

*[Subrahmanian 1988b] V.S. Subrahmanian, Z.D. Umrigar, QUANTLOG: A system for approximate reasoning in inconsistent formal systems, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 746-747.

[Suppes 1981] P. Suppes, University-level computer-assisted instruction at Stanford: 1968-1981, Institute for Mathematical Studies in the Social Sciences, Stanford Univ., Stanford, CA, 1981.

[Suppes 1984] P. Suppes, The next generation of interactive theorem provers, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 303-315.

[Suppes 1989] P. Suppes, S. Takahashi, An interactive calculus theorem-prover for continuity properties, J. Symbolic Comput. 7(6):573-590, June 1989.

[Sutcliffe 1989] G. Sutcliffe, A general clause theorem prover written in Prolog, Research Report 89//2, Western Australian College of Adv. Ed., Dept. of Computer Studies, 1989.

*[Sutcliffe 1990] G. Sutcliffe, A general clause theorem prover (abstract), Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 675-676.

*[Sutcliffe 1992a] G. Sutcliffe, Linear-input subset analysis, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 268-280.

*[Sutcliffe 1992b] G. Sutcliffe, The semantically guided linear deduction system, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 677-680.

[Suttner 1989] C.B. Suttner, Learning heuristics for automated theorem proving, Diploma thesis, Thesis Univ. Munich, May 1989.

*[Suttner 1990] C. Suttner, W. Ertel, Automatic acquisition of search guiding heuristics, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 470-484.

[Suzuki 1975] N. Suzuki, Verifying programs by algebraic and logical reduction, Proc. Intl. Conf. on Reliable Software (IEEE), 1975, pp. 473-481.

[Suzuki 1977] N. Suzuki, D. Jefferson, Verification decidability of Presburger array programs, Proc. Conf. on Theor. Comput. Science, Univ. of Waterloo, August 1977.

[Swain 1986] M.J. Swain, J.L. Mundy, Experiments in using a geometry theorem prover to prove and develop theorems in computer vision, Proc. IEEE Conf. on Robotics and Automation, San Francisco, CA, 1986, pp. 280-285.

[Szabo 1981a] P. Szabo, J. Siekmann, Universal unification, Univ. Karlsruhe, 1981.

[Szabo 1981b] P. Szabo, J. Siekmann, A minimal unification algorithm for idempotent functions, Univ. Karlsruhe, 1981.

[Szabo 1982a] P. Szabo, E. Unvericht, The unification problem for distributive terms, Univ. Karlsruhe, 1982.

[Szabo 1982b] P. Szabo, Undecidability of the DA-unification problem, Proc. GWAI, Springer-Verlag, 1982.

[Takasu 1978] A.S. Takasu, Proofs and programs, Proc. 3rd IBM Symp. on the Mathematical Foundations of Computer Science, Kansai, 1978.

[Tammet 1990] T. Tammet, The resolution program, able to decide some solvable classes, Proc. COLOG-88: Intl. Conf. on Computer Logic, LNCS 417, Springer-Verlag, 1990, pp. 300-312.

*[Tang 1989] T.G. Tang, Temporal logic CTL + PROLOG, J. Automated Reasoning 5(1):49-65, March 1989.

*[Tang 1991] T.G. Tang, Programming in temporal-nonmonotonic reasoning, J. Automated Reasoning 7(3):383-401, September 1991.

*[Tanimoto 1987] S.L. Tanimoto, The Elements of Artificial Intelligence: An Introduction using LISP, Computer Science Press, Rockville, MD 20850, 1987.

[Tarjan 1975] R.E. Tarjan, Efficiency of a good but not linear set union algorithm, JACM 22(2):215-225, 1975.

[Tarjan 1984] R.E. Tarjan, J. Van Leeuwen, Worst-case analysis of set union algorithms, JACM 31(2):245-281, April 1984.

[Tarski 1948] A. Tarski, A Decision Method for Elementary Algebra and Geometry, The RAND Corp., Santa Monica, 1948; 2nd Edition, Univ. of California Press, Berkeley and Los Angeles, 1951.

[Tarski 1968] A. Tarski, Equational logic and equational theories of algebra, In: Contributions to Mathematical Logic, ed. Schmidt et al., North-Holland, 1968.

*[Tarver 1990] M. Tarver, An examination of the Prolog technology theorem-prover, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 322-335.

[Tauts 1964] A. Tauts, Solution of Logical Equations in the First Order Predicate Calculus by the Iteration Method, Proc. Inst. Phys. Astr. of the Acad. Sci. Est., No. 24, 1964, pp. 17-24.

[Teitelbaum 1981] T. Teitelbaum, T.W. Reps, The Cornell program synthesizer: a syntax-directed programming environment, CACM 24(9): 563-573, 1981.

*[Tennant 1992] N. Tennant, Autologic, Edinburgh University Press, Edinburgh, 1992.

*[Thatte 1985] S.R. Thatte, On the correspondence between two classes of reduction systems, Information Processing Letters 20(2):83-85, February 1985.

[Thatte 1987] S.R. Thatte, A refinement of strong sequentiality for term rewriting with constructors, Information and Computing 72(1):1987.

[Thiel 1984] J.J. Thiel, A new completeness test, Proc. of an NSF Workshop on the Rewrite Rule Laboratory (September 1983), ed. J.V. Guttag, D. Kapur, and D.R. Musser, General Electric, Information Systems Laboratory, Schenectady, NY, No. 84GEN008, April 1984, pp. 299-300.

[Thistlewaite 1984] P.B. Thistlewaite, Automated theorem-proving in non-classical logics, PhD thesis, Australian; also with M.A. McRobbie and R.K. Meyer, Pittman, London, and Wiley, New York, 1988.

[Thistlewaite 1985] P.B. Thistlewaite, M.A. McRobbie, R.K. Meyer, Advanced theorem-proving techniques for relevant logics, Logique et Analyse 28(1985):233-256.

[Thistlewaite 1986] P.B. Thistlewaite, M.A. McRobbie, R.K. Meyer, The KRIPKE Automated Theorem Proving System, Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 705-706.

*[Thistlewaite 1988] P.B. Thistlewaite, M.A. McRobbie, R.K. Meyer, Automated Theorem-Proving in Non-Classical Logics, Research Notes in Theoretical Computer Science, Pitman, London, and John Wiley & Sons, Inc., New York, 1988.

*[Thistlewaite 1991] P.B. Thistlewaite, M.A. McRobbie, Approaching hard non-classical problems, J. Automated Reasoning 7(4):635-637, December 1991.

[Thomas 1984] C. Thomas, RRLab - Rewrite rule labor, Memo SEKI-84-01, Fachbereich Informatik, Universitat Kaiserslautern, Kaiserslautern, West Germany, 1984.

[Thompson 1981] D.H. Thompson, R.W. Erickson, eds., AFFIRM Reference Manual, USC Information Sciences Institute, Marina Dey Ray, CA, 1981.

[Tiden 1985a] E. Tiden, S. Arnborg, Unification problems with one-sided distributivity, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985. pp. 398-406; also J. of Symbolic Computation 3(1 and 2):183-202, February/April 1987.

[Tiden 1985b] E. Tiden, Unification in combinations of theories with disjoint sets of function symbols, Royal Institute of Technology, Dept. of Computing Science S-100 44 Stockholm, Sweden, 1985.

[Tiden 1986a] E. Tiden, Unification in combinations of collapse-free theories with disjoint sets of function symbols, Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 431-449.

[Tiden 1986b] E. Tiden, First-order unification in combinations of equational theories, PhD thesis, Royal Institute of Technology, Stockholm, Sweden, 1986.

[Tison 1967] P. Tison, Generalized consensus theory and application to the minimization of boolean functions, IEEE Trans. on Comp. 16(4):446-456, 1967.

*[Tison 1989] S. Tison, Fair termination is decidable for ground systems, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 462-476.

[Toledo 1975] S.A. Toledo, Tableau systems for first order number theory and certain higher order theories. In Lecture Notes in Mathematics 447, Springer-Verlag, NY, 1975.

*[Tour 1990] T.B. de la Tour, Minimizing the number of clauses by renaming, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 558-572.

[Townley 1980] J.A. Townley, A pragmatic approach to resolution-based theorem proving, Computer and Information Sciences 9(2):93-116, 1980.

[Toyama 1983] Y. Toyama, On the commutativity of term rewriting systems, Trans. IECE, Japan, J66-D, 12, 1983, pp. 1370-1375.

[Toyama 1984] Y. Toyama, On equivalence transformations for term rewriting systems, Proc. RIMS Symp. on Software Science and Engineering II (Kyoto, Japan), ed. E. Goto, K. Araki, and T. Yuasa, LNCS 220, Springer-Verlag, Berlin, 1984, pp. 44-61.

[Toyama 1986] Y. Toyama, How to prove equivalence of term rewriting systems without induction, Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 118-127.

[Toyama 1987a] Y. Toyama, On the Church-Rosser property for the direct sum of term rewriting systems, JACM 34(1):128-143, January 1987.

[Toyama 1987b] Y. Toyama, Counterexamples to termination for the direct sum of term rewriting systesm, Information Processing Letters 25(1987):141-143.

*[Toyama 1988a] Y. Toyama, Confluent term rewriting systems with membership conditions, Proc. 1st Intl. Workshop on Conditional Term Rewriting Systems (Orsay, France, 8-10 July 1987), ed. S. Kaplan and J.-P. Jouannaud, LNCS 308, Springer-Verlag, Berlin, 1988, pp. 228-241.

[Toyama 1988b] Y. Toyama, Commutativity of term rewriting systems, In Programming of Future Generation Computer II, ed. K. Fuchi and L. Kott, North-Holland, 1988, pp. 393-407.

*[Toyama 1989] Y. Toyama, J.W. Klop, H.P. Barendregt, Termination for the direct sum of left-linear term rewriting systems, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 477-491.

[Traugott 1986a] J. Traugott, Nested resolution, Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 394-402.

[Traugott 1986b] J. Traugott, Deductive synthesis of sorting programs, Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 641-660.

[Travis 1964] L.G. Travis, Experiments with AI theorem utilizing program, AFIPS Conf. Proc. 25, SJCL, Spartan Books, Baltimore, Mo., 1964, pp. 339-358.

[Treitel 1986] R. Treitel, Sequentialization of logic programs, PhD thesis, Stanford Univ., 1986.

[Treitel 1987] R. Treitel, M.R. Genesereth, Choosing directions for rules, J. of Automated Reasoning 3(4):395-431, December 1987.

[Trum 1978] P. Trum, G. Winterstein, Description, implementation, and practical comparison of unification algorithms, Interner Bericht 6/78, Fachbereich Informatik, Universitat Kaiserslautern, 1978.

[Tseitin 1968] G.S. Tseitin, On the complexity of derivations in the propositional calculus, In: Studies in Constructive Mathematics Logic, Part II, ed. Slisenko, A.O., 1968, pp. 115-125.

[Tseitin 1983] G.S. Tseitin, On the complexity of derivation in propositional calculus, in Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 466-483; also Structures in Constructive Mathematics and Mathematical Logic Part II, ed. A.O. Siliosenko, 1968, pp. 115-125.

*[Tuominen 1990] H. Tuominen, Dynamic logic as a uniform framework for theorem proving in intensional logic, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 514-527.

[Turner 1984] R. Turner, Logics for Artificial Intelligence, Halsted Press (John Wiley & Sons), NY, 1984.

[Turing 1950] A.M. Turing, Computing machinery and intelligence, Mind, 1950, pp. 433-460.

[Tyson 1979] M. Tyson, W.W. Bledsoe, Conflicting bindings and generalized substitutions, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979, pp. 14-18.

[Tyson 1981] W.M. Tyson, APRVR: A priority-ordered agenda theorem prover, PhD Dissertation, Univ. of Texas at Austin, August 1981; also Proc. AAAI National Conf., Pittsburgh, PA, August 1982, pp. 225-228.

[Tyson 1982] M. Tyson, Proof methods in an agenda-based natural-deduction prover, Proc. AAAI-82, Natl Conf. on Artificial Intelligence, Carnegie-Mellon Univ., 1982, pp. 225-228.