ORA Canada

ORA Canada
Home
Contact us
What's new?
Products and services
Z/EVES
EVES
Ada'95
Reports and Collections
ORA Canada
Bibliography
Automated Deduction
Bibliography
    A-B
    C-E
    F-G
    H-J
    K-L
    M-N
    O-R
    S-T
    U-Z

ORA Canada Bibliography of Automated Deduction: Authors A to B

*[Aaby 1988] A.A. Aaby, K.T. Narayana, Propositional temporal interval logic is PSPACE complete, 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. 218-237.

[Aandreaa 1963] S. Aandreaa, P. Andrews, B. Dreben, False lemmas in Herbrand, Bull. of the American Math. Soc. 68(1963):699-706.

[Aandreaa 1964] S. Aandreaa, A deterministic proof procedure, Technical Report, Harvard Univ., May 1964.

[Abadi 1984] M. Abadi, et al., Generalization heuristics for theorems related to recursively defined functions, Proc. 4th Natl Conf. on Artificial Intelligence, Austin, 1984.

[Abadi 1985] M. Abadi, Z. Manna, Nonclausal temporal deduction, Report STAN-CS-85-1056, Dept. of Computer Science, Stanford Univ., Stanford, CA, 1985; also Logics of Programs, ed. R. Parikh, LNCS 193, Springer-Verlag, Berlin, 1985, pp. 1-15.

[Abadi 1986a] M. Abadi, Z. Manna, Modal theorem proving, STAN-CS-86-1101, Dept. of Computer Science, Stanford Univ., May 1986; 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. 172-189.

[Abadi 1986b] M. Abadi, Z. Manna, A timely resolution, STAN-CS-86-1106, Dept. of Computer Science, Stanford Univ., April 1986.

[Abadi 1987] M. Abadi, Temporal-logic theorem proving, STAN-CS-87-1151, Stanford Univ. Computer Science Dept., CA, March 1987.

[Abadi 1990] M. Abadi, Z. Manna, Nonclausal deduction in first-order temporal logic, JACM 37(2):279-317, April 1990.

[Abdali 1982] S.K. Abdali, D.R. Musser, A proof method based on sequents and unification, Unpublished manuscript, G.E. R and D Center, Schenectady, NY, 1982.

[Abdali 1984] S.K. Abdali, Generalization heuristics for theorems related to recursively defined functions, Proc. AAAI-84, Natl Conf. on Artificial Intelligence, Univ. of Texas at Austin, 6-10 August 1984, pp. 1-5.

*[Abdulrab 1989] H. Abdulrab, J.-P. Pecuchet, Solving systems of linear diophantine equations and word equations, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 530-532.

[Abrahams 1963] P.W. Abrahams, Machine verification of mathematical proof, Doctoral Dissertation in Math., MIT, May 1963.

[Abrahams 1964] P.W. Abrahams, W. Rode, A proposal for a proof-checker for certain axiomatic systems, SRI-MEMO-41, Stanford Research Institute, Stanford, 1964.

[Abrahams 1966] P.W. Abrahams, Application of LISP to checking mathematical proofs, The Programming Language LISP, ed. Berkeley and Bobrow, MIT Press, Cambridge, MA, 1966, pp. 137-160.

[Abrahams 1968] P.W. Abrahams, Machine verification of mathematical proofs, Maths Algorithms, Vol. 1 (1966), Vol. 2 (1967), Vol. 3 (1968).

[Adi 1989] M. Adi, C. Kirchner, AC-unification race: the system solving approach, implementation and benchmarks, Research Report 89-R-169, CRIN, Nancy, France, 1989.

*[Adi 1990] M. Adi, C. Kirchner, AC-unification race: The system solving approach and its implementation, 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. 174-183.

[Agnarsson 1984] S. Agnarsson, A. Kandri-Rody, D. Kapur, D. Narendran, B.D. Saunders, Complexity of testing whether a polynomial ideal is non-trivial, Proc. 1984 MACSYMA Users' Conf., Schenectady, NY, July 1984, pp. 452-458.

[Aiello 1975] L.M. Aiello, R.W. Weyhrauch, Checking proofs in the metamathematics of first order logic, Proc. 4th IJCAI, Tbilisi, Georgia, USSR, 1975, pp. 1-8.

[Aiello 1977a] L.M. Aiello, R.W. Weyhrauch, PASCAL in LCF: Semantics and examples of proof, Theoretical Computer Science 5(2):135-178, October 1977.

[Aiello 1977b] L.M. Aiello et al., PPC (Pisa proof checker): A tool for experiments in theory of proving and mathematical theory of computation, Fundamenta Informaticae 1, 1977.

[Aiello 1980] L.M. Aiello, R.W. Weyhrauch, Using meta-theoretic reasoning to do algebra, Proc. 5th Conf. on Automated Deduction (Les Arcs, France, 8-11 July 1980), ed. W. Bibel and R. Kowalski, LNCS 87, Springer-Verlag, Berlin, 1980, pp. 1-13.

*[Aiello 1988] L.M. Aiello, R.W. Weyhrauch, Checking proofs in the metamathematics of first order logic, In Meta-Level Architectures and Reflection, ed. P. Maes and D. Nardi, North-Holland, Amsterdam, 1988, pp. 1-18.

[Ait-Kaci 1985a] H. Ait-Kaci, Solving type equations by graph rewriting, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985, pp. 158-179.

[Ait-Kaci 1985b] H. Ait-Kaci, An algorithm for finding a minimal recursive path ordering, Theoretical Informatics 19(4): 359-382, 1985.

*[Ait-Kaci 1989] H. Ait-Kaci, M. Nivat, eds., Resolution of Equations in Algebraic Structures (Vol 1, Algebraic Techniques; Vol. 2: Rewriting Techniques), Academic Press, Inc., San Diego, 1989. (Proc. Colloquium on the Resolution of Equations in Algebraic Structures, CREAS, Lakeway, Texas, 4-7 May 1987.)

[Ait-Kaci 1990] H. Ait-Kaci, The WAM: a (real) tutorial, PRL Research Report Number 5, Digital Equipment Corporation, Paris Research Laboratory, Rueil-Malmaison, France, 1990.

*[Ait-Kaci 1991] H. Ait-Kaci, Warren's Abstract Machine: A Tutorial Reconstruction, The MIT Press, Cambridge, MA, 1991.

*[Alexander 1992] G.D. Alexander, D.A. Plaisted, Proving equality theorems with hyper-linking, 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. 706-710.

[Allen 1970] J. Allen, D. Luckham, An interactive theorem proving program, Machine Intelligence 5, ed. B. Meltzer and D. Michie, American Elsevier, NY, 1970, pp. 321-326; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 417-434.

*[Allen 1988] P.E. Allen, S. Bose, E.M. Clarke, S. Michaylov, PARTHENON: A parallel theorem prover for non-Horn clauses, 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. 764-765.

*[Allen 1990] S.F. Allen, R.L. Constable, D.J. Howe, W.E. Aitken, The semantics of reflected proof, Proc. 5th Annual IEEE Symp. on Logic Computer Science (Philadelphia, PA, 4-7 June 1990), IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 95-105.

*[Altucher 1990] J.A. Altucher, P. Panangaden, A mechanically assisted constructive proof in category theory, 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. 500-513.

[Amarel 1962] S. Amarel, An approach to problem-solving by computer, Final Report AFCRL-62-367, Part 2, Air Force Cambridge Res. Lab., Cambridge, MA, May 1962.

[Amarel 1967] S. Amarel, An approach to heuristic problem solving and theorem proving in propositional calculus, in Systems and Computer Science, ed. J.F. Hart and S. Takasu, Univ. of Toronto, 1967.

[Amarel 1968] S. Amarel, On representations of problems of reasoning about actions, Machine Intelligence 3, ed. B. Meltzer and D. Michie, American Elsevier, NY, 1968, pp. 131-171.

[Amble 1975] T. Amble, A connection graph theorem prover, Institut for Databehandling, Universitetet i Trondheim, 1975.

[Ammon 1985] K. Ammon, The automatic discovery of concepts by induction and feedback: towards a theory of intelligence, Proc. Osterreichische Artificial Intelligence-Tagvung, Wien (24-27 September 1985), Informatik-Fachberichte 106, Springer-Verlag, Berlin, 1985, pp. 81-89.

*[Ammon 1988] K. Ammon, Discovering a proof for the fixed point theorem: a case study, Proc. 8th ECAI, Institut fur Informatik der Technischen Universitat Munchen, 1-5 August 1988, pp. 613-618.

*[Ammon 1992a] K. Ammon, Automatic proofs in mathematical logic and 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. 4-19.

*[Ammon 1992b] K. Ammon, The SHUNYATA 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. 681-685.

[Anantharaman 1989a] S. Anantharaman, J. Mzali, Unfailing completion modulo a set of equations, Research report 470, LRI-Orsay, France, 1989.

*[Anantharaman 1989b] S. Anantharaman, J. Hsiang, J. Mzali, SbReve2: A term rewriting laboratory with (AC-)unfailing completion, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 533-537.

*[Anantharaman 1990] S. Anantharaman, J. Hsiang, Automated proofs of the Moufang identities in alternative rings, J. of Automated Reasoning 6(1):79-109, March 1990.

*[Anantharaman 1990] S. Anantharaman, N. Andrianarivelo, Heuristical criteria in refutational theorem proving, 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. 184-193.

[Anderson 1962] J.M. Anderson, H.W. Johnstone, Natural Deduction, Wadsworth Publ. Co., Belmont, CA, 1962.

[Anderson 1970a] R. Anderson, Some theoretical aspects of automatic theorem proving, PhD thesis, Univ. of Texas at Austin, Texas, 1970.

[Anderson 1970b] R. Anderson, Completeness results for E-resolution, Proc. AFIPS'70, Spring Joint Computer Conf. Vol. 36, AFIPS Press, Montvale, NJ, 1970, pp. 653-656; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 317-320.

[Anderson 1970c] R. Anderson, W. Bledsoe, A linear format for resolution with merging and a new technique for establishing completeness, JACM 17(July 1970):525-534; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 321-330.

[Anderson 1970d] D.B. Anderson, An investigation of some clause indexing schemes, MIP-R-80, Edinburgh Univ., Technical Report, 1970.

[Anderson 1971] R. Anderson, Completeness of the locking restriction for paramodulation, Dept. of Comput. Sci., Univ. of Houston, Texas, 1971.

[Anderson 1972] D.B. Anderson, P.J. Hayes, An arraignment of theorem proving or the logicians folly, Memo. 54, Dept. of Computational Logic, Univ. of Edinburgh, 1972.

[Anderson 1979] R. Anderson, A linear format resolution and a new technique for establishing completeness, JACM 17(1979):525-534.

[Anderson 1981] J.R. Anderson, Turning of search of the problem space for geometry proofs, Proc. 7th IJCAI, 1981.

[Andrews 1965] P.B. Andrews, A transfinite type theory with type variables, North-Holland, Amsterdam, 1965.

[Andrews 1968a] P.B. Andrews, Resolution with merging, JACM 15(3):367-381, 1968; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 85-101.

[Andrews 1968b] P.B. Andrews, On simplifying the matrix of a WFF, J. Symbolic Logic 33(2):180-192, 1968; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 102-116.

[Andrews 1971] P.B. Andrews, Resolution in type theory, J. Symbolic Logic 36(3):414-432, 1971; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 487-507.

[Andrews 1972] P.B. Andrews, General models and extensionality, J. Symbolic Logic 37(2):395-397, 1972.

[Andrews 1974] P.B. Andrews, Provability in elementary type theory, Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik 20(1974):441-418.

[Andrews 1976] P.B Andrews, Refutations by matings, IEEE Trans. on Computers C-25(8):801-808, August 1976.

[Andrews 1977] P.B. Andrews, E.L. Cohen, Theorem proving in type theory, Proc. 5th IJCAI, MIT, Cambridge, MA, 1977, pp. 566.

[Andrews 1979] P.B. Andrews, General Matings, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979, pp. 19-25.

[Andrews 1980] P.B. Andrews, Transforming matings into natural deduction proofs, Proc. 5th Conf. on Automated Deduction (Les Arcs, France, 8-11 July 1980), ed. W. Bibel and R. Kowalski, LNCS 87, Springer-Verlag, Berlin, 1980, pp. 281-292.

[Andrews 1981] P.B. Andrews, Theorem proving via general matings, JACM 28(2):193-214, April 1981.

[Andrews 1983] P.B. Andrews, D.A. Miller, E.L. Cohen, F. Pfenning, Automating higher-order logic, Dept. of Math., Univ. Carnegie-Mellon, January 1983; also In: Automated Theorem Proving: After 25 Years, ed. W.W. Bledsoe, and D. Loveland, Contemporary Mathematics Series 19, American Math. Society, Providence, RI, 1984, pp. 169-192.

[Andrews 1986a] P.B. Andrews, Connections and higher-order 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. 1-4.

[Andrews 1986b] P.B. Andrews, F. Pfenning, S. Issar, C.P. Klapper, The TPS 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. 663-664.

[Andrews 1986c] P.B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Academic Press, NY, 1986.

[Andrews 1987] P.B. Andrews, Typed lambda-calculus and automated mathematics, Mathematical Logic and Theoretical Computer Science, ed. E.G.K. Lopez-Escobar, D.W. Kueker, and C.H. Smith, Lecture Notes in Pure and Applied Mathematics 106, Marcel Dekker, 1987, 1-14.

*[Andrews 1988] P.B. Andrews, S. Issar, D. Nesmith, F. Pfenning, The TPS Theorem Proving 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. 760-761.

*[Andrews 1989] P.B. Andrews, On connections and higher-order logic, J. Automated Reasoning 5(3):257-291, September 1989.

