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. AitKaci, M. Nivat, Academic Press, Inc., San Diego, 1989,
pp. 411444.
[Sacerdoti 1974] E. Sacerdoti, Planning in a hierarchy of
abstraction spaces, Artificial Intelligence 5(1974):115135.
[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, 1317 July 1987, Vol. 2, pp.
649654.
*[Sacks 1987c] E. Sacks, Piecewise linear reasoning, Proc. 6th
Natl Conf. on Artificial Intelligence (AAAI 87), Seattle,
Washington, 1317 July 1987, Vol. 2, pp. 655659.
*[Sacks 1989] E. Sacks, An approximate solver for symbolic
equations, Proc. 11th IJCAI (Detroit, Michigan, USA, 2025 August
1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 431434.
[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 statespace search, Proc.
8th National Conf. on Artificial Intelligence (AAAI90, July
29August 3, 1990), AAAI Press/MIT Press, 1990, pp. 227233.
[Samet 1980] H. Samet, Efficient online proofs of equalities
and inequalities of formulas, IEEE Trans. on Computers
C29(1):2830, January 1980.
[Sandewall 1969] E.J. Sandewall, A propertylist 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 BSUTminimal refinement: A
forbidden substitution refinement, DCSTM10, Dept. of Computer
Sci., Rutgers Univ., June 1977.
[Sandford 1977b] D.M. Sandford, Formal specifications of models
for semantic theorem proving strategies, ARPA SOSAPTR32, Dept.
of Computer Sci., Rutgers Univ., 1977.
[Sandford 1977c] D.M. Sandford, Hereditarylock resolution: A
resolution refinement combining a strong model strategy with lock
resolution, ARPA SOSAPTR30, 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,
SpringerVerlag, NY, 1980.
[Sandford 1980b] D.M. Sandford, A mechanism for resolution
refinements based on back substitutions, DCSTR77, Dept. of
Computer Sci., Rutgers Univ., December 1980.
[Sannella 1983] D.T. Sannella, R.M. Burstall, Structured
theories in LCF, Internal Report, CSR12983, 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):19, January 1989. *[Sasaki
1986] T. Sasaki, Simplification of algebraic expression by
multiterm rewriting rules, Proc. 1986 ACMSIGSAM Symp. on Symbolic
and Algebraic Computation (SYMSAC '86, Univ. of Waterloo,
Waterloo, Ontario, 2123 July 1986), ed. B.W. Char, ACM, New York,
NY, 1986, pp. 115119.
*[Satz 1990] R.W. Satz, EXPERT THINKER: An adaptation of
FProlog to microcomputers (abstract), Proc. 10th Intl. Conf. on
Automated Deduction (CADE10, Kaiserslautern, FRG, July 1990),
Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel,
SpringerVerlag, Berlin, 1990, pp. 671672.
[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, STANCS861124, Stanford Univ.
Computer Science, June 1986.
*[Schagrin 1985] M.L. Schagrin, W.J. Rapaport, R.R. Dipert,
Logic: A Computer Approach, McGrawHill Book Company, New York,
1985.
*[Scheidhauer 1988] R. Scheidhauer, G. Seul, A test environment
for unification algorithms, SEKI Working Paper SWP8803,
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, 25 June 1987), ed. J.H. Davenport, LNCS 378,
SpringerVerlag, Berlin, 1989, pp. 300310.
*[Schmerl 1987] R. U. Schmerl, Resolution on formula trees,
Proc. 11th German Workshop on Artificial Intelligence (GWAI87,
Geseke, September 28October 2, 1987), ed. K. Morik,
SpringerVerlag, Berlin, 1987, pp. 211220; also Acta Informatica
25(4):425438, 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):403408, September 1989.
[Schmidt 1983a] D. Schmidt, A programming notation for tactical
reasoning, Internal Report, CSR14183, Univ. of Edinburgh, Dept.
of Computer Sci., Edinburgh, September 1983; also Proc. 7th Conf.
on Automated Deduction, ed. R.E. Shostak, SpringerVerlag, LNCS
170, 1984, pp. 445459.
*[Schmidt 1983b] D. Schmidt, Natural deduction theorem proving
in set theory, Internal Report, CSR14283, 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 (CADE7,
Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, SpringerVerlag,
NY, 1984, pp. 445459.
[SchmidtSchauss 1985a] M. SchmidtSchauss, Mechanical
generation of sorts in clause sets, Interner Bericht MK856,
Fachber, Informatik, Universitat Kaiserslautern, 1985.
[SchmidtSchauss 1985b] M.A. SchmidtSchauss, A manysorted
calculus with polymorphic functions based on resolution and
paramodulation, Internal Report Memo SEKI85IIKL, Fachbereich
Informatik, Universitat Kaiserslautern, 1985; also Proc. 9th
IJCAI, Los Angeles, CA, August 1985, pp. 11621168.
[SchmidtSchauss 1985c] M.A. SchmidtSchauss, Unification in a
manysorted calculus with declarations, Proc. GWAI85, 9th German
Workshop on Artificial Intelligence (Dassel/Solling, FRG, 2327
September 1985), InformatikFachberichte 118, ed. H. Stoyan,
SpringerVerlag, Berlin, 1985, pp. 118132.
[SchmidtSchauss 1986a] M. SchmidtSchauss, Unification under
associativity and idempotence is of type nullary, J. of Automated
Reasoning 2(3):277281, September 1986.
[SchmidtSchauss 1986b] M. SchmidtSchauss, Unification in
manysorted equational theories, Interner Bericht, Institut fur
Informatik, Universitat Kaiserslautern; also Proc. 8th Intl. Conf.
on Automated Deduction (CADE8, Oxford, England, July 27August 1,
1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986,
pp. 538552.
*[SchmidtSchauss 1986c] M. SchmidtSchauss, Unification
properties of idempotent semigroups, SEKI Report SR8607,
Universitat Kaiserslautern, 1986.
*[SchmidtSchauss 1986d] M. SchmidtSchauss, Some undecidable
classes of clause sets, SEKI Report SR8608, Universitat
Kaiserslautern, 1986.
*[SchmidtSchauss 1987a] M. SchmidtSchauss, Unification in
permutative equational theories is undecidable, SEKI Report
SR8703, Fachbereich Informatik, Universitat Kaiserslautern,
1987.
*[SchmidtSchauss 1987b] M. SchmidtSchauss, Unification in a
combination of arbitrary disjoint equational theories, SEKI Report
SR8716, Universitat Kaiserslautern, 1987; also Proc. 9th Intl.
Conf. on Automated Deduction (CADE9, Argonne, Illinois, 2326 May
1988), ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag,
Berlin, 1988, pp. 378396; also in J. of Symbolic Computation
8:5199, 1989.
*[SchmidtSchauss 1988a] M. SchmidtSchauss, J.H. Siekmann,
Unification algebras: An axiomatic approach to unification,
equation solving and constraint solving, SEKI Report SR8823,
Universitat Kaiserslautern, 1988.
*[SchmidtSchauss 1988b] M. SchmidtSchauss, Computational
aspects of an ordersorted logic with term declarations, PhD
thesis SEKI Report SR8810, FB Informatik, Universitat
Kaiserslautern, FRG, 1988; also Lecture Notes in Artificial
Intelligence 395, SpringerVerlag, Berlin, 1989.
[SchmidtSchauss 1988c] M.J. SchmidtSchauss, Two problems in
unification theory, Bulletin of the EATCS 34(February 1988):273.
[SchmidtSchauss 1988d] M. SchmidtSchauss, Implication of
clauses is undecidable, J. Theoretical Computer Science
59(1988):287296.
[SchmidtSchauss 1989] M. SchmidtSchauss, Combination of
unification n algorithms, J. Symbolic Computation 8(1 and
2):51100, 1989 (special issue on unification, part 2).
[Schmitt 1986] P.H. Schmitt, Computation aspects of threevalued
logic, Proc. 8th Intl. Conf. on Automated Deduction (CADE8,
Oxford, England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS
230, SpringerVerlag, Berlin, 1986, pp. 190198.
[Schneider 1986a] HA. Schneider, An improvement of deduction
plans: refutation plans, Proc. 8th Intl. Conf. on Automated
Deduction (CADE8, Oxford, England, July 27August 1, 1986), ed.
J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp.
377383.
[Schneider 1986b] HA. Schneider, Refutation plans: Definition,
soundness, and completeness, Interner Bericht, Universitat
Kaiserslautern, Fachbereich Informatik, in preparation.
*[Schneider 1992a] K. Schneider, R. Kumar, T. Kropf, The
FAUSTprover, Proc. 11th Intl. Conf. on Automated Deduction
(CADE11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur,
Lecture Notes in Artificial Intelligence 607, SpringerVerlag,
Berlin, 1992, pp. 766770.
[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.
471492.
[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,
AddisonWesley, Reading, Massachusetts, 1967.
[Schonfeld 1983] W. Schonfeld, Proof search for unprovable
formulas, Proc. GWAI83, 7th German Workshop on Artificial
Intelligence, Dassel/Solling (September 1983),
InformatikFachberichte 76, SpringerVerlag, Berlin, 1983, pp.
207215.
[Schonfeld 1985] W. Schonfeld, Prolog extensions based on
Tableau Calculus, Proc. 9th IJCAI, Los Angeles, CA, 1985, pp.
730732.
[Schorre 1980] V. Schorre, J. Stein, The interactive theorem
prover user manual, TM6889/000/01, System Development Co., Santa
Monica, CA, November 1980.
*[Schreye 1991] D. de Schreye, B. Martens, G. Sablon, M.
Bruynooghe, Compiling bottomup and mixed derivations into
topdown executable logic programs, J. Automated Reasoning
7(3):337358, September 1991.
[SchroederHeister 1984] P. SchroederHeister, 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, ATPreport, Technische
Universitat Munchen, 1989.
*[Schumann 1990a] J. Schumann, R. Letz, PARTHEO: A
highperformance parallel theorem prover, Proc. 10th Intl. Conf.
on Automated Deduction (CADE10, Kaiserslautern, FRG, July 1990),
Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel,
SpringerVerlag, Berlin, 1990, pp. 4056.
*[Schumann 1990b] J. Schumann, R. Letz, F. Kurfess,
Highperformance theorem provers: Efficient implementation and
parallelisation (tutorial abstract), Proc. 10th Intl. Conf. on
Automated Deduction (CADE10, Kaiserslautern, FRG, July 1990),
Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel,
SpringerVerlag, Berlin, 1990, p. 683.
*[Schumann 1992] J.M.Ph Schumann, KPROP  an ANDparallel
theorem prover for proporsitional logic implemented in KL1, Proc.
11th Intl. Conf. on Automated Deduction (CADE11, Saratoga
Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in
Artificial Intelligence 607, SpringerVerlag, Berlin, 1992, pp.
740742.
[Schwartz 1978] J.T. Schwartz, Instantiation and decision
procedures for certain classes of quantified settheoretic
formulas, Rept. No. 7810, Inst. for Computer Applications in
Science and Engineering, NASA Langley Research Center, Hampton,
Virginia, 1978.
*[Schwind 1990] C.B. Schwind, A tableauxbased theorem prover
for a decidable subset of default logic, Proc. 10th Intl. Conf. on
Automated Deduction (CADE10, Kaiserslautern, FRG, July 1990),
Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel,
SpringerVerlag, Berlin, 1990, pp. 528542.
[Seidenberg 1954] A. Seidenberg, A new decision method for
elementary algebra, Annals of Mathematics 60(2):365374, 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, 35
April 1989), ed. N. Dershowitz, SpringerVerlag, NY, 1989, pp.
403418.
*[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, 47 June
1990), IEEE Computer Society Press, Los Alamitos, CA, 1990, pp.
230241.
*[Sekar 1992] R.C. Sekar, I.V. Ramakrishnan, Programming with
equations: A framework for lazy parallel evaluation, Proc. 11th
Intl. Conf. on Automated Deduction (CADE11, Saratoga Springs, NY,
USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial
Intelligence 607, SpringerVerlag, Berlin, 1992, pp. 618632.
[Seki 1985] H. Seki, Incorporating Generalization Heuristics
into Verification of Prolog Programs, Proc. 9th IJCAI, Vol. 2, Los
Angeles, CA, 1823 August 1985, pp. 737741.
[Sethi 1974] R. Sethi, Testing for the ChurchRosser property,
JACM 21(4):671679, October 1974.
*[Seul 1988] S. Seul, A test environment for unification
algorithms, SEKI Working Paper SWP8803, 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,
19571966, ed. J. Siekmann and G. Wrightson, SpringerVerlag,
Berlin, 1983, pp. 424483.
[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):407434, D.
Reidel Publ. Co., Dordrecht, Holland, 1985.
*[Shankar 1985] N. Shankar, A mechanical proof of the
ChurchRosser theorem, Tech. Report ICSCACMP45, Institute for
Computing Science, Univ. of Texas at Austin, 1985; also in JACM 35
(3):475522, 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, Proofchecking metamathematics, PhD
dissertation, Dept. of CS, Univ. of Texas at Austin, Austin, TX,
1986.
[Shankar 1987] N. Shankar, A machinechecked 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):804805, July/August 1988.
*[Shankar 1992] N. Shankar, Proof search in the intuitionistic
sequent calculus, Proc. 11th Intl. Conf. on Automated Deduction
(CADE11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur,
Lecture Notes in Artificial Intelligence 607, SpringerVerlag,
Berlin, 1992, pp. 522536.
[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. 446451.
*[Shensa 1989] M.J. Shensa, A computational structure for the
propositional calculus, Proc. 11th IJCAI (Detroit, Michigan, USA,
2025 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp.
384388.
[Shieber 1984] S. Shieber, L. Karttunen, F. Pereira, Notes from
the unification underground, Tech. Report, SRI International
TN327, 1984.
[Shimada 1974] K. Shimada, A theoremprover for intuitionistic
propositional logic, J. of Tsuda College 6:3944, 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. 809814.
[Shostak 1974] R.E. Shostak, Refutation graphs and resolution
theorem proving, Harvard Univ., 1974.
[Shostak 1975] R.S. Shostak, On the completeness of the SUPINF
method, Stanford Research Inst. Rep., 1975.
[Shostak 1976] R.E. Shostak, Refutation graphs, Artificial
Intelligence 7(1):5164, 1976.
[Shostak 1977a] R.E. Shostak, On the role of unification in
mechanical theorem proving, Acta Informatica 7(3):319323, 1977.
[Shostak 1977b] R.E. Shostak, An algorithm for reasoning about
equality, Proc. 5th IJCAI, MIT, Cambridge, MA, 1977, pp. 526527;
also CACM 21(7):583585, July 1978.
[Shostak 1977c] R.E. Shostak, On the SUPINF method for proving
Presburger formulas, JACM 24(4):529543, October 1977.
[Shostak 1977d] R.E. Shostak, An efficient decision procedure
for arithmetic with function symbols, SRI Report CSL65, Stanford
Research Institute, CA, 1977.
[Shostak 1979a] R.E. Shostak, Deciding linear inequalities by
computing loop residues, Proc. 4th Workshop on Automated Deduction
(CADE4, Austin, Texas, 13 February 1979), ed. W.H. Joyner, 1979;
also in JACM 28(4):769779.
[Shostak 1979b] R. Shostak, A practical decision procedure for
arithmetic with function symbols, JACM 26(2):351360, April 1979.
[Shostak 1979c] R.E. Shostak, A graphtheoretic view of
resolution theoremproving, Report SRI International, Menlo Park,
CA, 1979.
[Shostak 1981] R.E. Shostak, P.M. MelliarSmith, Techniques for
automatic deduction, AFOSRTR810853, SRI International, Menlo
Park, 1981.
[Shostak 1982a] R.E. Shostak, R. Schwartz, P.M. MelliarSmith,
STP: a mechanized logic for specification and verification, Proc.
6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138,
SpringerVerlag, Berlin, 1982, pp. 3249.
[Shostak 1982b] R.E. Shostak, Deciding combinations of theories,
Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138,
SpringerVerlag, Berlin, 1982, pp. 209222; also JACM 31(1), 1984.
[Shostak 1984] R.E. Shostak, ed., Proc. 7th Intl. Conf. on
Automated Deduction (CADE7, Napa, CA, May 1984), LNCS 170,
SpringerVerlag, NY, 1984.
[Sibert 1969] E.E. Sibert, A machineoriented logic
incorporating the equality relation, Machine Intelligence 4, ed.
B. Meltzer and D. Michie, Edinburgh Univ. Press, Edinburgh, 1969,
pp. 103133.
[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 C25(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
C25(8):823835, 1976.
[Sickel 1977a] S. Sickel, Formal grammars as models of logic
derivations, Proc. 5th IJCAI, MIT, Cambridge, MA, 1977, pp.
544551.
[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 CSM7,
Univ. of Essex, 1975.
[Siekmann 1976a] J. Siekmann, Unification of commutative terms,
Memo SEKI76IV, 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, Tunification, 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 CSM478, Univ. of Essex, 1978.
[Siekmann 1980] J. Siekmann, G. Wrightson, Paramodulated
connection graphs, Acta Informatica 13(1980):6786.
[Siekmann 1981a] J. Siekmann, P. Szabo, Universal unification
and regular equational ACFM theories, Memo SEKI81III, Institut
fur Informatik I, Universitat Karlsruhe, W. Germany, 1981; also
Proc. 7th IJCAI, Univ. of British Columbia, Vancouver, Canada,
August 1981, pp. 532538.
[Siekmann 1981b] J. Siekmann, P. Szabo, Universal unification
and a classification of equational theories, Interner Bericht
7/82, Memo SEKI81II, Institut fur Informatik I, Universitat
Karlsruhe, W. Germany, 1981; also Proc. 6th Conf. on Automated
Deduction, ed. D. Loveland, LNCS 138, SpringerVerlag, Berlin,
1982, pp. 369389.
[Siekmann 1981c] J. Siekmann, P. Szabo, A Noetherian rewrite
system for idempotent semigroups, Proc. GWAI81,
InformatikFachberichte 47, ed. Siekmann, SpringerVerlag, Berlin,
1981, pp. 235245.
[Siekmann 1981d] J. Siekmann, G. Smolka, Selection heuristics,
deletion strategies and Nlevel terminator configurations for the
connection graph, Proc. GWAI81, InformatikFachberichte 47, ed.
Siekmann, SpringerVerlag, Berlin, 1981, pp. 199200.
[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. GWAI82, InformatikFachberichte 58, ed. Wahlster,
SpringerVerlag, Berlin, 1982, pp. 102141.
[Siekmann 1982c] J. Siekmann, P. Szabo, A Noetherian and
confluent rewrite system for idempotent semigroups, Semigroup
Forum 25, pp. 83100, 1982.
[Siekmann 1983a] J. Siekmann, G. Wrightson, eds., Automation of
Reasoning  Classical Papers on Computational Logic, Vol. I,
19571966, SpringerVerlag, Berlin, 1983.
[Siekmann 1983b] J. Siekmann, G. Wrightson, eds., Automation of
Reasoning  Classical Papers on Computational Logic, Vol. II,
19671970, SpringerVerlag, Berlin, 1983.
[Siekmann 1984] J.H. Siekmann, Universal unification, Proc. 7th
Intl. Conf. on Automated Deduction (CADE7, Napa, CA, May 1984),
ed. R.E. Shostak, LNCS 170, SpringerVerlag, NY, 1984, pp. 142.
[Siekmann 1986a] J.H. Siekmann, ed., Proc. 8th Intl. Conf. on
Automated Deduction (CADE8, Oxford, England, July 27August 1,
1986), LNCS 230, SpringerVerlag, Berlin, 1986.
*[Siekmann 1986b] J.H. Siekmann, Unification theory, Proc. 8th
Intl. Conf. on Automated Deduction (CADE8, Oxford, England, July
27August 1, 1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag,
Berlin, 1986, p. vixxxv; also Proc. 7th European Conf. on
Artificial Intelligence (ECAI86, Brighton, UK, 2025 July 1986),
In: Advances in Artificial Intelligence  II, ed. B. du Boulay,
D. Hogg, and L. Steels, NorthHolland, Amsterdam, 1987, pp.
365400; also available from Automated Reasoning Project,
Australian National Univ., Canberra, ACT.2601, Australia, 1988;
also J. of Symbolic Computation 7(3,4):207274, 1989 (special
issue on unification, part one).
*[Siekmann 1986c] J. Siekmann, P. Szabo, The undecidability of
the DAunification problem, SEKI Report SR8619, 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. 369424.
[Siklossy 1971] L. Siklossy, V. Marinor, Heuristic search vs
exhaustive search, Proc. 2nd IJCAI, Imperial College, London,
1971, pp. 601607.
[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. 383387.
[Silbert 1969] E.E. Silbert, A machineoriented 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):110114.
[Silver 1986] B. Silver, MetaLevel Inference: Representing and
Learning Control Information in Artificial Intelligence, Studies
in Computer Science and Artificial Intelligence, NorthHolland,
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
secondorder instantiation, Proc. 7th Intl. Conf. on Automated
Deduction (CADE7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS
170, SpringerVerlag, NY, 1984, pp. 200223.
*[Simon 1988] D. Simon, Checking natural language proofs, Proc.
9th Intl. Conf. on Automated Deduction (CADE9, Argonne, Illinois,
2326 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310,
SpringerVerlag, Berlin, 1988, pp. 141150.
*[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. 11351147.
[Slagle 1965a] J.R. Slagle, A multipurpose theorem proving
heuristic program that learns, Proc. IFIP Congr. 1965, 2, pp.
323328.
[Slagle 1965b] J.R. Slagle, A proposed preference strategy using
sufficiency resolution for answering questions, UCRL14361,
Lawrence Radiation Lab., Livermore, CA, 1965.
[Slagle 1965c] J.R. Slagle, Experiments with a deductive
questionanswering program, CACM 8(1965):792798.
[Slagle 1967] J.R. Slagle, Automatic theorem proving with
renamable and semantic resolution, JACM 14(4):687697, October
1967; also Automation Of Reasoning  Classical Papers On
Computational Logic, Vol. II, 19671970, ed. J. Siekmann And G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 5565.
[Slagle 1968] J.R. Slagle, P. Bursky, Experiments with a
multipurpose theoremproving heuristic program, JACM 15(1):8599,
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. 281285.
[Slagle 1970a] J.R. Slagle, Interpolation theorem for resolution
in lower predicate calculus, JACM 17(3):535542, 1970.
[Slagle 1970b] J.R. Slagle, Heuristic search programs, in
Theoretical Approaches to Nonnumerical Problem Solving, ed. R.
Banerji and M. Mesavoric, SpringerVerlag, NY, 1970, pp. 246273.
[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):304310, 1970.
[Slagle 1971a] J. Slagle, Artificial Intelligence: The Heuristic
Programming Approach, McGrawHill, NY, 1971.
[Slagle 1971b] J.R. Slagle, D. Koniver, Finding resolution
proofs and using duplicate goals in and/or trees, Information Sci.
4(3):315342, 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):682688.
[Slagle 1971d] J.R. Slagle, Automatic theoremproving 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
builtin theories including equality, partial ordering and sets,
JACM 19(1):120135, January 1972.
[Slagle 1972b] J.R. Slagle, An approach for finding clinear
complete inference systems, JACM 19(July 1972):496516.
[Slagle 1974] J.R. Slagle, Automated theorem proving for
theories with simplifiers, commutativity and associativity, JACM
21(4):622642, October 1974.
[Slagle 1975] J.R. Slagle, L.M. Norton, Automatic
theoremproving for the theories of partial and total ordering,
Comput. J. 18(February 1975):4954.
[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 (CADE10, Kaiserslautern, FRG, July 1990),
Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel,
SpringerVerlag, Berlin, 1990, pp. 2839.
*[Slaney 1991] J.K. Slaney, The Ackermann constant theorem: A
computerassisted investigation, J. Automated Reasoning
7(4):453474, December 1991.
*[Slaney 1993] J. Slaney, SCOTT: A modelguided theorem prover,
Proc. 13th IJCAI (Chambery, France, 28 August3 September 1993),
Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 109115.
[Smith 1975] R.L. Smith, W.H. Graves, L.H. Blaine, V.G. Marinov,
ComputerAssisted Axiomatic Mathematics: Informal Rigor, In
Computers in Education, ed. O. Lecarme and R. Lewis,
NorthHolland/American Elsevier, 1975, pp. 803809.
[Smith 1981] D.R. Smith, A design for an automatic programming
system, Proc. 7th IJCAI, Vancouver, B.C., Canada, 1981, pp.
10241027.
[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):171215, 1985.
[Smith 1986a] D.E. Smith, M.R. Genesereth, M.L. Ginsberg,
Controlling recursive inference, Artificial Intelligence
30(1986):343389.
[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 nHProlog
implementation, Proc. 9th Intl. Conf. on Automated Deduction
(CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk and R.
Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp. 766767.
[Smith 1988b] B. Smith, Reference manual for the environmental
theorem prover, an incarnation of AURA, Tech. report ANL882,
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 unitrefutable clause sets, Proc. GWAI82, 6th
German Workshop on Artificial Intelligence, Bad Honnef (September
1982), InformatikFachberichte 58, ed. Wahlster, SpringerVerlag,
Berlin, 1982, pp. 191204.
[Smolka 1982b] G. Smolka, Completeness of the connection graph
proof procedure for unitrefutable clause sets, Proc. GWAI82,
InformatikFachberichte 58, ed. Wahlster, SpringerVerlag, Berlin,
1982, pp. 191204.
[Smolka 1982c] G. Smolka, Completeness and confluence properties
of Kowalski's clause graph calculus, Interner Bericht 31/82, Memo
SEKI82III, Institut fur Informatik I, Universitat Karlsruhe, W.
Germany, December 1982.
*[Smolka 1986] G. Smolka, Ordersorted Horn logic: semantics and
deduction, SEKI Report SR8617, Universitat Kaiserslautern, W.
Germany, September 1986.
*[Smolka 1987] G. Smolka, W. Nutt, J. Meseguer, J.A. Goguen,
Ordersorted equational computation, SEKI Report SR8714,
Universitat Kaiserslautern, 1987; In: Resolution of Equations in
Algebraic Structures: Vol 2, Rewriting Techniques, ed. H.
AitKaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp.
297367.
[Smullyan 1963] R.M. Smullyan, A unifying principal in
quantification theory, Proc. Nat. Acad. Sci. 49(1963):828832.
[Smullyan 1968] R.M. Smullyan, FirstOrder Logic,
SpringerVerlag, 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
(CADE11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur,
Lecture Notes in Artificial Intelligence 607, SpringerVerlag,
Berlin, 1992, p. 208.
[Snyder 1988] W. Snyder, J.H. Gallier, Higherorder 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):101140, 1989; reprinted in
[Kirchner 1990c], pp. 565604.
*[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, 35 April 1989), ed. N. Dershowitz, SpringerVerlag, NY,
1989, pp. 419433.
[Snyder 1989b] W. Snyder, J.H. Gallier, Complete sets of
transformations for general Eunification, Theoretical Computer
Science 67(1989):203260.
*[Snyder 1990] W. Snyder, Higher order Eunification, Proc. 10th
Intl. Conf. on Automated Deduction (CADE10, Kaiserslautern, FRG,
July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E.
Stickel, SpringerVerlag, Berlin, 1990, pp. 573587.
*[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 SR8704, Universitat Kaiserslautern, June
1987.
*[Socher 1987b] R. Socher, An optimized transformation into
conjunctive (or disjunctive) normal forms, SEKI Report SR8713,
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 (CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk
and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
573581.
*[Socher 1991] R. Socher, Optimizing the clausal normal form
transformation, J. Automated Reasoning 7(3):325336, September
1991.
*[SocherAmbrosius 1988] R. SocherAmbrosius, Using theory
resolution to simplify interpreted formulae, SEKI Report SR8816,
Universitat Kaiserslautern, 1988; also Proc. Kunstliche
Intelligenz (GWAI88, 12. Jahrestagung, Eringerfeld, 1923
September 1988), InformatikFachberichte 181, ed. W. Hoeppener,
SpringerVerlag, Berlin, pp. 179185.
[SocherAmbrosius 1989a] R. SocherAmbrosius, Reducing the
derivation of redundant clauses in reasoning systems, SEKI Report
SR8904, Fachbereich Informatik, Universitat Kaiserslautern,
Kaiserslautern, 1989; also Proc. 11th IJCAI (Detroit, Michigan,
USA, 2025 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp.
401406.
[SocherAmbrosius 1989b] R. SocherAmbrosius, Another technique
for proving completeness of resolution, SEKI Report SR8905,
Fachbereich Informatik, Universitat Kaiserslautern,
Kaiserslautern, 1989.
*[SocherAmbrosius 1989c] R. SocherAmbrosius, Detecting
redundancy caused by congruent links in clause graphs, SEKI Report
SR8806, Universitat Kaiserslautern; also Proc. 13 German
Workshop on Artificial Intelligence (GWAI89, Eringerfeld, 1822
September 1989), ed. D. Metzing, SpringerVerlag, Berlin, 1989,
pp. 7482.
[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, CSR14083, 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
CSR14683, 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, 2527 May 1987), ed. P. Lescanne, LNCS 256,
SpringerVerlag, Berlin, 1987, pp. 6273.
[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. 567584.
*[Sperschneider 1991] V. Sperschneider, G. Antoniou, Logic: A
foundation for Computer Science, AddisonWesley Publishing
Company, Wokingham, England, 1991.
[Sridhar 1986] S. Sridhar, An implementation of OBJ2: an
objectoriented language for abstract program specification, Proc.
6th Conf. on Foundations of Software Technology and Theoretical
Computer Science, LNCS 241, ed. K.V. Nori, SpringerVerlag, 1986,
pp. 8195.
[Srinivasan 1976] C.V. Srinivasan, Theorem proving in the meta
description system, ARPA SOSAPTR20, 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. 319336.
*[Stabler 1993] E.P. Stabler, Jr, Parsing as nonHorn deduction,
Artificial Intelligence 63(12):225264, October 1993.
*[Stachniak 1990] M. Stachniak, Resolution proof systems with
weak transformation rules, Proc. ISSAC '90 (Tokyo, Japan, 2024
August 1990), ACM, NY, NY, 1990, p. 3843.
[Stanfield 1986] C. Stanfield, D. Waltz, Toward memorybased
reasoning, Thinking Machines Report, 1986.
[Staples 1980a] J. Staples, A graphlike lambda calculus for
which leftmostoutermost 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. 440455.
[Staples 1980b] J. Staples, Computation on graphlike
expresions, Theor. Comp. Sci 10(1980):171185.
[Staples 1981] J. Staples, Efficient lazy evaluation of lambda
expressions: a stackbased 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. 277285.
[Staples 1988] J. Staples, P.J. Robinson, Efficient unification
of quantified terms, J. Logic Programming 5(1988):133149.
*[Staples 1990] J. Staples, P.J. Robinson, Structure sharing for
quantified terms: Fundamentals, J. of Automated Reasoning
6(2):115145, June 1990.
[Statman 1978] R. Statman, Bounds for proofsearch and speedup
in the predicate calculus, Annals of Mathematical Logic
15:225287, 1978.
[Statman 1980] R. Statman, Worst case exponential lower bounds
for input resolution with paramodulation, SIAM J. Computing
9(1):104110, February 1980.
*[Steinbach 1988a] J. Steinbach, Comparison of simplification
orderings, SEKI Report SR8802, Artificial Intelligence
Laboratories, Dept. of Computer Science, Universitat
Kaiserslautern, W. Germany, February 1988.
*[Steinbach 1988b] J. Steinbach, Term ordering with status, SEKI
Report SR8812, 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, 35
April 1989), ed. N. Dershowitz, SpringerVerlag, NY, 1989, pp.
434448.
[Steinbach 1989b] J. Steinbach, Proving termination of
associativecommutative term rewriting systems using the
KnuthBendix ordering, SEKI Report SR8913, Artificial
Intelligence Laboratories, Dept. of Computer Science, Universitat
Kaiserslautern, W. Germany, 1989.
[Steinbach 1989c] J. Steinbach, Path and decomposition orderings
for proving ACtermination, 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 (CADE10,
Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial
Intelligence 449, ed. M.E. Stickel, SpringerVerlag, Berlin, 1990,
pp. 411425.
[Stenlund 1972] S. Stenlund, Combinators, lambdaterms, 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, 1820
July 1978), ed. C. Sleeman, Leeds Univ. Press, 1978, pp. 340344.
[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,
SpringerVerlag, 1982, pp. 109116.
[Sterling 1982b] L. Sterling, A. Bundy, Metalevel 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, SpringerVerlag,
Berlin, 1982, pp. 144150.
[Sterling 1983] L. Sterling, IMPRESS  Metalevel concepts in
theorem proving, Working Paper 119, Dept. of Artificial
Intelligence, Univ. of Edinburgh, 1983.
[Sterling 1984] L. Sterling, Implementing problemsolving
strategies using the metalevel. 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):177180,
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 ECAI88, ed. Y. Kodratoff, pp. 565570, 1988.
[Stevens 1987b] R.L. Stevens, Some experiments in nonassociative
ring theory with an automated theorem prover, J. of Automated
Reasoning 3(2):211221, June 1987.
*[Stevens 1988a] R. L. Stevens, Challenge problems for
nonassociative rings for theorem provers, Proc. 9th Intl. Conf. on
Automated Deduction (CADE9, Argonne, Illinois, 2326 May 1988),
ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag, Berlin,
1988, pp. 730734.
*[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, 15 August 1988, pp. 565570.
[Stickel 1974] M.E. Stickel, The programmable strategy theorem
prover: an implementation of the linear MESON procedure, Tech.
Report, CarnegieMellon Univ. Comput. Sci. Dept., June 1974.
[Stickel 1975] M.E. Stickel, A complete unification algorithm
for associativecommutative functions, Proc. 4th IJCAI, Tbilisi,
Georgia, USSR, 1975, pp. 7176; also JACM 28(3):423434, 1981.
[Stickel 1976] M.E. Stickel, Unification algorithms for
artificial intelligence languages, PhD thesis, CarnegieMellon
Univ., 1976.
[Stickel 1977] M.E. Stickel, Mechanical theorem proving and
artificial intelligence languages, PhD thesis, CarnegieMellon
Univ., Pittsburgh, 1977.
[Stickel 1981] M.E. Stickel, A complete unification algorithm
for associativecommutative functions, JACM 28(3):423434, July
1981.
[Stickel 1982] M.E. Stickel, A nonclausal connectiongraph
resolution theoremproving program, Tech. Note 268, SRI
International, Artificial Intelligence Center, Menlo Park, CA,
1982; also Proc. AAAI82, Natl Conf. on Artificial Intelligence
(Pittsburgh, PA, CarnegieMellon Univ., August 1982), Morgan
Kaufmann Publishers, Los Altos, CA, 1982, pp. 229233.
[Stickel 1983a] M.E. Stickel, A note on leftmostinnermost term
reduction, ACM SIGSAM Bulletin 17(3&4), issue no. 67 & 68,
August and November 1983, pp. 1920.
[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. 391397.
[Stickel 1984a] M.E. Stickel, A case study of theorem proving by
the KnuthBendix method discovering that (x cubed = x) implies
ring commutativity, Proc. 7th Intl. Conf. on Automated Deduction
(CADE7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170,
SpringerVerlag, NY, 1984, pp. 248258.
[Stickel 1984b] M.E. Stickel, A Prolog technology theorem
prover, New Generation Computing 2(4):371383, 1984; also 1984
Intl. Symp. on Logic Programming, Atlantic City, New Jersey, 69
February 1984, pp. 211217.
[Stickel 1985a] M.E. Stickel, Automated deduction by theory
resolution, J. of Automated Reasoning 1(4):333355, D. Reidel
Publ. Co., Dordrecht, Holland, 1985; also Proc. 9th IJCAI, Vol. 2,
Los Angeles, CA, 1823 August 1985, pp. 11811186.
*[Stickel 1985b] M.E. Stickel, W.M. Tyson, An analysis of
consecutively bounded depthfirst search with applications in
automated deduction, Proc. 9th IJCAI, Los Angeles, CA, 1985, pp.
10731075.
[Stickel 1986a] M.E. Stickel, Schubert's steamroller problem:
formulations and solutions, J. of Automated Reasoning 2(1):89101,
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 (CADE8, Oxford, England, July
27August 1, 1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag,
Berlin, 1986, pp. 573587.
[Stickel 1986c] M.E. Stickel, The KLAUS Automated Theorem
Proving System, Proc. 8th Intl. Conf. on Automated Deduction
(CADE8, Oxford, England, July 27August 1, 1986), ed. J.H.
Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp. 703704.
*[Stickel 1986d] M.E. Stickel, An introduction to automated
deduction, In Fundamentals of Artificial Intelligence, ed. W.
Bibel and Ph. Jorrand, LNCS 232, SpringerVerlag, Berlin, 1986,
pp. 75132.
[Stickel 1987] M.E. Stickel, A comparison of the
variableabstraction and constantabstraction methods for
associativecommutative unification, J. of Automated Reasoning
3(3):285289, September 1987.
*[Stickel 1988a] M.E. Stickel, The KLAUS automated deduction
system, Proc. 9th Intl. Conf. on Automated Deduction (CADE9,
Argonne, Illinois, 2326 May 1988), ed. E. Lusk and R. Overbeek,
LNCS 310, SpringerVerlag, Berlin, 1988, pp. 750751.
*[Stickel 1988b] M.E. Stickel, A Prolog Technology Theorem
Prover, Proc. 9th Intl. Conf. on Automated Deduction (CADE9,
Argonne, Illinois, 2326 May 1988), ed. E. Lusk and R. Overbeek,
LNCS 310, SpringerVerlag, Berlin, 1988, pp. 752753.
*[Stickel 1988c] M.E. Stickel, A Prolog Technology Theorem
Prover: Implementation by an extended Prolog compiler, J.
Automated Reasoning 4(4):353380, 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.
285316.
[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 pathindexing 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
(CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes in
Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, pp. 673674.
*[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 1012 April 1990), LNCS 429, ed. A Miola,
SpringerVerlag, 1990, pp. 154163.
[Stillman 1972] R.B. Stillman, Associative processing techniques
for theorem proving, RADCTR7256, Rome Air Dev. Center, NY,
April 1972.
[Stillman 1973] R.B. Stillman, The concept of weak substitution
in theorem proving, JACM 20(4):648667, October 1973.
*[Stokes 1990] T. Stokes, Grobner bases in exterior algebra, J.
of Automated Reasoning 6(3):233250, September 1990.
[Strandh 1987] R. Strandh, Optimizing equational programs, Proc.
2nd Intl. Conf. on Rewriting Techniques and Applications
(Bordeaux, France, 2527 May 1987), ed. P. Lescanne, LNCS 256,
SpringerVerlag, Berlin, 1987, pp. 1324.
[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, 35 April 1989), ed. N. Dershowitz, SpringerVerlag, NY,
1989, pp. 449461.
*[Subrahmanian 1988a] V.S. Subrahmanian, Query processing in
quantitative logic programming, Proc. 9th Intl. Conf. on Automated
Deduction (CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk
and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
81100.
*[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 (CADE9, Argonne,
Illinois, 2326 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310,
SpringerVerlag, Berlin, 1988, pp. 746747.
[Suppes 1981] P. Suppes, Universitylevel computerassisted
instruction at Stanford: 19681981, 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
(CADE7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170,
SpringerVerlag, NY, 1984, pp. 303315.
[Suppes 1989] P. Suppes, S. Takahashi, An interactive calculus
theoremprover for continuity properties, J. Symbolic Comput.
7(6):573590, 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
(CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes in
Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, pp. 675676.
*[Sutcliffe 1992a] G. Sutcliffe, Linearinput subset analysis,
Proc. 11th Intl. Conf. on Automated Deduction (CADE11, Saratoga
Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in
Artificial Intelligence 607, SpringerVerlag, Berlin, 1992, pp.
268280.
*[Sutcliffe 1992b] G. Sutcliffe, The semantically guided linear
deduction system, Proc. 11th Intl. Conf. on Automated Deduction
(CADE11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur,
Lecture Notes in Artificial Intelligence 607, SpringerVerlag,
Berlin, 1992, pp. 677680.
[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 (CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes
in Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, pp. 470484.
[Suzuki 1975] N. Suzuki, Verifying programs by algebraic and
logical reduction, Proc. Intl. Conf. on Reliable Software (IEEE),
1975, pp. 473481.
[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. 280285.
[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 DAunification
problem, Proc. GWAI, SpringerVerlag, 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. COLOG88: Intl. Conf. on Computer
Logic, LNCS 417, SpringerVerlag, 1990, pp. 300312.
*[Tang 1989] T.G. Tang, Temporal logic CTL + PROLOG, J.
Automated Reasoning 5(1):4965, March 1989.
*[Tang 1991] T.G. Tang, Programming in temporalnonmonotonic
reasoning, J. Automated Reasoning 7(3):383401, 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):215225, 1975.
[Tarjan 1984] R.E. Tarjan, J. Van Leeuwen, Worstcase analysis
of set union algorithms, JACM 31(2):245281, 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., NorthHolland, 1968.
*[Tarver 1990] M. Tarver, An examination of the Prolog
technology theoremprover, Proc. 10th Intl. Conf. on Automated
Deduction (CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes
in Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, pp. 322335.
[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. 1724.
[Teitelbaum 1981] T. Teitelbaum, T.W. Reps, The Cornell program
synthesizer: a syntaxdirected programming environment, CACM
24(9): 563573, 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):8385, 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. 299300.
[Thistlewaite 1984] P.B. Thistlewaite, Automated theoremproving
in nonclassical 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 theoremproving techniques for relevant logics,
Logique et Analyse 28(1985):233256.
[Thistlewaite 1986] P.B. Thistlewaite, M.A. McRobbie, R.K.
Meyer, The KRIPKE Automated Theorem Proving System, Proc. 8th
Intl. Conf. on Automated Deduction (CADE8, Oxford, England, July
27August 1, 1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag,
Berlin, 1986, pp. 705706.
*[Thistlewaite 1988] P.B. Thistlewaite, M.A. McRobbie, R.K.
Meyer, Automated TheoremProving in NonClassical 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 nonclassical problems, J. Automated Reasoning
7(4):635637, December 1991.
[Thomas 1984] C. Thomas, RRLab  Rewrite rule labor, Memo
SEKI8401, 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
onesided distributivity, Proc. 1st Conf. Rewriting Techniques and
Applications (Dijon, France, 2022 May 1985), ed. J.P. Jouannaud,
LNCS 202, SpringerVerlag, Berlin, 1985. pp. 398406; also J. of
Symbolic Computation 3(1 and 2):183202, 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 S100 44 Stockholm, Sweden,
1985.
[Tiden 1986a] E. Tiden, Unification in combinations of
collapsefree theories with disjoint sets of function symbols,
Proc. 8th Intl. Conf. on Automated Deduction (CADE8, Oxford,
England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS 230,
SpringerVerlag, Berlin, 1986, pp. 431449.
[Tiden 1986b] E. Tiden, Firstorder 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):446456, 1967.
*[Tison 1989] S. Tison, Fair termination is decidable for ground
systems, Proc. 3rd Intl. Conf. Rewriting Techniques and
Applications (Chapel Hill, North Carolina, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 462476.
[Toledo 1975] S.A. Toledo, Tableau systems for first order
number theory and certain higher order theories. In Lecture Notes
in Mathematics 447, SpringerVerlag, NY, 1975.
*[Tour 1990] T.B. de la Tour, Minimizing the number of clauses
by renaming, Proc. 10th Intl. Conf. on Automated Deduction
(CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes in
Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, pp. 558572.
[Townley 1980] J.A. Townley, A pragmatic approach to
resolutionbased theorem proving, Computer and Information
Sciences 9(2):93116, 1980.
[Toyama 1983] Y. Toyama, On the commutativity of term rewriting
systems, Trans. IECE, Japan, J66D, 12, 1983, pp. 13701375.
[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, SpringerVerlag, Berlin, 1984, pp. 4461.
[Toyama 1986] Y. Toyama, How to prove equivalence of term
rewriting systems without induction, Proc. 8th Intl. Conf. on
Automated Deduction (CADE8, Oxford, England, July 27August 1,
1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986,
pp. 118127.
[Toyama 1987a] Y. Toyama, On the ChurchRosser property for the
direct sum of term rewriting systems, JACM 34(1):128143, January
1987.
[Toyama 1987b] Y. Toyama, Counterexamples to termination for the
direct sum of term rewriting systesm, Information Processing
Letters 25(1987):141143.
*[Toyama 1988a] Y. Toyama, Confluent term rewriting systems with
membership conditions, Proc. 1st Intl. Workshop on Conditional
Term Rewriting Systems (Orsay, France, 810 July 1987), ed. S.
Kaplan and J.P. Jouannaud, LNCS 308, SpringerVerlag, Berlin,
1988, pp. 228241.
[Toyama 1988b] Y. Toyama, Commutativity of term rewriting
systems, In Programming of Future Generation Computer II, ed. K.
Fuchi and L. Kott, NorthHolland, 1988, pp. 393407.
*[Toyama 1989] Y. Toyama, J.W. Klop, H.P. Barendregt,
Termination for the direct sum of leftlinear term rewriting
systems, Proc. 3rd Intl. Conf. Rewriting Techniques and
Applications (Chapel Hill, North Carolina, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 477491.
[Traugott 1986a] J. Traugott, Nested resolution, Proc. 8th Intl.
Conf. on Automated Deduction (CADE8, Oxford, England, July
27August 1, 1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag,
Berlin, 1986, pp. 394402.
[Traugott 1986b] J. Traugott, Deductive synthesis of sorting
programs, Proc. 8th Intl. Conf. on Automated Deduction (CADE8,
Oxford, England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS
230, SpringerVerlag, Berlin, 1986, pp. 641660.
[Travis 1964] L.G. Travis, Experiments with AI theorem utilizing
program, AFIPS Conf. Proc. 25, SJCL, Spartan Books, Baltimore,
Mo., 1964, pp. 339358.
[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):395431, 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. 115125.
[Tseitin 1983] G.S. Tseitin, On the complexity of derivation in
propositional calculus, in Automation Of Reasoning  Classical
Papers On Computational Logic, Vol. II, 19671970, ed. J. Siekmann
And G. Wrightson, SpringerVerlag, Berlin, 1983, pp. 466483; also
Structures in Constructive Mathematics and Mathematical Logic Part
II, ed. A.O. Siliosenko, 1968, pp. 115125.
*[Tuominen 1990] H. Tuominen, Dynamic logic as a uniform
framework for theorem proving in intensional logic, Proc. 10th
Intl. Conf. on Automated Deduction (CADE10, Kaiserslautern, FRG,
July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E.
Stickel, SpringerVerlag, Berlin, 1990, pp. 514527.
[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. 433460.
[Tyson 1979] M. Tyson, W.W. Bledsoe, Conflicting bindings and
generalized substitutions, Proc. 4th Workshop on Automated
Deduction (CADE4, Austin, Texas, 13 February 1979), ed. W.H.
Joyner, 1979, pp. 1418.
[Tyson 1981] W.M. Tyson, APRVR: A priorityordered agenda
theorem prover, PhD Dissertation, Univ. of Texas at Austin, August
1981; also Proc. AAAI National Conf., Pittsburgh, PA, August 1982,
pp. 225228.
[Tyson 1982] M. Tyson, Proof methods in an agendabased
naturaldeduction prover, Proc. AAAI82, Natl Conf. on Artificial
Intelligence, CarnegieMellon Univ., 1982, pp. 225228.