*[Andrews 1990] P.B. Andrews, S. Issar, D. Nesmith, F. Pfenning, The TPS Theorem Proving System (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. 641-642.

*[Andrews 1991] P.B. Andrews, More on the problem of finding a mapping between clause representation and natural-deduction representation, J. of Automated Reasoning 7(2):285-286, June 1991.

[Andreka 1991] H. Andreka, I. Nemeti, Sain, I., On the strength of temporal proofs, Theor. Comput. Sci. 80(2):125-151, March 1991.

[Antoniou 1983] G. Antoniou, H.J. Ohlbach, TERMINATOR, Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, pp. 916-919.

[Anufriev 1966] F.V. Anufriev, V.V. Fedjurko, A.A. Leticevskii, Z.M. Asel'derov, J.J. Diduh, On a certain algorithm for search of proofs of theorems in the theory of groups, Kibernetika (Kiev), No. 1, pp. 23-29, 1966.

*[Aponte 1984] M.V. Aponte, J.A. Fernandez, P. Roussel, Editing first-order proofs: Programmed rules vs. derived rules, Proc. 1984 Intl. Symp. on Logic Programming, Atlantic City, New Jersey, 6-9 February 1984, pp. 92-98.

[Applebaum 1985] C.H. Applebaum, et al, Logic machine architecture database support system - Layer 1 user's manual, The Mitre Corporation (and Argonne National Lab.), August 1985.

[Arnon 1984] D.S. Arnon, T.W. Sederberg, Implicit equation for a parametric surface by Grobner bases, Proc. 1984 MACSYMA User's Conf., ed. V.E. Golden, General Electric, Schenectady, New York, pp. 431-436.

*[Arnon 1986] D.S. Arnon, Geometric reasoning with logic and algebra, Proc. Workshop on Geometric Reasoning, Oxford Univ., June 30 - July 3, 1986, In: Artificial Intelligence 37(1-3):37-60, December 1988.

[Arnon 1988] D. Arnon; M. Mignotte, On mechanical quantifier elimination for elementary algebra and geometry, J. Symb. Com. 5(1988):237-259.

[Aronson 1980] A.R. Aronson, B.E. Jacabs, J. Minker, A note on fuzzy deduction, JACM 27(4):599-607, October 1980.

*[Arora 1992] S. Arora, S. Safra, Probabilistic checking of proofs, Proc. 33rd Annual Symp. on Foundations of Computer Science (Pittsburgh, PA, October 24-27, 1992), IEEE Computer Society Press, Los Alamitos, CA, 1992, pp. 2-13.

*[Arora 1992] S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and hardness of approximation problems, Proc. 33rd Annual Symp. on Foundations of Computer Science (Pittsburgh, PA, October 24-27, 1992), IEEE Computer Society Press, Los Alamitos, CA, 1992, pp. 14-23.

[Ashcroft 1976] E.A. Ashcroft, W.W. Wadge, Lucid - A formal system for writing and proving programs, SIAM J. on Computing 5(3):336-354, September 1976.

*[Aspetsberger 1985] K. Aspetsberger, Substitution expression: extracting solutions of non-Horn clause proofs, Proc. European Conf. on Computer Algebra (EUROCAL '85, Linz, Austria, 1-3 April 1985), Vol. 2: Research Contributions, ed. B.F. Caviness, LNCS 204, Springer-Verlag, Berlin, pp. 78-86.

[Aspvall 1979] B.Aspvall, M.R. Plass, R.E. Tajan, A linear-time algorithm for testing the truth of certain quantified boolean formulas, Information Processing Letters 8(1979):121-123.

*[Astesiano 1989] E. Astesiano, M. Wirsing, Bisimulation in algebraic specifications, In: Resolution of Equations in Algebraic Structures: Vol 1, Algebraic Techniques, ed. H. Ait-Kaci and M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 1-31.

*[Astrachan 1992] O.W. Astrachan, M.E. Stickel, Caching and lemmaizing in model elimination theorem provers, 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. 224-238.

[Aubin 1975] R. Aubin, Some generalization heuristics in proofs by induction, In: Actes du Colloque Construction: Amelioration et Verification de Programmes, ed. G. Huet and G. Kahn, 1975; also Proc. IRIA Colloquium on Proving and Improving Programs, Arc et Senans, France, July 1985, pp. 197-208.

[Aubin 1976] R. Aubin, Mechanizing structural induction, PhD thesis, Univ. of Edinburgh, Edinburgh, 1976.

[Aubin 1979a] R. Aubin, Mechanizing structural induction I: Formal system, Theoretical Computer Science 9(1979):329-345.

[Aubin 1979b] R. Aubin, Mechanizing structural induction II: Strategies, Theor. Comput. Sci. 9(2):347-362, October 1979.

[Auffray 1988] Y. Auffray, P. Enjalbert, Modal theorem proving using equational methods, Tech. Report 88-11, Laboratoire d'Informatique, Universite de Caen, 1988.

*[Auffray 1989] Y. Auffray, P. Enjalbert, Modal theorem proving: an equational viewpoint, Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 441-445.

*[Auffray 1990] Y. Auffray, P. Enjalbert, J.-J. Hebrard, Strategies for modal resolution: Results and problems, J. of Automated Reasoning 6(1):1-38, March 1990.

*[Augustsson 1985] L. Augustsson, Compiling pattern matching, Proc. Functional Programming Languages and Computer Architecture (Nancy, France, 16-19 September 1985), ed. J.-P. Jouannaud, LNCS 201, Springer-Verlag, Berlin, pp. 368-381.

[Avenhaus 1984] J. Avenhaus, On the termination of the Knuth-Bendix completion algorithm, Int. Report 120/84, Universitat Kaiserslautern, Kaiserslautern, W. Germany, 1984.

[Avenhaus 1984b] J. Avenhaus, On the descriptive power of term rewriting systems, J. of Symbolic Computation 2(2):109-122, June 1986.

[Avenhaus 1986] J. Avenhaus, B. Benninghofen, R. Gobel, K. Madlener, TRSPEC: A term rewriting based system for algebraic specifications, 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. 665-667.

*[Avenhaus 1988] J. Avenhaus, R. Gobel, B. Gramlich, K. Madlener, J. Steinbach, TRSPEC: A term rewriting based system for algebraic specifications, 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. 245-248.

*[Avenhaus 1989a] J. Avenhaus, J. Denzinger, J. Muller, THEOPOGLES - An efficient theorem prover based on rewrite-techniques, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 538-541.

*[Avenhaus 1989b] J. Avenhaus, K. Madlener, J. Steinbach, COMTES - An experimental environment for the completion of 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. 542-546.

*[Avenhaus 1990] J. Avenhaus, K. Madlener, Term rewriting and equational reasoning, In Formal Techniques in Artificial Intelligence: A Sourcebook, ed. R.B. Banerji, Elsevier Science Publishers, Amsterdam, 1990, pp. 1-43.

[Avron 1987a] Arnon Avron, Simple consequence relations, Tech. Report ECS-LFCS-87-30, Laboratory for the Foundations of Computer Science, Univ. of Edinburgh, 1987.

[Avron 1987b] Arnon Avron, I. Mason, Case studies in the Edinburgh logical framework, Laboratory for the Foundations of Computer Science, Univ. of Edinburgh, 1987.

[Avron 1987c] Arnon Avron, F.A. Honsell, I. Mason, Using typed lambda calculus to implement formal systems on a machine, Tech. Report ECS-LFCS-87-31, Laboratory for the Foundations of Computer Science, Univ. of Edinburgh, 1987.

*[Avron 1989] A. Avron, F. Honsell, I.A. Mason, An overview of the Edinburgh logical framework, In Current Trends in Hardware Verification and Automated Theorem Proving, ed. G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, NY, 1989, pp. 323-340.

*[Azzoune 1988] H. Azzoune, Type inference in Prolog, 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. 258-277.

[Baader 1986] F. Baader, The theory of idempotent semigroups is of unification type zero, J. Automated Reasoning 2(3):283-286, September 1986.

*[Baader 1989a] F. Baader, Characterizations of unification type zero, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 2-14.

[Baader 1989b] F. Baader, Unification in commutative theories, Special Issue on Unification, J. Symbolic Computation, ed. C. Kirchner, 1989.

*[Baader 1990] F. Baader, Rewrite systems for varieties of semigroups, 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. 396-410.

*[Baader 1992] R. Baader, K.U. Schulz, Unification in the union of disjoint equational theories: combining decision procedures, 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. 50-65.

[Baader 1993] R. Baader, K.U. Schulz, Combination techniques and decision problems for disunification, Research report CIS-Rep-93-65, Center for Language and Information Processing (CIS), Munich, Germany, January 1993.

*[Baaz 1987] M. Baaz, A. Leitsch, Strong splitting rules in automated theorem proving, 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. 424-425.

*[Baaz 1990] M. Baaz, A. Leitsh, A strong problem reduction method based on function introduction, Proc. ISSAC '90 (Tokyo, Japan, 20-24 August 1990), ACM, NY, NY, 1990, p. 30-37.

[Bachmair 1980] L. Bachmair, B. Buchberger, A simplified proof of the characterization theorem for Grobner bases, ACM SIGSAM Bull 14(4):29-34, 1980.

[Bachmair 1982a] L. Bachmair, Implementation of the Nelson-Oppen method for combining decision procedures: Implementation guide, CAMP 82-17.0, Computer-Aided Mathematical Problem Solving at the Univ. of Linz, Austria, 1982.

[Bachmair 1982b] L. Bachmair, The Nelson-Oppen method of combining special theorem provers: Implementation and application to program verification, CAMP 82-18.0, Computer-Aided Mathematical Problem Solving at the Univ. of Linz, Austria, 1982.

[Bachmair 1984] L. Bachmair, D.A. Plaisted, Termination orderings for associative-commutative rewriting systems, Report UIUCDCS-R-84-1179, Dept. of Computer Science, Univ. of Illinois at Urbana-Champaign, December 1984.

[Bachmair 1985a] L. Bachmair, D.A. Plaisted, Associative path orderings, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985, pp. 241-254; also J. of Symbolic Computation 1(4):329-349, December 1985.

[Bachmair 1985b] L. Bachmair, N. Dershowitz, Critical pair criteria for the Knuth-Bendix completion method, Dept. of Computer Science, Univ. of Illinois, Urbana-Champaign, 1985.

[Bachmair 1985c] L. Bachmair, N. Dershowitz, Commutation, transformation, and termination, Inter. Report Univ. of Illinois, 1985; 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. 5-20.

[Bachmair 1986a] L. Bachmair, N. Dershowitz, and J. Hsiang, Orderings for equational proofs, Proc. IEEE Symp. on Logic in Computer Science, Cambridge, MA, 16-18 June 1986, pp. 346-357.

[Bachmair 1986b] L. Bachmair, N. Dershowitz, Rewriting modulo a congruence (in preparation), Univ. of Illinois, 1986.

*[Bachmair 1986c] L. Bachmair, N. Dershowitz, Critical-pair criteria for the Knuth-Bendix completion procedure, 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. 215-217.

[Bachmair 1987a] L. Bachmair, N. Dershowitz, Inference rules for rewrite-based first-order theorem proving, Proc. 2nd Annual IEEE Symp. on Logic in Computer Science, Ithaca, NY, 22-25 June 1987, pp. 331-337.

[Bachmair 1987b] L. Bachmair, N. Dershowitz, Completion for rewriting modulo a congruence, 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. 192-203; also Theoretical Computer Science 67(2&3):173-202, October 1989.

[Bachmair 1987c] L. Bachmair, Proof methods for equational theories, PhD thesis, Univ. of Illinois at Urbana-Champaign, Illinois, 1987; revised August 1988.

*[Bachmair 1987d] L. Bachmair, N. Dershowitz, A critical pair criterion for completion modulo a congruence, 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. 452-453.

*[Bachmair 1988a] L. Bachmair, Proof by consistency in equational theories, Proc. 3rd Annual Symp. on Logic in Computer Science (Edinburgh, Scotland, 5-8 July 1988), IEEE, 1988, pp. 228-233.

*[Bachmair 1988b] L. Bachmair, N. Dershowitz, Critical pair criteria for completion, J. of Symbolic Computation 6(1):1-18, August 1988.

*[Bachmair 1989a] L. Bachmair, Proof normalization for resolution and paramodulation, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 15-28.

*[Bachmair 1989b] L. Bachmair, N. Dershowitz, D.A. Plaisted, Completion without failure, In: Resolution of Equations in Algebraic Structures, Vol. 2: Rewriting Techniques, ed. H. Ait-Kaci and M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 1-30.

*[Bachmair 1990] L. Bachmair, H. Ganzinger,, On restrictions of ordered paramodulation with simplification, 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. 427-441.

*[Bachmair 1991] L. Bachmair, Canonical Equational Proofs, Birkhauser, Boston, 1991.

*[Bachmair 1992] L. Bachmair, H. Ganzinger, C. Lynch, W. Snyder, Basic paramodulation and superposition, 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. 462-476.

*[Bachmair 1993] L Bachmair, Rewrite techniques in theorem proving, Proc. 5th Intl. Conf, RTA-93 (Montreal, Canada, June 1993), LNCS 690, ed. C. Kirchner, Springer-Verlag, Berlin, 1993, pp. 1.

[Backer 1963] P. Backer, D. Sayre, The reduced model for satisfiability for two decidable classes of formulae in the predicate calculus, IBM Research Report, RC 1083, Yorktown Heights, 1963.

[Backhouse 1985] R. Backhouse, Algorithm development in Martin-Lof's type theory, Computer Science Department, Univ. of Essex, England, 1985.

[Baeten 1984] J.C.M. Baeten, J.A. Bergstra, J.W. Klop, Priority rewrite systems, Report CS-R8407, Centre for Mathematics and Computer Science, Amsterdam, 1984.

[Baeten 1987a] J.C.M. Baeten, J.A. Bergstra, J.W. Klop, Term rewriting systems with priorities, 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. 83-94.

*[Baeten 1988a] J.C.M. Baeten, W.P. Weijland, Semantics for Prolog via term rewrite systems, 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. 3-14.

*[Baeten 1988b] J.C.M. Baeten, J.A. Bergstra, J.W. Klop, W.P. Weijland, Term rewriting systems with rule priorities, Report CS-R8815, Centrum voor Wiskunde en Informatica, April 1988.

*[Baj 1990] F. Baj, M. Bruschi, A. Zanzi, Design and development of ENprover, an automated theorem proving system based on EN-strategy, 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. 278-279.

*[Bailin 1988] S.C. Bailin, A lambda-unifiability test for set theory, J. Automated Reasoning 4(3):269-286, September 1988.

[Bailin 1990] S.C. Bailin, D. Barker-Plummer, Automated deduction in set theory, Final Report NSF/ISI-90006, National Science Foundation, 1992; Available from National Technical Information Service, 5285 Port Royal Road, Springfield, VA 22161. [Baird 1988] T. Baird, Complete sets of reductions modulo a class of equational theories which generate infinite congruence classes, PhD dissertation, Univeersity of Missouri-Rolla, Rolla, MO, 1988.

*[Baird 1989] T.B. Baird, G.E. Peterson, R.W. Wilkerson, Complete sets of reductions modulo associativity, commutativity and identity, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 29-44.

[Baker 1992] S. Baker, A. Ireland, A. Smaill, On the use of the constructive Omega-rule within automated deduction, DAI Research Paper No. 560, Dept. of Artificial Intelligence, Univ. of Edinburgh; also International Conf. on Logic Programming and Automated Reasoning (LPAR 92, St. Petersburg), Lecture Notes in Artificial Intelligence 624, Springer-Verlag, 1992, pp. 214-225.

[Balbin 1985] I. Balbin, K. Lecot, Logic Programming: A classified bibliography, Wildgrass Books, Victoria, Australia, 1985; also D. Reidel Publ., Dordrecht, 1986.

[Ballantyne 1969] M. Ballantyne, J.H. Bennett, Semi-automated mathematics, JACM 16(1), January 1969.

[Ballantyne 1973] M. Ballantyne, W. Bennett, Graphing methods for topological proofs, Univ. of Texas at Austin, Math. Dept. Memo ATP-7, 1973.

[Ballantyne 1975a] M. Ballantyne, Computer generation of counterexamples in topology, Univ. of Texas at Austin, Math. Dept. Memo ATP-24, 1975.

[Ballantyne 1975b] A.M. Ballantyne, D.S. Lankford, An implementation of derived reduction, Univ. of Texas at Austin, Math. Dept. Memo, August 1975.

[Ballantyne 1977] A.M. Ballantyne, W.W. Bledsoe, Automatic proofs of theorems in analysis using non-standard techniques, ATP-23, Univ. of Texas at Austin; also JACM 24(3):353-374, 1977.

[Ballantyne 1979] A.M. Ballantyne, D.S. Lankford, New decision algorithms for finitely presented commutative semigroups, MTP-4, Dept. of Math., Louisiana Tech. Univ., May 1979; also J. Comput. Math. with Appl. 7(1981):159-165.

[Ballantyne 1982] A.M. Ballantyne, W.W. Bledsoe, On generating and using examples in proof discovery, Machine Intelligence 10, ed. J.H. Hayes, D. Michie, and Y.-H. Pao, Ellis Harwood Ltd., Chichester, 1982, pp. 3-39.

[Ballard 1986] D. Ballard, Parallel logical inference and energy minimization, Proc. AAAI-86, 5th Natl Conf. on Artificial Intelligence (Philadelphia, PA, 11-15 August 1986), pp. 203-208.

[Banachowski 1977] L. Banachowski, A. Kreczmar, G. Mirkowska, H. Rasiowa, A. Salwicki, An Introduction to Algorithmic Logic, Banach Center Publ., vol. 2, Warsaw, 1977.

[Baral 1990] C. Baral, J. Lobo, J. Minker, Generalized well-founded semantics for logic programs, 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. 102-116.

*[Barker-PLummer 1992a] D. Barker-Plummer, S.C. Bailin, Graphical theorem proving: an approach to reasoning with the help of diagrams, Proc. 10th ECAI (ECAI 92, Vienna, Austria, 3-7 August 1992), ed. B. Neumann, John Wiley & Sons, Chichester, 1992, pp. 55-59.

*[Barker-PLummer 1992b] D. Barker-Plummer, S.C. Bailin, A.S. Merrill, &: Automated natural deduction, 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. 716-720.

*[Barker-PLummer 1992b] D. Barker-Plummer, A. Rothenberg, The GAZER theorem 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. 726-730.

[Barnett 1992] R. Barnett, D. Basin, J. Hesketh. A recursion planning analysis of inductive completion, Research Paper 518, Dept. of Artificial Intelligence, Edinburgh, 1992; presented to the 2nd Annual Symp. on Artificial Intelligence and Mathematics.

[Barros 1984] L. Barros, J.L. Remy, ECOLOGISTE, a system to make complete and consistent specifications easier, 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. 301-318.

[Bartley 1977] W.W. Bartley, Lewis Carroll's Symbolic Logic, Clarkson N. Potter, Inc., New York, 1977.

[Barwise 1990] J. Barwise, J. Etchemendy, Valid inference and visual representation, In: Visualization in Mathematics, ed. Zimmerman and Cunningham, Mathematical Association of America, 1990.

*[Basin 1988] D.A. Basin, An environment for automated reasoning about partial functions, 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. 101-110.

[Basin 1989] D. Basin, Generalized rewriting in type theory, Tech. Report 89-1031, Cornell Univ., Computer Science Dept., 1989.

*[Basin 1990] D.A. Basin, Equality of terms containing associative-commutative functions and commutative binding operators is isomorphism complete, Proc. 10th Intl. Conf. on Automated Deduction (Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 251-260.

[Basin 1991] D.A. Basin, M. Kaufmann, The Boyer-Moore prover and Nuprl: An experimental comparison, In Logical Frameworks, Cambridge University Press, 1991, pp. 89-119.

*[Basin 1992] D. Basin, T. Walsh, Difference Matching, DAI Research Paper No. 556, Dept. of Artificial Intelligence, Univ. of Edinburgh; also Proc. 11th 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. 295-309.

*[Basin 1993a] D.A. Basin, T. Walsh, Difference unification, Proc. 13th IJCAI (Chambery, France, 28 August-3 September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 116-122.

[Basin 1993b] D. Basin, R. Constable, Metalogical frameworks, In Logical Environmnets, ed. G. Huet and G. Plotkin, Cambridge, Cambridge University Press, 1993.

[Bates 1985] J.L. Bates, R. Constable, Proofs as programs, ACM Transactions on Programming Languages and Systems 7(1):113-136, January 1985.

[Bates 1986] J.L. Bates, The PRL mathematics environment: A knowledge based medium (extended abstract), Tech. Report 86-768, Dept. of Computer Science, Cornell Univ., 1986.

[Bauderon 1986] M. Bauderon, B. Courcelle, Graph Expressions and Graph Rewritings, Rapport interne no. I-8623, Universite de Bordeaux I., September 1986.

[Bauer 1973] M. Bauer, D. Brand, M.J. Fischer, A.R. Meyer, M.S. Paterson, A note on disjunctive form tautologies, SIGACT News 5:17-20, 1973.

[Bauer 1984] G. Bauer, F. Otto, Finite complete rewriting systems and the complexity of the word problem, Acta Informatica 21(1984):521-540.

[Bauer 1985] G. Bauer, N-level rewriting systems, Theoret. Comput. Sci. 40(2-3):85-99, 1985.

*[Bauer 1992] M. Bauer, An interval-based temporal logic in a multivalued setting, 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. 355-369.

[Baxter 1973] L.D. Baxter, An efficient unification algorithm, Tech. Report CS-73-23, Dept. of Analysis and Computer Science, Univ. of Waterloo, Ontario, Canada, 1973.

[Baxter 1976a] L.D. Baxter, The complexity of unification, PhD dissertation, Dept. Comput. Sci., Univ. of Waterloo, Ontario, 1976.

[Baxter 1976b] L.D. Baxter, A practically linear unification algorithm, Report CS-76-13, Dept. Computer Science, Univ. of Waterloo, Waterloo, Ontario, Canada, 1976.

[Baxter 1977] L.D. Baxter, The complexity of unification, Internal Report CS-77-25, Faculty of Mathematics, Univ. of Waterloo, Ontario Canada, 1978.

[Baxter 1978] L.D. Baxter, The undecidability of the third order dyadic unification problem, Information and Control 38(2), 1978.

[Bayerl 1986a] C. Bayerl, Highly parallel inference machine, 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. 668-669.

[Bayerl 1986b] S. Bayerl, F. Kurfess, R. Letz, J. Schumann, PROTHEO/2; sequential PROLOG-like theorem prover based on the connection method, Tech. Univ. Munchen, W. Germany, 1986.

*[Bayerl 1987a] S. Bayerl, E. Eder, F. Kurfess, R. Letz, J. Schumann, An implementation of a PROLOG-like theorem prover based on the connection method, Proc. 2nd Intl. Conf. on Artificial Intelligence: Methodology, Systems, Applications (AIMSA'86, Varna, Bulgaria, 16-19 September 1986), ed. P. Jorrand and V. Sgurev, North-Holland, Amsterdam, 1987, pp. 29-36.

*[Bayerl 1987b] S. Bayerl, M. Breu, S. Heilmeier, K. Llichtenwalder, An implemented simulation of a parallel theorem prover, Proc. 2nd Intl. Conf. on Artificial Intelligence: Methodology, Systems, Applications (AIMSA'86, Varna, Bulgaria, 16-19 September 1986), ed. P. Jorrand and V. Sgurev, North-Holland, Amsterdam, 1987, pp. 21-28.

[Bayerl 1988] S. Bayerl, W. Ertel, R. Letz, F.Kurfess, J. Schumann, PARTHEO/5: Layout and design of full first order logic parallel inference machine, ESPRIT 415F, Deliverable D14, 1988.

[Bayerl 1989a] S. Bayerl, W. Ertel, F. Kurfess, R. Letz, J. Schumann, Ch. Suttner, and N. Trapp, PARTHEO/6: PARallel Automated THEorem Prover based on the Connection Method for Full First Order Logic -- Implementation and Performance, ESPRIT 415F Deliverable D15, 1989.

[Bayerl 1989b] S. Bayerl, W. Ertel, F. Kurfess, R. Letz, J. Schumann, D16 / Full first order logic PARallel inference machine -- Language and design, ESPRIT 415, Deliverables, Brussels, 1989.

*[Beckert 1992a] B. Beckert, R. Hahnle, An improved method for adding equality to free variable semantic tableaux, 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. 507-521.

*[Beckert 1992b] B. Beckert, S. Gerberding, R. Hahnel, W. Kernig, The tableau-based theorem prover 3TAP for muliple-valued logics, 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.758-760.

[Beeson 1981] M.J. Beeson, Formalizing constructive mathematics, why and how? in Constructive Mathematics, ed. F. Richman, Lecture Notes in Mathematics, Springer-Verlag, NY, 1981, pp. 146-190.

[Beeson 1983] M.J. Beeson, Proving programs and programming proofs, In Intl. Congress on Logic, Methodology and Philosophy of Science (Salzbury, Austria), North-Holland, Amsterdam, 1983.

[Beeson 1985] M.J. Beeson, Foundations of Contructive Mathematics, Springer-Verlag, NY, 1985.

[Beetz 1987] M. Beetz, Specifying meta-level architectures for rule-based systems, SEKI Report SR-87-06, Universitat Kaiserslautern, Fachbereich Informatik, Kaiserslautern, 1987.

*[Beetz 1988] M. Beetz, H. Freitag, J. Klug, The MKRP user manual (ed. Christoph Lingenfelder), SEKI Working Paper SWP-88-01, Universitat Kaiserslautern, 1988.

[Beierle 1986] C. Beierle, W. Olthoff, A. Voss, Automatic theorem proving in the ISDV 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. 670-671.

*[Belleannee 1990] C. Belleannee, Improving deduction in a sequent calculus, Proc. 8th Biennial Conf. of the Canadian Society for Computational Studies of Intelligence (CSCSI-90, Univ. of Ottawa, Ottawa, Canada, 22-25 May 1990), published by CSCSI, 1990, pp. 220-226.

*[Bellegarde 1987] F. Bellegarde, P. Lescanne, Transformation ordering, Proc. Intl. Joint Conf. on Theory and Practice of Software Development (TAPSOFT'87, Pisa, Italy, 23-27 March 1987), Vol. I, ed. H. Ehrig, R. Kowalski, G. Levi, and U. Montanari, LNCS 249, Springer-Verlag, Berlin, 1987, pp. 69-80.

[Bellin 1990] G. Bellin, Mechanizing proof theory: Resource-aware logics and proof transformations to extract implicit information, STAN-CS-90-1319, Dept. of Computer Science, Stanford Univ., June 1990.

[Ben-Ari 1980] M. Ben-Ari, A simplified proof that regular resolution is exponential, Information Processing Letters 10(1980):96-98.

[Ben-Ari 1981] M. Ben-Ari, Complexity of proofs and models in programming logics, PhD, Tel-Aviv Univ., May 1981.

[Benanav 1985] D. Benanav, D. Kapur, P. Narendran, Complexity of matching problems, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985, pp. 417-479; J. of Symbolic Computation 3(1 and 2):203-216, February/April 1987.

*[Benanav 1989] D. Benanav, Recognizing unnecessary inference, PhD thesis, Rensselaer Polytechnic Institute, Computer Science Dept., Troy, NY 12180, 3 January 1989; also Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 366-371.

*[Benanav 1990] D. Benanav, Simultaneous paramodulation, 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. 442-455.

[BenCherifa 1987] A. BenCherifa, P. Lescanne, Termination of rewriting systems by polynomial interpretations and its implementation, Science of Computer Programming 9(2):137-159, 1987.

*[Benhamou 1992] B. Benhamou, L. Sais, Theoretical study of symmetries in propositional calculus and applications, 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. 281-294.

[Bennett 1963] J.H. Bennett, W.B. Easton, J.R. Guard, T.H. Mott, Introduction to semi-automated mathematics, AFCRL 63-180, Air Force Cambridge Res. Lab., Cambridge, MA, April 1963.

[Bennett 1964a] J.H. Bennett, W.B. Easton, A. Guard, T.H. Mott, Toward semi-automated mathematics: The language and logic of SAM III, Sci. Rep. 2, AFCRL 64-562, Air Force Cambridge Res. Lab., Cambridge, MA, May 1964.

[Bennett 1964b] J.H. Bennett, W.B. Easton, J.R. Guard, T.H. Mott, Semi-automated mathematics: SAM IV, Sci. Rep. 3, AFCRL 64-827, Air Force Cambridge Res. Lab., Cambridge, MA, October 1964.

[Bennett 1967] J.H. Bennett, W.B. Easton, J.R. Guard, L.G. Settle, CRT-aided semi-automated mathematics, Final Report, AFCRL 67-017, Air Force Cambridge Res. Lab., Cambridge, MA, January 1967.

[Bennett 1973] A.N. Bennett, M. Bennett, W. Bennett, Graphing methods for topological proofs, Dept. Memo ATP-7, Dept. Math. Univ. of Texas at Austin, 1973.

*[Benninghofen 1987] B. Benninghofen, S. Kemmerich, M.M. Richter, eds., Systems of Reductions, LNCS 277, Springer-Verlag, Berlin, 1987.

[Benois 1987] M. Benois, Descendants of regular language in a class of rewriting systems: Algorithm and complexity of an automata construction, 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. 121-132.

*[Bergstra 1982] J.A. Bergstra, J.W. Klop, Conditional rewrite rules: Confluence and termination, Research Report IW 198/82, Mathematical Centre, Amsterdam, 1982; also J. Computer and System Sciences 32(3):323-362, June 1986.

[Bergstra 1987] J.A. Bergstra, J. Heering, P. Klint, ASF - an algebrai specification formalism, Report CS-R8705, Centre for Mathematics and Computer Science, Amsterdam, 1987.

[Bergstra 1989] J.A. Bergstra, J. Heering, P. Klint, Algebraic Specification, ACM Press, New York, New York, 1989.

[Bertling 1987] H. Bertling, H. Ganzinger, R. Schafers, CEC: A system for conditional equation completion -- User Manual (Version 1.0), Report, PROSPECTRA-Project, U. Dortmund, 1987.

*[Bertling 1988b] H. Bertling, H. Ganzinger, R. Schafers, CEC: A system for conditional equational specifications, PROSPECTRA-Report M.1.3-R-7.0, Universitat Dortmund, 1988; also 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. 249-250.

[Bertling 1988c] H. Bertling, H. Ganzinger, R. Schaefers, CEC: A system for conditional equational specifications: User Manual (Version 1.4), PROSPECTRA-Report M.a.3-R-7.0, U. Dortmund, West Germany, 1988.

[Bertling 1988c] H. Bertling, H. Ganzinger, R. Schafers, A collection of specifications completed by the CEC-system, Report, PROSPECTRA-Project, U. Dortmund, 1988.

*[Bertling 1989a] H. Bertling, H. Ganzinger, Completion-time optimization of rewrite-time goal solving, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 45-58.

[Bertling 1989b] H. Bertling, H. Ganzinger, Completion of application-restricted equations, Report 289, FB Informatik, U. Dortmund, 1989. [Besnard 1983a] P. Besnard, A proof procedure for a non-monotonic logic, Technical Note 198, Univ. of Rennes, 1983.

[Besnard 1983b] P. Besnard, R. Quiniou, P. Quinton, A theorem prover for a decidable subset of default logic, Proc. Natl Conf. on Artificial Intelligence, Washington, D.C., August 1983, pp. 27-30.

*[Besnard 1988] P. Besnard, P. Siegal, Supposition-based logic for automated nonmonotonic reasoning, 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. 592-601.

[Beth 1959] E.W. Beth, The Foundations of Mathematics, North-Holland, Amsterdam, 1959; revised edition 1964.

[Beth 1963] E.W. Beth, Observations concerning computing, deduction and heuristics, in Computer Programming and Formal Systems, ed. Braffort and Hirschberg, North-Holland, Amsterdam, 1963, pp. 21-32.

[Beth 1969] E.W. Beth, Semantic entailment and formal derivability, 1955 in Hintikka, Philosophy of Mathematics, Oxford, 1969.

[Beth 1983] E.W. Beth, On machines which prove theorems, 1958, Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 79-90.

*[Bevier 1989a] W.R. Bevier, W.A. Hunt Jr, J S. Moore, W.D. Young, An approach to systems verification, J. Automated Reasoning 5(4):411-428, December 1989.

*[Bevier 1989b] W.R. Bevier, Kit and the short stack, J. Automated Reasoning 5(4):519-530, December 1989.

*[Bezem 1988] M. Bezem, Consistency of rule-based expert 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. 151-161.

[Bibel 1974] W. Bibel, An approach to a systematic theorem-proving procedure in first-order logic, Computing 12(1974):43-55.

[Bibel 1975] W. Bibel, J. Schreiber, Proof search in a Gentzen-like system of first-order logic, Proc. Intl. Computing Symp., ed. E. Gelenbe and D. Potier, North-Holland, Amsterdam, 1975, pp. 205-212.

[Bibel 1977a] W. Bibel, A syntactic connection between proof procedures and refutation procedures, GI-3. Fachtagung Theoretische Informatik, LNCS 48, Springer-Verlag, Berlin, 1977, pp. 215-225.

[Bibel 1977b] W. Bibel, Tautology testing with an improved matrix reduction, Research report TUM-INFO-7706, Institut fur Informatik, Technische Universitat Munchen, May 1977.

[Bibel 1979] W. Bibel, Tautology testing with a generalized matrix reduction method, Theoretical Computer Science 8(1979):31-44.

*[Bibel 1980a] W. Bibel, R. Kowalski, eds., Proc. 5th Conf. on Automated Deduction (Les Arcs, France, 8-11 July 1980), ed. W. Bibel and R. Kowalski, LNCS 87, Springer-Verlag, Berlin, 1980.

[Bibel 1980b] W. Bibel, The complete theoretical basis for the systematic proof method, Technische Universitat Munchen, Bericht ATP-6-XII-80, December 1980.

[Bibel 1980c] W. Bibel, A theoretical basis for the systematic proof procedure, Proc. of 9th Symp. on Mathematical Foundations of Computer Science (Rydzzyna, Poland), ed. P. Dembinski, LNCS 88, Springer-Verlag, Berlin, 1980, pp. 154-167.

[Bibel 1980d] W. Bibel, A strong completeness result for the connection graph proof procedure, Bericht ATP-3-IV-80, Institut fur Informatic, Technische Universitat, Munchen, 1980.

[Bibel 1981a] W. Bibel, On matrices with connections, JACM 28(4):633-645, October 1981.

[Bibel 1981b] W. Bibel, Mating in matrices, Proc. GWAI-81, Informatik-Fachberichte 47, ed. Siekmann, Springer-Verlag, Berlin, 1981, pp. 171-187, revised in Research Contributions, Artificials Intelligence and Language Processing, ed. C. Montgomery and F. Fosdick, CACM 26(11):844-852, November 1983.

[Bibel 1981c] W. Bibel, On the completeness of connection graph resolution, Proc. GWAI-81, Informatik-Fachberichte 47, ed. J.H. Siekmann, Springer-Verlag, Berlin, 1981, pp. 246-247.

*[Bibel 1982a] W. Bibel, Automated Theorem Proving, Friedr. Vieweg & Sohn, Braunschweig/Wiesbaden, West Germany, 1982; 2nd Edition, Friedr. Vieweg & Verlagsgesellschaft mbH, Braunschweig, 1987.

[Bibel 1982b] W. Bibel, A comparative study of several proof procedures, Artificial Intelligence 18(3):269-293, May 1982.

[Bibel 1982c] W. Bibel, Computationally imporved versions of Herbrand's Theorem, Proc. of the Hebrand Symp., Logic Colloquium '81, ed. J. Stern, North-Holland Publishing, 1982, pp. 11-28.

[Bibel 1983] W. Bibel, E. Eder, B. Fronhoefer, Towards an advanced implementation of the connection method, Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, pp. 920-922.

[Bibel 1984] W. Bibel, B. Buchberger, Towards a connection machine for logical inference, Future Generations Computer Systems 1(1984-1985):177-185.

[Bibel 1985a] W. Bibel, Automated inferencing, J. of Symbolic Computation 1(3):245-260, September 1985.

[Bibel 1985b] W. Bibel, K. Aspetsberger, A bibliography on parallel inference machines, J. of Symbolic Computation 1:115-118, 1985.

*[Bibel 1985c] W. Bibel, B. Buchberger, Towards a connection machine for logical inference, FGCS 1(3):177-185, February 1985.

*[Bibel 1986a] W. Bibel, Methods of automated reasoning: A tutorial, In Fundamentals of Artificial Intelligence -- An Advanced Course, ed. W. Bibel and Ph. Jorrand, LNCS 232, Springer-Verlag, Berlin, 1986, pp. 171-220. [Bibel 1986b] W. Bibel, A deductive solution for plan generation, New Generation Computing 4:115-132, 1986.

[Bibel 1987a] W. Bibel, R. Letz, J. Schumann, Bottom-up enhancements of deductive systems, MS, Technische Universitat Munchen, 1987; also AI and Robotics, ed. I. Plander, North-Holland, Amsterdam (to appear).

[Bibel 1987b] W. Bibel, F. Kurfess, et al., Parallel inference machines, Bericht Nr. ATP-68-II.87, Institut fur Informatik, TUM, February 1987.

*[Bibel 1988a] W. Bibel, Finding proofs, programs, and plans, Proc. 7th Biennial Conf. of the Canadian Society for Computational Studies of Intelligence (Edmonton, Alberta, 6-10 June 1988), ed. R. Goebel, Univ. of Alberta Printing Services, 1988, pp. 1-6.

[Bibel 1988b] W. Bibel, Advanced topics in automated deduction, In: Fundamentals of Artificial Intelligence II, ed. R. Nossum, Springer, Berlin, 1988, pp. 41-59.

*[Bibel 1990a] W. Bibel, Perspectives on 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, p. 426.

*[Bibel 1990b] W. Bibel, Short proofs of the pigeonhole formulas based on the connection method, J. of Automated Reasoning 6(3):287-297, September 1990.

[Bibel 1991] W. Bibel, S. Holldobler, J. Wurtz, Cycle unification, Forschungsbericht AIDA-91-15, TH Darmstadt, August 1991.

*[Bibel 1992] W. Bibel, S. Holldobler, J. Wurtz, Cycle Unification, 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. 94-108.

[Bidoit 1982] M. Bidoit, Proofs by induction in 'fairly' specified equational theories, Proc. GWAI-82, Informatik-Fachberichte 58, ed. Wahlster, Springer-Verlag, Berlin, 1982, pp. 154-166.

[Bidoit 1983] M. Bidoit, J. Corbin, A rehabilitation of Robinson's unification algorithm, Information Processing 83, ed. R.E.A. Pavon, North-Holland, 1983, pp. 909-914.

[Bidoit 1985] M. Bidoit, C. Choppy, ASSPEGIQUE: An integrated environment for algebraic specifications, Proc. TAPSOFT '85: Coll. on Software Engineering, LNCS 186, Springer-Verlag, Berlin, 1986, pp. 246-260.

*[Bidoit 1988] M. Bidoit, F. Capy, C. Choppy, S. Kaplan, F. Schleinger, F. Voisin, ASSPEGIQUE: An integrated specification environment, 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. 251-252.

*[Bidoit 1989] M. Bidoit, F. Capy, C. Choppy, S. Kaplan, F. Schlienger, F. Voisin, ASSPEGIQUE: An integrated specification environment, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 547.

*[Bieber 1988] P. Bieber, L. Farinas del Cerro, A. Herzig, MOLOG: A modal PROGLOG, 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. 762-763.

[Bing 1969] K. Bing, Natural deduction with few restrictions on variables, Inf. Sciences 1(4):381-402, October 1969.

[Binkley 1968] R.W. Binkley, R.L. Clark, A cancellation algorithm for elementary logic, Theoria 33(1967):79-97, corrected in Theoria, 1968; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 27-47.

*[Birkhoff 1989] G. Birkhoff, Rewriting ideas from universal algebra (abstract), Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 1.

[Biundo 1986a] S. Biundo, B. Hummel, D. Hutter, C. Walther, The Karlsruhe induction 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. 672-674.

*[Biundo 1987] S. Biundo, A synthesis system mechanizing proofs by induction, Proc. 7th European Conf. on Artificial Intelligence (EDAI-86, Brighton, U.K., 20-25 July 1986), In Advances in Artificial Intelligence -- II, ed. B. du Boulay, D. Hogg, and L. Steels, North-Holland, Amsterdam, 1987, pp. 287-296.

*[Biundo 1988] S. Biundo, Automated synthesis of recursive algorithms as a theorem proving tool, Proc. 8th ECAI, Institut fur Informatik der Technischen Universitat Munchen, 1-5 August 1988, pp. 553-558.

*[Blackburn 1992] K. Blackburn, A report on ICL HOL, 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. 743-747.

[Blaine 1981] L. Blaine, Programs for structured proofs, In University-Level Computer-Assisted Instruction at Stanford: 1968-1980, ed. P. Suppes, IMSSS Stanford Univ., pp. 81-119, 1981.

[Blair 1971] F. Blair, et al., SCRATCHPAD/1: An interactive facility for symbolic mathematics, Proc. 2nd Symp. on Symbolic Manipulation, Los Angeles, 1971.

[Blasius 1981] K. Blasius, N. Eisinger, J. Siekmann, G. Smolka, A. Herold, C. Walther, The Markgraf Karl refutation procedure, Proc. 7th IJCAI, Univ. of British Columbia, Vancouver, Canada, 1981, pp. 511-518.

[Blasius 1983a] K. Blasius, Equality reasoning in clause graphics, Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, pp. 936-939.

[Blasius 1983b] K.H. Blasius, Equality reasoning based on graphs, Tech. Report SR-87-01, 1987.

[Blasius 1985] K.H. Blasius, Equality reasoning with equality paths, Proc. GWAI-85, 9th German Workshop on Artificial Intelligence (Dassel/Solling, 23-27 September 1985), Informatik-Fachberichte 118, ed. H. Stoyan, Springer-Verlag, Berlin, 1985, pp. 57-76.

*[Blasius 1986a] K.-H. Blasius, Construction of Equality Graphs, SEKI Report SR-86-01, Universitat Kaiserslautern, Dept. of Computer Science, 1986.

*[Blasius 1986b] K.-H. Blasius, Against the ``Anti Waltz Effect'' in equality reasoning, Proc. GWAI-86 und 2. Osterreichische Artificial-Intelligence-Tagung (Ottenstein/Niederosterreich, 22-26 September 1986), Informatik-Fachberichte 124, Springer-Verlag, Berlin, 1986, pp. 230-241.

*[Blasius 1986c] K.-H. Blasius, Equality reasoning based on graphs, PhD thesis, Fachbereich Informatik, Universitat Kaiserslautern, 1986; also SEKI Report SR-87-01, Universitat Kaiserslautern, 1987.

*[Blasius 1988] K.H. Blasius, J.H. Siekmann, Partial unification for graph based equational reasoning, 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. 397-414.

*[Blasius 1989] K.H. Blasius, H.J. Burckert, Deduction Systems in Artificial Intelligence, Ellis Horwood Limited, Chichester, W. Sussex; and John Wiley & Sons, NY, NY, 1989.

[Bledsoe 1967] W.W. Bledsoe, E.J. Gilbert, Automatic theorem proof-checking in set theory: a preliminary report, Sandia Corp. Rep. SC-RR-67-525, July 1967.

[Bledsoe 1970] W.W. Bledsoe, Description of LISP functions in the theorem prover, Univ. of Texas Memo, January 1970.

[Bledsoe 1971] W. Bledsoe, Splitting and reduction heuristics in automatic theorem proving, Artificial Intelligence 2(1971):55-77; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 508-530.

[Bledsoe 1972] W. Bledsoe, R. Boyer, W. Henneman, Computer proofs of limit theorems, Artificial Intelligence 3(1):27-60, 1972.

[Bledsoe 1973a] W.W. Bledsoe, Discussions on theorem proving, Dept. Memo ATP-10, Univ. of Texas at Austin, 1973.

[Bledsoe 1973b] W.W. Bledsoe, P. Bruell, A man-machine theorem proving system, Proc. 3rd IJCAI, Stanford Univ., 1973; also Artificial Intelligence 5(1):51-72, 1974.

[Bledsoe 1973c] W.W. Bledsoe, Some ideas on automatic theorem proving, Memo ATP-9, Austin, Texas: Dept of Mathematics, Univ. of Texas at Austin, 1973. [Bledsoe 1974] W.W. Bledsoe, The sup-inf method in Presburger arithmetic, Memo ATP-18, Math. Dept., Univ. of Texas at Austin, 1974.

[Bledsoe 1975a] W.W. Bledsoe, M. Tyson, The UT interactive prover, Report ATP-17a & 17b, Automated Theorem Priving Project, Dept. Math., Univ. of Texas at Austin, May 1975, 1983.

[Bledsoe 1975b] W.W. Bledsoe, A new method for proving certain Presburger formulas, Proc. 4th IJCAI, Tbilisi, Georgia, USSR, 1975, pp. 15-21.

[Bledsoe 1977a] W. Bledsoe, Non-resolution theorem proving, Artificial Intelligence 9(1):1-36, 1977; also in Readings in Artificial Intelligence, ed. B.L. Webber and N.J. Nilsson, Morgan Kaufmann Publishers, Los Altos, CA, 1981, pp. 91-108.

[Bledsoe 1977b] W.W. Bledsoe, Set Variables, Proc. 5th IJCAI, MIT, Cambridge, MA, 1977, pp. 501-510.

[Bledsoe 1977c] W. Bledsoe, A maximal method for set variables in automatic theorem proving, ATP-33, Univ. of Texas, 1977; also Machine Intelligence 9, ed. Hayes and Michie, Ellis Harwood Ltd., Chichester, 1979, pp. 53-100.

[Bledsoe 1977d] W.W. Bledsoe, M. Tyson, Typing and proof by cases in program verification, Machine Intelligence 8, ed. E.W. Elcock and D. Michie, Ellis Harwood Ltd., Chichester, Sussex, England, 1977, pp. 30-51.

[Bledsoe 1978a] W.W. Bledsoe, M. Tyson, The UT interactive prover, ATP-17A, Univ. of Texas at Austin, Texas, June 1978.

[Bledsoe 1978b] W.W. Bledsoe, M. Ballantyne, Unskolemizing, ATP-41a, Dept. Math. Univ. of Texas at Austin, 1978.

[Bledsoe 1979a] W.W. Bledsoe, P. Bruell, R. Shostak, A prover for general inequalities, ATP-40a, Dept. Math. Univ. of Texas at Austin, 1979, abridged pp. 66-69, Proc. 6th IJCAI, Tokyo, August 20-23, 1979.

[Bledsoe 1979b] W.W. Bledsoe, A resolution-based prover for general inequalities, Univ. of Texas, Math. Dept. Memo ATP-52, July 1979.

[Bledsoe 1980a] W.W. Bledsoe, L.M. Hines, Variable elimination and chaining in a resolution-based prover for inequalities, Memo ATP-56a, Math. Dept., Univ. of Texas at Austin, April 1980; also Proc. 5th Conf. on Automated Deduction (Les Arcs, France, 8-11 July 1980), ed. W. Bibel and R. Kowalski, LNCS 87, Springer-Verlag, Berlin, 1980, pp. 70-87.

[Bledsoe 1980b] W.W. Bledsoe, Automatic theorem proving, in What Can be Automated, ed. Arden, The MIT Press, Cambridge, MA, 1980.

[Bledsoe 1982a] W.W. Bledsoe, K. Kunen, R. Shostak, Completeness proofs for inequality provers, Univ. of Texas Math. Dept. Memo ATP-65, Univ. of Texas at Austin, 1982; also J. of Artificial Intelligence 27(3):255-288, December 1985.

*[Bledsoe 1982b] W.W. Bledsoe, Using examples to generate instantiations for set variables, Automatic Theorem Proving Project, Univ. of Texas at Austin, ATP-67, July 1982; also Proc. 8th IJCAI, Karlsruhe, W. Germany, 8-12 August 1983, pp. 892-901.

[Bledsoe 1982c] W.W. Bledsoe, Some automatic proofs in analysis, Automatic Theorem Proving Project, Univ. of Texas at Austin, ATP-71, December 1982; also In: Automated Theorem Proving: After 25 Years, ed. W.W. Bledsoe and D. Loveland, Contemporary Mathematics Series 19, American Math. Society, Providence, RI, 1984, pp. 89-118.

[Bledsoe 1983a] W.W. Bledsoe, The UT natural deduction prover, Automatic Theorem Proving Project, Univ. of Texas at Austin, ATP-17B, April 1983.

[Bledsoe 1983b] W.W., Ground resolution using anti-clauses, Report No. ATP-72, Departments of Mathematics and Computer Sciences, Univ. of Texas at Austin, April 1983.

[Bledsoe 1984] W.W. Bledsoe, D. Loveland, eds. Automated Theorem Proving: After 25 Years, Contemporary Mathematics Series 19, American Math. Society, Providence, RI, 1984.

[Bledsoe 1985a] W.W. Bledsoe, L.J. Henschen, What is automated theorem proving? J. of Automated Reasoning 1(1):23-27, Dordrecht, Holland: D. Reidel Publ. Co. 1985.

[Bledsoe 1985b] W.W. Bledsoe, The use of analogy in automatic proof discovery, Univ. of Texas Math Dept. Memo ATP-83, MCC-AI-158-86, November 1985.

[Bledsoe 1986a] W.W. Bledsoe, The use of analogy in proof discovery, MCC Tech. Report AI-2158-86, 1986.

[Bledsoe 1986b] W.W. Bledsoe, Some thoughts on proof discovery, MCC Tech. Report AI-208-86, June 1986; also Proc. IEEE 1986 Symp. on Logic Programming (Salt Lake City, UT, 22-25 September 1986), 1986, pp. 2-10; also in In Computers in Mathematics, ed. D.V. Chudnovsky and R.D. Jenks, Marcel Dekker, Inc., New York, 1990, pp. 83-108.

*[Bledsoe 1988] W.W. Bledsoe, R. Hodges, A survey of automated deduction, In: Exploring Artificial Intelligence: Survey Talks from the National Conferences on Artificial Intelligence, ed. H.E. Shrobe and the AAAI, Morgan Kaufmann Publishers, Inc., San Mateo, CA, 1988, pp. 483-543.

[Bledsoe 1989a] W.W. Bledsoe, Journal ready proofs: A new standard for interactive proof presentation, Univ. of Texas CS Dept. Memo, ATP 88, August 1988.

[Bledsoe 1989b] W.W. Bledsoe, The paracompactness theorem, Univ. of Texas CS Dept. Memo, ATP 96, June 1989.

*[Bledsoe 1990] W.W. Bledsoe, Challenge problems in elementary calculus, J. of Automated Reasoning 6(3):341-359, September 1990.

[Bockmayr 1987] A. Bockmayr, A note on a canonical theory with undecidable unification and matching problem, J. of Automated Reasoning 3(4):379-381, December 1987.

*[Boge 1986] W. Boge, R. Gebauer, H. Kredel, Some examples for solving systems of algebraic equations by calculating Grobner bases, J. Symbolic Computation 2(1), 1986.

[Bollen 1985] A.W. Bollen, A relevant reasoner, Research Paper No. 18, Logic Group, Research School of Social Sciences, Australian National University, 1985.

[Bollen 1987] A.W. Bollen, A relevant extension to PROLOG, Tech. Report TR-ARP-15/87, Automated Reasoning Project, Australian National University, 1987.

[Bollen 1988] A.W. Bollen, Conditional Logic Programming, Ph.D. Thesis, Australian National University, 1988.

*[Bollen 1991] A.W. Bollen, Relevant logic programming, J. Automated Reasoning 7(4):563-585, December 1991.

*[Bollinger 1991] T. Bollinger, A model elimination calculus for generalized clauses, IWBS-Report, IBM Deutschland, Scientific Center, 1991; also Proc. 12th Intl. Conf. on Artificial Intelligence, Vol 1 (IJCAI-91, Darling Harbour, Sydney, Australia, 24-30 August 1991), Morgan Kaufmann Publ., Inc., 1991, pp. 126-131.

*[Bonacina 1989] M. P. Bonacina, G. Sanna, KBlab: An equational theorem prover for the Macintosh, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 548-550.

[Book 1981] R.V. Book, C.P. O'Dunlaing, Testing for the Church-Rosser property, Theoretical Computer Science 16(2):223-230, November 1981.

[Book 1982a] R.V. Book, The power of the Church-Rosser property for string rewriting systems, Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982. pp. 360-368.

[Book 1982b] R.V. Book, Confluent and other types of Thue systems, JACM 29(2):178-218, August 1982.

[Book 1982c] R.V. Book, M. Jantzen, C. Wrathall, Monadic Thue Systems, North-Holland, Theoretical Computer Science 19(1982):231-251.

[Book 1983] R.V. Book, Decidable sentences of Church-Rosser congruences, Theoret. Comput. Sci. 24(1983):301-312.

[Book 1984] R. Book, J.H. Siekmann, On the unification hierarchy, Memo SEKI-84-V, Universitat Karlsruhe, Institut fur Informatik I, W. Germany, 1984; also Proc. GWAI-85, 9th German Workshop on Artificial Intelligence (Dassel/Solling, 23-27 September 1985), Informatik-Fachberichte 118, ed. H. Stoyan, Springer-Verlag, Berlin, 1985, pp. 111-117.

[Book 1985a] R. Book, Thue systems as rewriting systems, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985, pp. 63-94; also J. of Symbolic Computation 3(1 and 2):39-68, February/April 1987.

[Book 1985b] R.V. Book, F. Otto, Cancellation rules and extended word problems, Information Processing Letters 20(1):5-11, 1985.

[Book 1986] R.V. Book, J.H. Siekmann, On unification: Equational theories are not bounded, J. of Symbolic Computation 2(4):317-324, December 1986.

[Borning 1981] A. Borning, A. Bundy, Using matching in algebraic equation solving, DAI Research Paper 158, Univ. of Edinburgh; also Proc. 7th IJCAI, Univ. of British Columbia, Vancouver, Canada, August 1981, pp. 466-471.

[Bosco 1987a] P.G. Bosco, E. Giovannetti, C. Moiso, Refined strategies for semantic unification, Proc. Intl. Joint Conf. on Theory and Practice of Software Development (TAPSOFT'87, Pisa, Italy, March 1987), LNCS 250, Springer-Verlag, Berlin, 1987, pp. 276-290.

[Bosco 1987b] P.G. Bosco, E. Giovannetti, G. Levi, C. Moiso, C. Palamidessi, A complete semantic characterization of K-LEAF, a logic language with partial functions, Proc. 1987 Symp. on Logic Programming, IEEE Society Press, 1987, pp. 318-327.

[Bosco 1988] P.G. Bosco, E. Giovannetti, C. Moiso, Narrowing vs. SLD-resolution, J. of Theoretical Computer Science 59(1-2):3-23, North-Holland.

*[Bosco 1989] P.G. Bosco, C. Cecchi, C. Moiso, An extension of WAM for K-LEAF: A WAM-based compilation of conditional narrowing, Logic Programming: Proc. 6th Intl. Conf., ed. G. Levi and M. Martelli, The MIT Press, Cambridge, MA, 1989, pp. 318-333.

*[Bose 1988] S. Bose, E.M. Clarke, D.E. Long, S. Michaylov, Parthenon, a parallel theorem prover for non-Horn clauses, Tech. Rept. No. CMU-CS-88-137, Computer Scinece Dept., Carnegie-Mellon Univ., Pittsburgh, PA, 1988; Proc. 4th Annual Symp. Logic in Computer Science (Pacific Grove, CA, 5-8 June 1989), IEEE, 1989, pp. 80-89.

*[Boudet 1988] A. Boudet, J.P. Jouannaud, M. Schmidt-Schauss, Unification in free extensions of Boolean rings and Abelian groups, Proc. 3rd Annual Symp. on Logic in Computer Science (Edinburgh, Scotland, 5-8 July 1988), IEEE, 1988, pp. 121-130.

[Boudet 1989] A. Boudet, A new combination technique for AC unification, Internal Report 494, LRI, Orsay, France, June 1989.

*[Boudet 1990a] A. Boudet, Unification in a combination of equational theories: an efficient algorithm, 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. 292-307.

*[Boudet 1990b] A. Boudet, E. Contejean, H. Devie, A new AC unification algorithm with an algorithm for solving systems of diophantine equations, Proc. 5th Annual IEEE Symp. on Logic Computer Science (Philadelphia, PA, 4-7 June 1990), IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 289-299.

*[Boudet 1992] A. Boudet, Unification in order-sorted algebras with overloading, 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. 193-207.

[Boudol 1983a] G. Boudol, L. Kott, Recursion induction principal revisited, Theoretical Computer Science 22(1):135-174, January 1983.

[Boudol 1983b] G. Boudol, Computational semantics of terms rewriting systems, Rapports de Recherche 192, Institut National de Recherche en Informatique et en Automatique, France, February 1983; also in Algebraic Methods in Semantics, ed. M. Nivat and J.C. Reynolds, Cambridge Univ. Press, Cambridge, 1985, pp. 169-236.

*[Bouhoula 1993] A. Bouhoula, M. Rusinowitch, Automatic case analysis in proof by induction, Proc. 13th IJCAI (Chambery, France, 28 August-3 September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 88-94.

*[Bousdira 1988a] W. Bousdira, J.L. Remy, Hierarchical contextual rewriting with several levels, 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. 15-30; also Proc. 5th Annual Symp. on Theoretical Aspects of Computer Science (Bordeaux, France), ed. R. Cori and M. Wirsing, LNCS 294, Springer-Verlag, Berlin, 1988, pp. 193-206.

*[Bousdira 1988b] W. Bousdira, J.-L. Remy, REVEUR4 : A laboratory for conditional rewriting, 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. 253-257.

*[Bousdira nd] W. Bousdira, J.-L. Remy, On sufficient completeness of conditional specifications, CRIN and INRIA Lorraine, France, no date.

*[Boy 1987] T. Boy de la Tour, R. Caffera, Proof analogy in interactive theorem proving: A method to express and use it via second order pattern matching, Proc. 6th Natl Conf. on Artificial Intelligence (AAAI 87), Seattle, Washington, 13-17 July 1987, pp. 95-99.

*[Boy 1988] T. Boy de la Tour, R. Caferra, G. Chaminade, Some tools for an inference laboratory (ATINF), 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. 744-745.

*[Boy 1989a] T. Boy de la Tour, R. Caffera, A formal approach to some usually informal techniques used in mathematical reasoning, Proc. Intl. Symp. Symbolic and Algebraic Computation (ISSAC '88, Rome, Italy, 4-8 July 1988), ed. P. Gianni, LNCS 358, Springer-Verlag, Berlin, 1989, pp. 402-406.

[Boy 1989b] T. Boy de la Tour, A locally optimal transformation into clause form using partial formula renaming, RR 765-I-IMAG - 90 LIFIA, Institute IMAG, BP 68, 38402 Saint Martin d'Heres cedex, January 1989.

[Boyer 1971] R.S. Boyer, Locking: a restriction of resolution, PhD, Univ. of Texas at Austin, August 1971, 74pp.

[Boyer 1972] R.S. Boyer, J S. Moore, The sharing of structure in theorem proving programs, Machine Intelligence 7, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, Edinburgh, 1972, pp. 101-116.

[Boyer 1975] R. Boyer, J S. Moore, Proving theorems about LISP functions, DCL Memo 60, Univ. of Edinburgh; also Proc. 3rd IJCAI, Stanford Univ., pp. 486-493; also JACM 22(1):129-144, 1975.

[Boyer 1977a] R.S. Boyer, J S. Moore, A fast string searching algorithm, CACM 20(10), 1977.

[Boyer 1977b] R.S. Boyer, J S. Moore, A lemma driven automatic theorem prover for recursive function theory, Proc. 5th IJCAI, MIT, Cambridge, MA, 1977, pp. 511-519.

[Boyer 1979a] R.S. Boyer, J S. Moore, A Computational Logic, Academic Press, NY, 1979.

[Boyer 1979b] R.S. Boyer, J S. Moore, A theorem prover for recursive functions: A user's manual, Tech. Rep. CSL-91, Comput. Sci Lab. SRI International, Menlo Park, June 1979.

[Boyer 1981a] R.S. Boyer, J S. Moore, eds., The Correctness Problem in Computer Science, Academic Press, London, 1981.

[Boyer 1981b] R.S. Boyer, J S. Moore, Metafunctions: Proving them correct and using them efficiently as new proof procedures, SRI International Tech. Report CSL-108, 1979; also In: The Correctness Problem in Computer Science, ed. R.S. Boyer and J S. Moore, Academic Press, London, 1981, pp. 103-184.

[Boyer 1982a] R.S. Boyer, J S. Moore, A mechanical proof of the unsolvability of the halting problem, ICSCA-CMP-28, Univ. of Texas at Austin, July 1982; also JACM 31(3):441-458, 1984.

[Boyer 1982b] R.S. Boyer, J S. Moore, Proof checking the RSA public key encryption algorithm, ICSCA-CMP-33, Univ. of Texas at Austin, September 1982.

[Boyer 1983a] R.S. Boyer, J S. Moore, Proof-checking, theorem-proving, and program verification, Technical Report 35, Univ. of Texas at Austin, January 1983.

[Boyer 1983b] R.S. Boyer, J S. Moore, A fully automatic proof of the correctness of an ordered tree insertion function, ICSCA-CMP-36, Univ. of Texas at Austin, May 1983.

[Boyer 1983c] R.S. Boyer, J S. Moore, A mechanical proof of the Turing completeness of pure Lisp, ICSCA-CMP-37, Univ. of Texas at Austin, May 1983; also In: Automated Theorem Proving: After 25 Years, ed. W.W. Bledsoe and D.W. Loveland, American Mathematical Society, Providence, RI, 1984, pp 133-167.

[Boyer n.d.] R.S. Boyer, J S. Moore, The User's Manual for a Computational Logic, Tech. Report 18, Computational Logic, Inc., 1717 West Sixth Street Suite 290, Austin, TX 78703.

[Boyer 1985a] R.S. Boyer, J S. Moore, Program Verification, J. of Automated Reasoning 1(1):17-22, D. Reidel Publ. Co., Dordrecht, Holland, 1985.

*[Boyer 1985b] R.S. Boyer, J S. Moore, Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic, Tech. Report ICSCA-CNP-44, Univ. of Texas at Austin, 1985; also in Machine Intelligence 11: Logic and the acquisition of knowledge ed. Hayes, Michie and Richards, Clarendon Press, Oxford, 1988, pp. 83-124.

[Boyer 1986a] R.S. Boyer, E. Lushk, W. McCune, R. Overbeek, M. Stickel, and L. Wos, Set theory in first-order logic: Clauses for Godel's axioms, J. of Automated Reasoning 2(3):287-327, September 1986.

[Boyer 1986b] R.S. Boyer, J S. Moore, Overview of a Theorem-Prover for a Computational 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. 675-678.

[Boyer 1986c] R.S. Boyer, Rewrite Rule Compilation, MCC Tech. Report AI-194-86, June 1986.

*[Boyer 1987] R.S. Boyer, J S. Moore, The addition of bounded quantification and partial functions to a computational logic and its theorem prover, ICSCA-CMP-52, Institute for Computing Science and Computer Applications, Univ. of Texas at Austin, Austin, Texas, January 1987.

*[Boyer 1988a] R.S. Boyer, J S. Moore, Quantification and partial functions to a computational logic and its theorem prover, J. Automated Reasoning 4(2):117-172, June 1988.

[Boyer 1988b] R.S. Boyer, J S. Moore, A Computational Logic Handbook, Academic Press, Boston, 1988.

[Boyer 1988c] R.S. Boyer, J S. Moore, The code for a computational logic, Tech. Report CLI-24, Computational Logic, Inc., 1988.

[Boyer 1988d] R.S. Boyer, J S. Moore, D. Russinoff, and N. Shankar, Basic events for a computational logic, Tech. Report CLI-23, Computational Logic, Inc., 1988.

[Boyer 1989] R.S. Boyer, D.M. Goldschlag, M. Kaufmann, and J S. Moore, Functional instantiation in first order logic, Report 44, Computational Logic, 1717 W. 6th St., Austin, TX 78703, U.S.A., 1989; to appear in the proc. of the 1989 Workshop of Programming Logic, Programming Methodology Group, Univ. of Goteborg.

*[Boyer 1989] R. Boyer, Note on verification, J. of Automated Reasoning 5(2):125, June 1989.

*[Boyer 1990] R.S. Boyer, J S. Moore, A theorem prover for a computational logic, Proc. 10th Intl. Conf. on Automated Deduction (Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 1-15.

*[Boyer 1992] R.S. Boyer, Y. Yu, Automated correctness proofs of machine code programs for a commercial microprocessor, 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. 416-430.

*[Brackin 1987] S.H. Brackin, Knowledge-based theorem proving for verification, M87-75, MITRE, Bedford, MA, September 1987, 66p.

[Brady 1976] R.T. Brady, A computer program for determining matrix models of propositional calculi, Logique et Analyse 74(1976):233-253.

[Branagan 1981] E.J. Branagan, An interactive theorem prover verification, CES-81-09, Case Western Reserve Univ., Computer Engineering and Science Dept., August 1981.

[Brand 1973] D. Brand, Resolution and equality in theorem proving, Technical Report 58, Dept. of Computer Science, Univ. of Toronto, 1973.

[Brand 1975] D. Brand, Proving theorems with the modification method, SIAM J. Computing 4(4):412-430, December 1975.

[Brand 1976] D. Brand, Analytic resolution in theorem proving, Artificial Intelligence 7(4), 1976.

*[Brand 1978] D. Brand, J.A. Darringer, W.H. Joyner, Completeness of conditional reductions, IBM Tech. Report RC-7404, T.J. Watson Research Center, Yorktown Heights, NY, December 1978; also Proc. 4th Workshop on Automatic Deduction, Austin, Texas, 1-3 February 1979, pp. 36-42.

[Bratko 1982] I. Bratko, Knowledge-based problem solving, Machine Intelligence 9, ed. Hayes, Michie, and Pao, Ellis Harwood Ltd., Chichester, 1982, pp. 73-100.

*[Breben 1981] M. Breben, A. Ferro, E.G. Omodeo, J.T. Schwartz, Decision procedures for elementary sublanguages of set theory. II: Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions, Commun. Pure and Appl. Math. 34(2):177-195, 1981.

[Breben 1982] M. Breban, Decision algorithms for a class of set-theoretic formulae involving one occurrence of the union set operator, PhD. thesis, Courant Institute, New York Univ., 1982.

*[Breben 1984] M. Breben, A. Ferro, Decision procedures for elementary sublanguages of set theory. III: Restricted classes of formulas involving the powerset operator and the general set union operator, Advances in Applied Mathematics 5(2):147-215, June 1984.

[Brice 1971] C. Brice, J. Derksen, A heuristically guided equality rule in a resolution theorem prover, Tech. Note 45, Stanford Res. Inst. Artificial Intelligence Group, 1971.

[Brock 1986] B. Brock, S. Cooper, W. Pierce, Some experiments with analogy in proof discovery (preliminary report), MCC Tech. Report AI-347-86, Microelectronics and Computer Technology Corporation, Austin, TX, October 1986.

[Brock 1987a] B. Brock, S. Cooper, W. Pierce, Some experiments with analogy in proof discovery: A natural deduction approach, MCC Tech. Report ACA-AI-274-87, Microelectronics and Computer Technology Corporation, Austin, TX, August 1987.

[Brock 1987b] B. Brock, S. Cooper, W. Pierce, Box users manual, MCC Tech. Rport ACA-AI-273-87, September 1987.

*[Brock 1988] B. Brock, S. Cooper, W. Pierce, Analogical reasoning and proof discovery, 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. 454-468.

*[Brock 1989] B. Brock, An experimental implementation of equivalence reasoning in the Boyer-Moore theorem prover, Internal note 104, Computational Logic Inc., Draft, 25 January 1989.

[Broda 1980] K. Broda, The relation between semantic tableaux and resolution theorem-provers, Internal report, Department of Computing and Control, Imperial College, Univ. of London, 1980.

[Broda 1984] K. Broda, D.M. Gabbay, F. Kriwaczek, A goal directed theorem prover for classical logic, Research Report, Dept. of Computing, Imperial College, London, 1984.

*[Brogi 1990] A. Brogi, P. Mancarella, D. Pedreschi, F. Turini, Universal quantification by case anaylsis, Proc. 9th ECAI (Stockholm, Sweden, 6-10 August 1990), ed. L.C. Aiello, Pitman Publishing, London, 1990, pp. 111-116.

[Brotz 1974a] D.K. Brotz, Embedding heuristic problem solving methods in a mechanical theorem prover, STAN-CS-74-443, Computer Sci. Dept., Stanford Univ., August 1974.

[Brotz 1974b] D. Brotz, Proving theorems by mathematical induction, PhD thesis, Computer Science Dept., Stanford Univ., 1974.

[Brown 1968] T.C. Brown, Resolution with covering strategies and equality theory, California Institute of Technology, CA, 1968.

[Brown 1973] F.M. Brown, The use of several models as a refinement of resolution with sets of Horn clauses, Memo. 63, Dept. of Computational Logic, Univ. of Edinburgh, 1973.

[Brown 1974] T. Brown, A structured design-method for specialized proof procedures, PhD thesis, California Inst. of Tech., Pasadena, 1974.

[Brown 1976] F.M. Brown, A deductive system for elementary arithmetic, Proc. 2nd AISB Conf., Edinburgh, 1976.

[Brown 1977a] F.M. Brown, Doing arithmetic without diagrams, Artificial Intelligence 8(2):175-200, 1977.

[Brown 1977b] R. Brown, Use of analogy to achieve new expertise, AI-TR-403, Artificial Intelligence Lab., MIT, 1977.

*[Brown 1977c] F.M. Brown, A theorem prover for elementary set theory, Proc. 5th IJCAI, MIT, Cambridge, MA, 22-25 August 1977, pp. 534-540.

[Brown 1977d] F.M. Brown, Inductive reasoning in mathematics, Proc. 5th IJCAI, MIT, Cambridge, MA, August 1977.

*[Brown 1978a] F.M. Brown, Towards the automation of set theory and its logic, Artificial Intelligence 10(3):281-316, November 1978.

[Brown 1978b] F.M. Brown, A sequent calculus for modal quantification logic, Proc. 3rd AISB/GI Conf., Hamburg, 1978.

[Brown 1978c] F.M. Brown, An automatic proof of the completeness of quantification logic, Dept. of Artificial Intelligence Research Rept. 52, 1978.

[Brown 1979a] F. Brown, A theorem prover for meta-theory, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979.

[Brown 1979b] F.M. Brown, S.A. Tarnlund, Inductive reasoning on recursive equation, Artificial Intelligence 12(1979): 207-229.

[Brown 1980] F.M. Brown, An investigation into the goals of research in automatic theorem proving as related to mathematical reasoning, Artificial Intelligence 14(3):221-242, October 1980.

[Brown 1981] F.M. Brown, Computation with automatic theorem provers, Proc. NSF Workshop on Logic Programming, Los Angeles, CA, 1981.

[Brown 1984] C.A. Brown, A self-modifying theorem prover, Proc. AAAI-84, Natl Conf. on Artificial Intelligence, Univ. of Texas at Austin, 6-10 August 1984, pp. 38-41.

[Brown 1985a] F.M. Brown, P. Liu, A logic programming and verification system for recursive quantificational logic, Proc. 9th IJCAI, Vol. 2, Los Angeles, CA, 18-23 August 1985.

[Brown 1986] F.M. Brown, An experimental logic based on the fundamental deduction principle, AIRIT TR-86-5, also Artificial Intelligence 30(2):117-263, 1986.

[Brown 1986b] R.M. Brown, A commonsense theory of nonmonotonic reasoning, 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. 209-228.

[Brown 1986c] R.M. Brown, Automatic deduction in set theory, Dept. of Computer Science TR-86-6, Univ. of Kansas, 1986.

*[Brown 1988a] F.M. Brown, S.S. Park, J. Phelps, SYMEVAL: A theorem prover based on the experimental logic, 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. 756-757.

*[Brown 1988b] F.M. Brown, S.S. Park, J. Phelps, ZPLAN: An automatic reasoning system for situations, 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. 758-759.

*[Brown 1988c] C. Brown, G. Cooperman, L. Finkelstein, Solving permutation problems using rewriting systems, Proc. Intl. Symp. Symbolic and Algebraic Computation (ISSAC '88, Rome, Italy, 4-8 July 1988), ed. P. Gianni, LNCS 358, Springer-Verlag, Berlin, 1989, pp. 364-377.

*[Brown 1990a] F.M. Brown, C. Araya, Schemata (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. 643-644.

*[Brown 1990b] F.M. Brown, C. Araya, Cylindric algebra equation solver (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. 645-646.

[Bruell 1973] P. Bruell, A description of the functions of the man-machine topology theorem prover, Univ. of Texas at Austin, Math. Dept. Memo ATP-8, 1973.

[Bruijn 1970a] N.G. de Bruijn, The mathematical language AUTOMATH, its sage and some of its extensions, Symp. on Automatic Demonstration (Versailles, France, 1968), ed. M. Laudet, D. Lacombe, L. Nolin, and M. Schutzenberger, Lecture Notes in Math. 125, Springer-Verlag, Berlin, 1970, pp. 29-61; also Symp. on Automatic Demonstration (IRIA, Versailles, 1968), Springer-Verlag, NY, Lecture Notes in Mathematics 125(1970):29-61.

[Bruijn 1970b] N.G. de Bruijn, On the use of bound variables in AUTOMATH, Notitie 9, Tech. Hochschule Eindhoven, 1970.

[Bruijn 1970c] N.G. de Bruijn, Formulas with indications for establishing definitional equivalence, Notitie 15, Tech. Hochschule Eindhoven, 1970.

[Bruijn 1971] N.G. de Bruijn, AUTOMATH, a language for mathematics, Notes (prepared by B. Fawcett) of a series of lectures in the Seminaire de Mathematiques Superieures, Universite de Montreal, 1971.

[Bruijn 1972] N.G. de Bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Indagationes Mathematicae 34(5):381-392, 1972.

[Bruijn 1974] N.G. de Bruijn, Some extensions of Automath: the AUT-4 family, Internal Automath memo M10, January 1974.

[Bruijn 1975] N.G. de Bruijn, An Algol program for deciding derivability in minimal propositional calculus with implication and conjunction over a three letter alphabet, Technological University Eindhoven, Memorandum 1975-06, 1975.

[Bruijn 1980] N.G. de Bruijn, A survey of the project AUTOMATH, in To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, ed. J.P. Seldin and J.R. Hindley, Academic Press, NY, 1980, pp. 579-606.

[Bruijn 1983] N.G. de Bruijn, AUTOMATH - a language for mathematics, Technological Univ., Eindhoven, Netherlands, 1968; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 159-200.

[Bruynooghe 1975] M. Bruynooghe, The inheritance of links in a connection graph, Report CW 2, Applied Mathematics and Programming Division, Katholieke Universiteit Leuven, 1975.

[Bruynooghe 1981] M. Bruynooghe, L.M. Pereira, Revision of top-down logical reasoning through intelligent backtracking, Report CIUNL-8/81, Universidade Nova de Lisboa, Portugal, 1981.

[Bruynooghe 1983] M. Bruynooghe, Deduction revision by intelligent backtracking, Universidade Nova de Lisboa, Research Report, July 1983.

[Bry 1986] F. Bry, R. Manthey, Proving finite satisfiability of first-order theories, Internal Report KB-27, ECRC, 1986.

*[Bryant 1986] R. E. Bryant, Graph-based algorithms for Boolean functions manipulations, IEEE Transactions on Computers C-35(8):677-691, August 1986. [Buchanan 1985] B.G. Buchanan, Expert Systems, J. of Automated Reasoning 1(1):28-34, D. Reidel Publ. Co., Dordrecht, Holland, 1985.

*[Buchanan 1991] S.A. Buchanan, Some theoretical problems when solving systems of polynomial equations using Grobner bases, SIGSAM Bulletin 25(2):24-27, April 1991.

[Buchberger 1965] B. Buchberger, An algorithm for finding a basis for the residue class ring of a zero-dimensional polynomial ideal, in German, PhD thesis, Univ. of Innsbruck, Austria, Math., Inst., 1965.

[Buchberger 1970] B. Buchberger, An algorithmic criterion for the solvability of an algebraic system of equations, Aequations Mathematical 4/3(1970):374-383.

[Buchberger 1976a] B. Buchberger, A theoretical basis for the reduction of polynomials to canonical forms, ACM-SIGSAM Bulletin 10(3):19-27, August 1976.

[Buchberger 1976b] B. Buchberger, Some properties of Grobner bases for polynomial ideals, JACM SIGSAM Bull. 10(4):19-24, 1976.

[Buchberger 1979] B. Buchberger, A criterion for detecting unnecessary reductions in the construction of Grobner bases, Proc. EUROSAM 79 (Marseille, June 1979), ed. W. Ng, LNCS 72, Springer-Verlag, Berlin, pp. 3-21.

[Buchberger 1982a] B. Buchberger, G.E. Collins, R. Loos, eds., Computer Algebra: Symbolic and Algebraic Computations, Computing Suppl. 4, Springer-Verlag, NY, 1982, 2nd edition 1983.

[Buchberger 1982b] B. Buchberger and R. Loos, Algebraic Simplification, In: Computer Algebra: Symbolic and Algebraic Computations, Computing Suppl. 4, ed. B. Buchberger, G.E. Collins, and R. Loos, Springer-Verlag, NY, 1982, 2nd edition 1983, pp. 11-43.

[Buchberger 1983] B. Buchberger, A note on the complexity of constructing Grobner bases, Proc. EUROCAL 83, LNCS 162, Springer-Verlag, Berlin, 1983, pp. 137-145.

[Buchberger 1984] B. Buchberger, A critical pair completion algorithm for finitely generated ideals in rings, Proc. Symp. Rekursive Kombinatorik, Logic and Machines: Decision Problems and Complexity, ed. E. Borger, et al., LNCS 171, Springer-Verlag, Berlin, 1984, pp. 137-161.

[Buchberger 1985a] B. Buchberger, Grobner bases: An algorithmic method in polynomial ideal theory, In: Recent Trends in Multidimensional Systems Theory, ed. N.K. Bose, D. Reidel Publishing Company, Dordrecht, 1985, pp. 184-232.

[Buchberger 1985b] B. Buchberger, Basic features and development of the critical-pair/completion approach, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985, pp. 1-45.

[Buchberger 1985c] B. Buchberger, A survey on the method of Grobner bases for solving problems in connection with systems of multi-variate polynomials, 2nd RIKEN Intl. Symp. on Symbolic and Algebraic Computation by Computers, ed. N. Inada and T. Soma, World Scientific Publishing Co., 1985, pp. 69-83.

[Buchberger 1985d] B. Buchberger, History and basic features of the critical-pair/completion procedure, Proc. 1st Intl. Conf. Rewriting Techniques and Applications, LNCS 202, Springer-Verlag, Berlin, 1985, pp. 301-324; also J. of Symbolic Computation 3(1 and 2):3-38, February/April 1987.

*[Buchberger 1987] B. Buchberger, Applications of Grobner bases in non-linear computational geometry, Proc. Trends in Computer Algebra, Intl. Symp. (Bad Neuenahr, 19-21 May 1987), ed. R. Janssen, LNCS 296, Springer-Verlag, Berlin, pp. 52-80.

*[Buchberger 1988] B. Buchberger, G.E. Collins, B. Kutzler, Algebraic methods for geometric reasoning, 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. 85-119.

[Buchen 1979] H. Buchen, Reduction systems and small cancellation theory, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979, pp. 53-59.

[Buchholz 1981] W. Buchholz, S. Feferman, W. Pohlers, W. Sieg, Iterated inductive definitions and subsystems of analysis, In Recent Proof-Theoretical Studies, Lecture Notes in Mathematics 897, Springer-Verlag, NY, 1981.

[Buchi 1960] J.R. Buchi, On a decision method in restricted second order arithmetic, Proc. Intl. Congress on Logic Methodology and Philos. Sci., ed. E. Nagel and P. Suppes, Stanford Univ. Press, Stanford, 1960, pp. 1-11.

[Buines-Rozas 1979] J. Buines-Rozas, GOAL: A goal-oriented command language for interactive proof construction, PhD thesis, Stanford Univ. Dept. of Computer Science, 1979.

[Bulnes 1979] J. Bulnes, Goal: a goal oriented command language for interactive proof construction, Stanford AI Memo AIM-328, 1979.

[Bundgen 1987] R. Bundgen, Design, implementation, and application of an extended ground-reducibility test, Master's thesis, Computer and Information Sciences, Univ. of Delaware, Newark, DE 19716, 1987; also Tech. Report 88-05, Computer and Information Sciences, Univ. of Delaware, Newark, DE 19716, December 1987.

*[Bundgen 1989] R. Bundgen, W. Kuchlin, Computing ground reducibility and inductively complete positions, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 59-75.

[Bundy 1971] A. Bundy, Counterexamples and conjectures: There is no best proof procedure, Metamathematics Unit, Univ. of Edinburgh, 1971.

[Bundy 1973] A. Bundy, Doing arithmetic by diagrams, Proc. 3rd IJCAI, Stanford Univ., 1973, pp. 130-138.

[Bundy 1975] A. Bundy, Analysing mathematical proofs (or reading between the lines), Proc. 4th IJCAI, Tbilisi, Georgia, USSR, 1975. pp. 22-28.

[Bundy 1977] A. Bundy, Exploiting the properties of functions to control search, Research Report 45, Dept. of AI, Univ. of Edinburgh, 1977.

[Bundy 1979a] A. Bundy, Bob Welhan, Using meta-level descriptions for selective application of multiple rewrite rule sets in algebraic manipulation, DAI Working Paper 55, Univ. of Edinburgh, Dept. of Artificial Intelligence; also Artificial Intelligence 16(2):189-211, May 1981.

[Bundy 1979b] A. Bundy, L. Byrd, G. Luger, C. Mellish, R. Milne, M. Palmer, Solving mechanics problems using meta-level inference, Proc. IJCAI-79 (6th IJCAI), ed. B.G. Buchanan, Tokyo, August 1979, pp. 1017-1027; reprinted in Expert Systems in the Microelectronic Age, ed. D. MIchie, pp. 50-64, Edinburgh Univ. Press, 1979; also available from Edinburgh Univ., DAI Research Paper 112.

[Bundy 1980] A. Bundy, B. Welham, Meta-level inference, Proc. 5th Conf. on Automated Deduction (Les Arcs, France, 8-11 July 1980), ed. W. Bibel and R. Kowalski, LNCS 87, Springer-Verlag, Berlin, 1980.

[Bundy 1981a] A. Bundy, B. Silver, Homogenization: Preparing equations for change of unknown, DAI Research Paper 159, Univ. of Edinburgh; also Proc. 7th IJCAI, Univ. of British Columbia, Vancouver, August 1981, pp. 551-553.

[Bundy 1981b] A. Bundy, Bob Welhan, Using meta-level inference for selective application of multiple rewrite rule sets in algebraic manipulation, DAI Research Paper 121, Edinburgh, 1981; also Artificial Intelligence 16(2):189-212, May 1981.

[Bundy 1981c] A. Bundy, L.S. Sterling, Meta-level inference in algebra, Research Paper 164, Dept. of Artificial Intelligence, Edinburgh, September 1981 (see revised version, DAI Research Paper 273, 1985); also Workshop on Logic Programming for Intelligent Systems, Los Angeles, 1981.

*[Bundy 1982a] A. Bundy, L. Byrd, C.S. Mellish, Special-purpose, but domain-independent, inference mechanisms, DAI Research Paper 179, Dept. of Artificial Intelligence, Univ. of Edinburgh, Edinburgh; also Proc. ECAI-82, Paris-Sud, Orsay, France, 12-14 July 1982, pp. 67-74; also Progress in Artificial Intelligence, ed. L. Steels and J.A. Campbell, Ellis Horwood Limited, Chichester, West Sussex, 1985. pp. 93-111.

[Bundy 1982b] A. Bundy, L. Byrd, R. O'Keefe, B. Silver, L. Sterling, Solving symbolic equations with press, In Computer Algebra, LNCS 144, ed. J. Calmet, Springer, pp. 109-116.

[Bundy 1983a] A. Bundy, The Computer Modelling of Mathematical Reasoning, Academic Press, NY, 1983.

[Bundy 1983b] A. Bundy, Finding a common currency - a new proof plan, Note 159, Univ. of Edinburgh, Artificial Intelligence Dept., Edinburgh, 1983.

[Bundy 1983c] A. Bundy, The impress proof plan revisited, Working Paper 138, Dept of Artificial Intelligence, Edinburgh, April 1983.

[Bundy 1985a] A. Bundy, Discovery and reasoning in mathematics, Research Paper 266, Dept. of Artificial Intelligence, Univ. of Edinburgh, Edinburgh, 1985; also Proc. 9th IJCAI, Los Angeles, CA, 1985, pp. 1221-1230.

[Bundy 1985b] A. Bundy, Meta-level inference in algebra, Research Paper 273, Dept. of Artificial Intelligence, Univ. of Edinburgh, Edinburgh, 1985 (revised version of DAI Research Paper 164); also in Proc. Capri-85 Conf. on AI, North Holland Publishers, Amsterdam.

[Bundy 1985c] A. Bundy, Proof Analysis: A technique for concept formation, DAI Research Paper 198, Dept. of Artificial Intelligence, Univ. of Edinburgh; also Proc. AISB-85, ed. P. Ross, 1985, pp. 78-86.

*[Bundy 1986] A. Bundy, `Poof' Analysis: A technique for concept formation, Proc. Conf. of the Society for the Study of Artificial Intelligence and Simulation of Behaviour (AISB, Warwick Univ., England, 10-12 April 1985), In: Artificial Intelligence and its applications, ed. A.G. Cohn and J.R. Thomas, John Wiley & Sons, Chichester, 1986, pp. 51-59.

[Bundy 1987a] A. Bundy, The derivation of tactic specifications, Blue Book Note 356, Dept. of Artificial Intelligence, Univ. of Edinburgh, March 1987.

*[Bundy 1987b] A. Bundy, The use of explicit plans to guide inductive proofs, DAI Research Paper 349, Dept. of Artificial Intelligence, Univ. of Edinburgh, 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. 111-120.

*[Bundy 1988a] A. Bundy, L. Sterling, Meta-level inference two applications, Research Paper No. 273, Dept. of AI, Univ. of Edinburgh; also J. of Automated Reasoning 4(1):15-27, March 1988.

*[Bundy 1988b] A. Bundy, F. van Harmelen, J. Hesketh, A. Smaill, Experiments with proof plans for induction, DAI Research Paper 413, Dept. of Artificial Intelligence, Univ. of Edinburgh, Forrest Hill, Edinburgh, EH1 2QL, Scotland, 1988; also J. Automated Reasoning 7(3):303-324, September 1991.

[Bundy 1989a] A. Bundy, F. van Harmelen, J. Hesketh, A. Smaill, A. Stevens, A rational reconstruction and extension of recursion analysis, DAI Research Paper 419, Dept. of Artificial Intelligence, Univ. of Edinburgh, Forrest Hill, Edinburgh, EH1 2QL, Scotland; also Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 359-365;

[Bundy 1989b] A. Bundy, A science of reasoning, DAI Research Paper 445, Dept. of Artificial Intelligence, Univ. of Edinburgh, Forrest Hill, Edinburgh, EH1 2QL, Scotland; also In Computational Logic: Essays in Honor or Alan Robinson, ed. J.-L. Lassez and G. Plotkin, MIT Press, 1991, pp. 178-198.

*[Bundy 1989c] A. Bundy, F. van Harmelen, A. Smaill, Extensions to the rippling-out tactic for guiding inductive proofs, DAI Research Paper 459, Dept. of Artificial Intelligence, Univ. of Edinburgh, Forrest Hill, Edinburgh, EH1 2QL, Scotland; also 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. 132-146.

*[Bundy 1989d] A. Bundy, F. van Harmelen, J. Hesketh, A. Smaill, A. Stevens, A rational reconstruction and extension of recursion analysis, Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 359-365.

*[Bundy 1990a] A. Bundy, A science of reasoning: extended 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. 633-640.

*[Bundy 1990b] A. Bundy, F. van Harmelen, C. Horn, A. Smaill, The oyster-clam system (abstract), DAI Research Paper No. 507, Univ. of Edinburgh; 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. 647-648.

[Bundy 1990c] A. Bundy, A. Smaill, J. Hesketh, Turning Eureka steps into calculations in automatic program synthesis, DAI Research Paper 448, Dept. of Artificial Intelligence, Univ. of Edinburgh, Scotland, 1990; to appear in the Proc. of the UK IT 90 Conf.

*[Bundy 1990d] A. Bundy, The use of proof plans in formal methods, 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. 151-153.

[Bundy 1990e] A. Bundy, G. Giunchiglia, T. Walsh, Building abstractions, In Proc. of the AAAI-90 Workshop on automatic Generation of Approximations and Abstractions, pp. 221-232, American Association for Artificial Intelligence, 1990; also DAI Research Paper No. 506, Univ. of Edinburgh.

[Bundy 1991a] A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, A. Smaill, Rippling: A heuristic for guiding inductive proofs, DAI Research Paper No. 567, Dept. of Artificial Intelligence, Univ. of Edinburgh, 1991; also Artificial Intelligence 62:185-253, 1993.

[Bundy 1991] A. Bundy, The use of proof plans for normalization, In Essays in Honor of Woody Bledsoe, ed. R.S. Boyer, Kluwer, 1991, pp. 149-166; also DAI Research Paper No. 513, Univ. of Edinburgh.

*[Buning 1990] H.K. Buning, U. Lowen, S. Schmitgen, Equivalence of propositional Prolog programs, J. of Automated Reasoning 6(3):319-335, September 1990.

*[Buntine 1988] W. Buntine, Generalized subsumption and its applications to induction and redundancy, Artificial Intelligence 36(2):149-177, September 1988.

[Buntine 1989] W. Buntine, H.-J. Burchert, On solving equations and disequations, SEKI Report SR-89-03, Fachbereich Informatik, Universitat Kaiserslautern, Kaiserslautern, 1989.

[Burckert 1983] H.-J. Burckert, H. Wang, R. Zheng, MKRP: A performance test by working mathematics, Memo SEKI-83-I, Institut fur Informatik I, Universitat Karlsruhe, W. Germany, 1983.

[Burckert 1986a] H.-J. Burckert, Some relationships between unification, restricted unification, and matching, SEKI Report SR-86-05, Universitat Kaiserslautern, 1986; 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. 514-524.

[Burckert 1986b] H.J. Burckert, A. Herold, M. Schmidt-Schauss, On equational theories, unification and decidability, SEKI Report SR-86-20, Universitat Kaiserslautern, 1986; also 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. 204-215; also Special Issue on Unification, J. Symbolic Computation, ed. C. Kirchner, 1989.

*[Burckert 1987a] H.-J. Burckert, Matching - A special case of unification? SEKI Report SR-87-08, Universitat Kaiserslautern, 1987; also J. Symbolic Computation 8(1989):523-536.

*[Burckert 1987b] H.-J. Burckert, Lazy E-unification - A method to delay alternative solutions, SEKI Working Paper SWP-87-07, Universitat Kaiserslautern, 1987; also Proc. 1st Workshop on Unification, University Nancy, Rapport Interne no. 87 R 34, ed. C. Kirchner, 1987.

*[Burckert 1987c] H.-J. Burckert, Solving disequations in equational theories, SEKI Report SR-87-15, 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. 517-526.

*[Burckert 1988] H.-J. Burckert, A. Herold, D. Kapur, J.H. Siekmann, M.E. Stickel, M. Tepp, H. Zhang, Opening the AC-Unification Race, SEKI Report SR-88-11, Universitat Kaiserslautern, July 1988; also J. Automated Reasoning 4(4):465-474, December 1988.

[Burckert 1989a] H.-J. Burckert, M. Schmidt-Schauss, On the solvability of equational problems, SEKI Report SR-89-07, Universitat Kaiserslautern, 1989.

[Burckert 1989b] H.-J. Burckert, A. Herold, and M. Schmidt-Schauss, On equational theories, unification, and (un)decidability, J. of Symbolic Computation 8(1 and 2):3-49, 1989 (special issue on unification. part 2).

*[Burckert 1990] H.-J. Burckert, A resolution principle for clauses with constraints, Research Report RR-90-02, Deutsches Forschungszentrum fur Kunstliche Intelligenz GmbH, Kaiserslautern, March 1990; also 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. 178-192.

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

[Burstall 1968] R.M. Burstall, A scheme for indexing and retrieving clauses for a resolution theorem-prover, MIP-R-45, Univ. of Edinburgh, 1968.

[Burstall 1969] R. Burstall, Proving properties of programs by structural induction, Computer J. 12(1):41-48, 1969.

[Burstall 1970] R.M. Burstall, Formalising semantics of first order logic in first order logic, and application to planning for robots, MIP-R-73, Dept. of Machine Intelligence, Univ. of Edinburgh, Edinburgh, March 1970.

[Burstall 1986] R.M. Burstall, Research in interactive theorem proving at Edinburgh University, ECS-LFCS-86-12, Laboratory for Foundations of Computer Science, Univ. of Edinburgh, Edinburgh, 1986; also published as CSR-218-86.

[Burstall 1987] R.M. Burstall, P. Taylor, C. Jones, Interactive proof editing with the Edinburgh IPE, course organised by the Laboratory for Foundations of Computer Science, Univ. of Edinburgh, 1987.

[Buss 1987] S.R. Buss, Polynomial size proofs of the propositional pigeonhole principle, J. of Symbolic Logic 52(4):916-927, 1987.

[Butler 1980] G. Butler, D. Lankford, Experiments with computer implementations of procedures which often derive decision algorithms for the word problem in abstract algebras, Memo MTP-7, Math. Dept., Louisiana Tech. Univ., Ruston, LA, August 1980.

[Butler 1986] R. Butler, E. Lusk, W. McCune, R. Overbeek, Paths to high-performance automated theorem proving, 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. 588-597.

*[Butler 1988a] R.M. Butler, R. Loganantharaj, R. Olson, Notes on Prolog program transformations, Prolog style, and efficient compilation to the Warren abstract machine, 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. 323-332.

*[Butler 1988] R.M. Butler, N.T. Karonis, Exploitation of parallelism in prototypical deduction problems, 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. 333-343.

*[Butler 1990] R. Butler, I. Foster, A. Jindal, R. Overbeek, 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. 649-650.

[Buttner 1985] W. Buttner, Unification in data structure multisets, Report, Siemens AG, Corporate Laboratories for Information Technology, Munchen, 1985; also SEKI-Report Memo SEKI-85-V-KL, Fachbereich Informatik, Universitat Kaiserslautern, 1985; also J. of Automated Reasoning 2(1):75-88, D. Reidel Publ. Co., Dordrecht, Holland, 1986.

[Buttner 1986a] W. Buttner, Unification in data structure sets, 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. 470-488.

*[Buttner 1986b] W. Buttner, H. Simonis, Embedding Boolean expressions into logic programming, preprint, Siemens AG, Munchen, 1986; also J. of Symbolic Computation 4(2):191-205, October 1987.

*[Buttner 1988] W. Buttner, Unification in finite algebras in unitary, 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. 368-377.


URL: http://www.oracanada.com/biblio/biblio-prover-a-b.html
Revised: July 31, 1998