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 (CADE9, Argonne, Illinois, 2326 May 1988),
ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag, Berlin,
1988, pp. 218237.
[Aandreaa 1963] S. Aandreaa, P. Andrews, B. Dreben, False lemmas
in Herbrand, Bull. of the American Math. Soc. 68(1963):699706.
[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 STANCS851056, Dept. of Computer Science, Stanford Univ.,
Stanford, CA, 1985; also Logics of Programs, ed. R. Parikh, LNCS
193, SpringerVerlag, Berlin, 1985, pp. 115.
[Abadi 1986a] M. Abadi, Z. Manna, Modal theorem proving,
STANCS861101, Dept. of Computer Science, Stanford Univ., May
1986; also Proc. 8th Intl. Conf. on Automated Deduction (CADE8,
Oxford, England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS
230, SpringerVerlag, Berlin, 1986, pp. 172189.
[Abadi 1986b] M. Abadi, Z. Manna, A timely resolution,
STANCS861106, Dept. of Computer Science, Stanford Univ., April
1986.
[Abadi 1987] M. Abadi, Temporallogic theorem proving,
STANCS871151, Stanford Univ. Computer Science Dept., CA, March
1987.
[Abadi 1990] M. Abadi, Z. Manna, Nonclausal deduction in
firstorder temporal logic, JACM 37(2):279317, 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. AAAI84,
Natl Conf. on Artificial Intelligence, Univ. of Texas at Austin,
610 August 1984, pp. 15.
*[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, 35 April 1989), ed. N. Dershowitz, SpringerVerlag, NY,
1989, pp. 530532.
[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
proofchecker for certain axiomatic systems, SRIMEMO41, 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. 137160.
[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, ACunification race: the system
solving approach, implementation and benchmarks, Research Report
89R169, CRIN, Nancy, France, 1989.
*[Adi 1990] M. Adi, C. Kirchner, ACunification race: The system
solving approach and its implementation, Proc. Intl. Symp. on
Design and Implementation of Symbolic Computation Systems (DISCO
'90, Capri, Italy 1012 April 1990), LNCS 429, ed. A Miola,
SpringerVerlag, 1990, pp. 174183.
[Agnarsson 1984] S. Agnarsson, A. KandriRody, D. Kapur, D.
Narendran, B.D. Saunders, Complexity of testing whether a
polynomial ideal is nontrivial, Proc. 1984 MACSYMA Users' Conf.,
Schenectady, NY, July 1984, pp. 452458.
[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. 18.
[Aiello 1977a] L.M. Aiello, R.W. Weyhrauch, PASCAL in LCF:
Semantics and examples of proof, Theoretical Computer Science
5(2):135178, 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 metatheoretic
reasoning to do algebra, Proc. 5th Conf. on Automated Deduction
(Les Arcs, France, 811 July 1980), ed. W. Bibel and R. Kowalski,
LNCS 87, SpringerVerlag, Berlin, 1980, pp. 113.
*[Aiello 1988] L.M. Aiello, R.W. Weyhrauch, Checking proofs in
the metamathematics of first order logic, In MetaLevel
Architectures and Reflection, ed. P. Maes and D. Nardi,
NorthHolland, Amsterdam, 1988, pp. 118.
[AitKaci 1985a] H. AitKaci, Solving type equations by graph
rewriting, Proc. 1st Conf. Rewriting Techniques and Applications
(Dijon, France, 2022 May 1985), ed. J.P. Jouannaud, LNCS 202,
SpringerVerlag, Berlin, 1985, pp. 158179.
[AitKaci 1985b] H. AitKaci, An algorithm for finding a minimal
recursive path ordering, Theoretical Informatics 19(4): 359382,
1985.
*[AitKaci 1989] H. AitKaci, 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, 47 May 1987.)
[AitKaci 1990] H. AitKaci, The WAM: a (real) tutorial, PRL
Research Report Number 5, Digital Equipment Corporation, Paris
Research Laboratory, RueilMalmaison, France, 1990.
*[AitKaci 1991] H. AitKaci, 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 hyperlinking, Proc. 11th Intl. Conf. on
Automated Deduction (CADE11, Saratoga Springs, NY, USA, June
1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607,
SpringerVerlag, Berlin, 1992, pp. 706710.
[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. 321326; also Automation
of Reasoning  Classical Papers on Computational Logic, Vol. II,
19671970, ed. J. Siekmann and G. Wrightson, SpringerVerlag,
Berlin, 1983, pp. 417434.
*[Allen 1988] P.E. Allen, S. Bose, E.M. Clarke, S. Michaylov,
PARTHENON: A parallel theorem prover for nonHorn clauses, Proc.
9th Intl. Conf. on Automated Deduction (CADE9, Argonne, Illinois,
2326 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310,
SpringerVerlag, Berlin, 1988, pp. 764765.
*[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, 47 June 1990),
IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 95105.
*[Altucher 1990] J.A. Altucher, P. Panangaden, A mechanically
assisted constructive proof in category theory, Proc. 10th Intl.
Conf. on Automated Deduction (CADE10, Kaiserslautern, FRG, July
1990), Lecture Notes in Artificial Intelligence 449, ed. M.E.
Stickel, SpringerVerlag, Berlin, 1990, pp. 500513.
[Amarel 1962] S. Amarel, An approach to problemsolving by
computer, Final Report AFCRL62367, 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. 131171.
[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 IntelligenceTagvung, Wien (2427
September 1985), InformatikFachberichte 106, SpringerVerlag,
Berlin, 1985, pp. 8189.
*[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, 15 August 1988, pp. 613618.
*[Ammon 1992a] K. Ammon, Automatic proofs in mathematical logic
and analysis, Proc. 11th Intl. Conf. on Automated Deduction
(CADE11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur,
Lecture Notes in Artificial Intelligence 607, SpringerVerlag,
Berlin, 1992, pp. 419.
*[Ammon 1992b] K. Ammon, The SHUNYATA system, Proc. 11th Intl.
Conf. on Automated Deduction (CADE11, Saratoga Springs, NY, USA,
June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence
607, SpringerVerlag, Berlin, 1992, pp. 681685.
[Anantharaman 1989a] S. Anantharaman, J. Mzali, Unfailing
completion modulo a set of equations, Research report 470,
LRIOrsay, 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, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 533537.
*[Anantharaman 1990] S. Anantharaman, J. Hsiang, Automated
proofs of the Moufang identities in alternative rings, J. of
Automated Reasoning 6(1):79109, 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 1012 April 1990), LNCS 429, ed. A Miola,
SpringerVerlag, 1990, pp. 184193.
[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
Eresolution, Proc. AFIPS'70, Spring Joint Computer Conf. Vol. 36,
AFIPS Press, Montvale, NJ, 1970, pp. 653656; also Automation Of
Reasoning  Classical Papers On Computational Logic, Vol. II,
19671970, ed. J. Siekmann And G. Wrightson, SpringerVerlag,
Berlin, 1983, pp. 317320.
[Anderson 1970c] R. Anderson, W. Bledsoe, A linear format for
resolution with merging and a new technique for establishing
completeness, JACM 17(July 1970):525534; also Automation Of
Reasoning  Classical Papers On Computational Logic, Vol. II,
19671970, ed. J. Siekmann And G. Wrightson, SpringerVerlag,
Berlin, 1983, pp. 321330.
[Anderson 1970d] D.B. Anderson, An investigation of some clause
indexing schemes, MIPR80, 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):525534.
[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, NorthHolland, Amsterdam, 1965.
[Andrews 1968a] P.B. Andrews, Resolution with merging, JACM
15(3):367381, 1968; also Automation Of Reasoning  Classical
Papers On Computational Logic, Vol. II, 19671970, ed. J. Siekmann
And G. Wrightson, SpringerVerlag, Berlin, 1983, pp. 85101.
[Andrews 1968b] P.B. Andrews, On simplifying the matrix of a
WFF, J. Symbolic Logic 33(2):180192, 1968; also Automation Of
Reasoning  Classical Papers On Computational Logic, Vol. II,
19671970, ed. J. Siekmann And G. Wrightson, SpringerVerlag,
Berlin, 1983, pp. 102116.
[Andrews 1971] P.B. Andrews, Resolution in type theory, J.
Symbolic Logic 36(3):414432, 1971; also Automation Of Reasoning 
Classical Papers On Computational Logic, Vol. II, 19671970, ed.
J. Siekmann And G. Wrightson, SpringerVerlag, Berlin, 1983, pp.
487507.
[Andrews 1972] P.B. Andrews, General models and extensionality,
J. Symbolic Logic 37(2):395397, 1972.
[Andrews 1974] P.B. Andrews, Provability in elementary type
theory, Zeitschrift fur Mathematische Logik und Grundlagen der
Mathematik 20(1974):441418.
[Andrews 1976] P.B Andrews, Refutations by matings, IEEE Trans.
on Computers C25(8):801808, 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 (CADE4, Austin, Texas, 13 February 1979),
ed. W.H. Joyner, 1979, pp. 1925.
[Andrews 1980] P.B. Andrews, Transforming matings into natural
deduction proofs, Proc. 5th Conf. on Automated Deduction (Les
Arcs, France, 811 July 1980), ed. W. Bibel and R. Kowalski, LNCS
87, SpringerVerlag, Berlin, 1980, pp. 281292.
[Andrews 1981] P.B. Andrews, Theorem proving via general
matings, JACM 28(2):193214, April 1981.
[Andrews 1983] P.B. Andrews, D.A. Miller, E.L. Cohen, F.
Pfenning, Automating higherorder logic, Dept. of Math., Univ.
CarnegieMellon, 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. 169192.
[Andrews 1986a] P.B. Andrews, Connections and higherorder
logic, Proc. 8th Intl. Conf. on Automated Deduction (CADE8,
Oxford, England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS
230, SpringerVerlag, Berlin, 1986, pp. 14.
[Andrews 1986b] P.B. Andrews, F. Pfenning, S. Issar, C.P.
Klapper, The TPS Theorem Proving System, Proc. 8th Intl. Conf. on
Automated Deduction (CADE8, Oxford, England, July 27August 1,
1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986,
pp. 663664.
[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 lambdacalculus and automated
mathematics, Mathematical Logic and Theoretical Computer Science,
ed. E.G.K. LopezEscobar, D.W. Kueker, and C.H. Smith, Lecture
Notes in Pure and Applied Mathematics 106, Marcel Dekker, 1987,
114.
*[Andrews 1988] P.B. Andrews, S. Issar, D. Nesmith, F. Pfenning,
The TPS Theorem Proving System, Proc. 9th Intl. Conf. on Automated
Deduction (CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk
and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
760761.
*[Andrews 1989] P.B. Andrews, On connections and higherorder
logic, J. Automated Reasoning 5(3):257291, 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 (CADE10, Kaiserslautern, FRG, July 1990),
Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel,
SpringerVerlag, Berlin, 1990, pp. 641642.
*[Andrews 1991] P.B. Andrews, More on the problem of finding a
mapping between clause representation and naturaldeduction
representation, J. of Automated Reasoning 7(2):285286, June 1991.
[Andreka 1991] H. Andreka, I. Nemeti, Sain, I., On the strength
of temporal proofs, Theor. Comput. Sci. 80(2):125151, March 1991.
[Antoniou 1983] G. Antoniou, H.J. Ohlbach, TERMINATOR, Proc. 8th
IJCAI, Karlsruhe, W. Germany, August 1983, pp. 916919.
[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. 2329, 1966.
*[Aponte 1984] M.V. Aponte, J.A. Fernandez, P. Roussel, Editing
firstorder proofs: Programmed rules vs. derived rules, Proc. 1984
Intl. Symp. on Logic Programming, Atlantic City, New Jersey, 69
February 1984, pp. 9298.
[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. 431436.
*[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(13):3760,
December 1988.
[Arnon 1988] D. Arnon; M. Mignotte, On mechanical quantifier
elimination for elementary algebra and geometry, J. Symb. Com.
5(1988):237259.
[Aronson 1980] A.R. Aronson, B.E. Jacabs, J. Minker, A note on
fuzzy deduction, JACM 27(4):599607, October 1980.
*[Arora 1992] S. Arora, S. Safra, Probabilistic checking of
proofs, Proc. 33rd Annual Symp. on Foundations of Computer Science
(Pittsburgh, PA, October 2427, 1992), IEEE Computer Society
Press, Los Alamitos, CA, 1992, pp. 213.
*[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 2427, 1992), IEEE Computer
Society Press, Los Alamitos, CA, 1992, pp. 1423.
[Ashcroft 1976] E.A. Ashcroft, W.W. Wadge, Lucid  A formal
system for writing and proving programs, SIAM J. on Computing
5(3):336354, September 1976.
*[Aspetsberger 1985] K. Aspetsberger, Substitution expression:
extracting solutions of nonHorn clause proofs, Proc. European
Conf. on Computer Algebra (EUROCAL '85, Linz, Austria, 13 April
1985), Vol. 2: Research Contributions, ed. B.F. Caviness, LNCS
204, SpringerVerlag, Berlin, pp. 7886.
[Aspvall 1979] B.Aspvall, M.R. Plass, R.E. Tajan, A lineartime
algorithm for testing the truth of certain quantified boolean
formulas, Information Processing Letters 8(1979):121123.
*[Astesiano 1989] E. Astesiano, M. Wirsing, Bisimulation in
algebraic specifications, In: Resolution of Equations in Algebraic
Structures: Vol 1, Algebraic Techniques, ed. H. AitKaci and M.
Nivat, Academic Press, Inc., San Diego, 1989, pp. 131.
*[Astrachan 1992] O.W. Astrachan, M.E. Stickel, Caching and
lemmaizing in model elimination theorem provers, Proc. 11th Intl.
Conf. on Automated Deduction (CADE11, Saratoga Springs, NY, USA,
June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence
607, SpringerVerlag, Berlin, 1992, pp. 224238.
[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. 197208.
[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):329345.
[Aubin 1979b] R. Aubin, Mechanizing structural induction II:
Strategies, Theor. Comput. Sci. 9(2):347362, October 1979.
[Auffray 1988] Y. Auffray, P. Enjalbert, Modal theorem proving
using equational methods, Tech. Report 8811, 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,
2025 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp.
441445.
*[Auffray 1990] Y. Auffray, P. Enjalbert, J.J. Hebrard,
Strategies for modal resolution: Results and problems, J. of
Automated Reasoning 6(1):138, March 1990.
*[Augustsson 1985] L. Augustsson, Compiling pattern matching,
Proc. Functional Programming Languages and Computer Architecture
(Nancy, France, 1619 September 1985), ed. J.P. Jouannaud, LNCS
201, SpringerVerlag, Berlin, pp. 368381.
[Avenhaus 1984] J. Avenhaus, On the termination of the
KnuthBendix 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):109122, 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
(CADE8, Oxford, England, July 27August 1, 1986), ed. J.H.
Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp. 665667.
*[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, 810 July 1987), ed. S.
Kaplan and J.P. Jouannaud, LNCS 308, SpringerVerlag, Berlin,
1988, pp. 245248.
*[Avenhaus 1989a] J. Avenhaus, J. Denzinger, J. Muller,
THEOPOGLES  An efficient theorem prover based on
rewritetechniques, Proc. 3rd Intl. Conf. Rewriting Techniques and
Applications (Chapel Hill, North Carolina, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 538541.
*[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, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 542546.
*[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. 143.
[Avron 1987a] Arnon Avron, Simple consequence relations, Tech.
Report ECSLFCS8730, 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 ECSLFCS8731, 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, SpringerVerlag, NY, 1989, pp. 323340.
*[Azzoune 1988] H. Azzoune, Type inference in Prolog, Proc. 9th
Intl. Conf. on Automated Deduction (CADE9, Argonne, Illinois,
2326 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310,
SpringerVerlag, Berlin, 1988, pp. 258277.
[Baader 1986] F. Baader, The theory of idempotent semigroups is
of unification type zero, J. Automated Reasoning 2(3):283286,
September 1986.
*[Baader 1989a] F. Baader, Characterizations of unification type
zero, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications
(Chapel Hill, North Carolina, 35 April 1989), ed. N. Dershowitz,
SpringerVerlag, NY, 1989, pp. 214.
[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
(CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes in
Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, pp. 396410.
*[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 (CADE11, Saratoga
Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in
Artificial Intelligence 607, SpringerVerlag, Berlin, 1992, pp.
5065.
[Baader 1993] R. Baader, K.U. Schulz, Combination techniques and
decision problems for disunification, Research report
CISRep9365, 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, 25 June 1987), ed. J.H.
Davenport, LNCS 378, SpringerVerlag, Berlin, 1989, pp. 424425.
*[Baaz 1990] M. Baaz, A. Leitsh, A strong problem reduction
method based on function introduction, Proc. ISSAC '90 (Tokyo,
Japan, 2024 August 1990), ACM, NY, NY, 1990, p. 3037.
[Bachmair 1980] L. Bachmair, B. Buchberger, A simplified proof
of the characterization theorem for Grobner bases, ACM SIGSAM Bull
14(4):2934, 1980.
[Bachmair 1982a] L. Bachmair, Implementation of the NelsonOppen
method for combining decision procedures: Implementation guide,
CAMP 8217.0, ComputerAided Mathematical Problem Solving at the
Univ. of Linz, Austria, 1982.
[Bachmair 1982b] L. Bachmair, The NelsonOppen method of
combining special theorem provers: Implementation and application
to program verification, CAMP 8218.0, ComputerAided Mathematical
Problem Solving at the Univ. of Linz, Austria, 1982.
[Bachmair 1984] L. Bachmair, D.A. Plaisted, Termination
orderings for associativecommutative rewriting systems, Report
UIUCDCSR841179, Dept. of Computer Science, Univ. of Illinois at
UrbanaChampaign, December 1984.
[Bachmair 1985a] L. Bachmair, D.A. Plaisted, Associative path
orderings, Proc. 1st Conf. Rewriting Techniques and Applications
(Dijon, France, 2022 May 1985), ed. J.P. Jouannaud, LNCS 202,
SpringerVerlag, Berlin, 1985, pp. 241254; also J. of Symbolic
Computation 1(4):329349, December 1985.
[Bachmair 1985b] L. Bachmair, N. Dershowitz, Critical pair
criteria for the KnuthBendix completion method, Dept. of Computer
Science, Univ. of Illinois, UrbanaChampaign, 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 (CADE8,
Oxford, England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS
230, SpringerVerlag, Berlin, 1986, pp. 520.
[Bachmair 1986a] L. Bachmair, N. Dershowitz, and J. Hsiang,
Orderings for equational proofs, Proc. IEEE Symp. on Logic in
Computer Science, Cambridge, MA, 1618 June 1986, pp. 346357.
[Bachmair 1986b] L. Bachmair, N. Dershowitz, Rewriting modulo a
congruence (in preparation), Univ. of Illinois, 1986.
*[Bachmair 1986c] L. Bachmair, N. Dershowitz, Criticalpair
criteria for the KnuthBendix completion procedure, Proc. 1986
ACMSIGSAM Symp. on Symbolic and Algebraic Computation (SYMSAC
'86, Univ. of Waterloo, Waterloo, Ontario, 2123 July 1986), ed.
B.W. Char, ACM, New York, NY, 1986, pp. 215217.
[Bachmair 1987a] L. Bachmair, N. Dershowitz, Inference rules for
rewritebased firstorder theorem proving, Proc. 2nd Annual IEEE
Symp. on Logic in Computer Science, Ithaca, NY, 2225 June 1987,
pp. 331337.
[Bachmair 1987b] L. Bachmair, N. Dershowitz, Completion for
rewriting modulo a congruence, Proc. 2nd Intl. Conf. on Rewriting
Techniques and Applications (Bordeaux, France, 2527 May 1987),
ed. P. Lescanne, LNCS 256, SpringerVerlag, Berlin, 1987, pp.
192203; also Theoretical Computer Science 67(2&3):173202,
October 1989.
[Bachmair 1987c] L. Bachmair, Proof methods for equational
theories, PhD thesis, Univ. of Illinois at UrbanaChampaign,
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, 25 June 1987),
ed. J.H. Davenport, LNCS 378, SpringerVerlag, Berlin, 1989, pp.
452453.
*[Bachmair 1988a] L. Bachmair, Proof by consistency in
equational theories, Proc. 3rd Annual Symp. on Logic in Computer
Science (Edinburgh, Scotland, 58 July 1988), IEEE, 1988, pp.
228233.
*[Bachmair 1988b] L. Bachmair, N. Dershowitz, Critical pair
criteria for completion, J. of Symbolic Computation 6(1):118,
August 1988.
*[Bachmair 1989a] L. Bachmair, Proof normalization for
resolution and paramodulation, Proc. 3rd Intl. Conf. Rewriting
Techniques and Applications (Chapel Hill, North Carolina, 35
April 1989), ed. N. Dershowitz, SpringerVerlag, NY, 1989, pp.
1528.
*[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.
AitKaci and M. Nivat, Academic Press, Inc., San Diego, 1989, pp.
130.
*[Bachmair 1990] L. Bachmair, H. Ganzinger,, On restrictions of
ordered paramodulation with simplification, Proc. 10th Intl. Conf.
on Automated Deduction (CADE10, Kaiserslautern, FRG, July 1990),
Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel,
SpringerVerlag, Berlin, 1990, pp. 427441.
*[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 (CADE11, Saratoga Springs, NY, USA, June
1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607,
SpringerVerlag, Berlin, 1992, pp. 462476.
*[Bachmair 1993] L Bachmair, Rewrite techniques in theorem
proving, Proc. 5th Intl. Conf, RTA93 (Montreal, Canada, June
1993), LNCS 690, ed. C. Kirchner, SpringerVerlag, 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
MartinLof'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 CSR8407, 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, 2527 May
1987), ed. P. Lescanne, LNCS 256, SpringerVerlag, Berlin, 1987,
pp. 8394.
*[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, 810 July
1987), ed. S. Kaplan and J.P. Jouannaud, LNCS 308,
SpringerVerlag, Berlin, 1988, pp. 314.
*[Baeten 1988b] J.C.M. Baeten, J.A. Bergstra, J.W. Klop, W.P.
Weijland, Term rewriting systems with rule priorities, Report
CSR8815, 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
ENstrategy, Proc. Intl. Symp. on Design and Implementation of
Symbolic Computation Systems (DISCO '90, Capri, Italy 1012 April
1990), LNCS 429, ed. A Miola, SpringerVerlag, 1990, pp. 278279.
*[Bailin 1988] S.C. Bailin, A lambdaunifiability test for set
theory, J. Automated Reasoning 4(3):269286, September 1988.
[Bailin 1990] S.C. Bailin, D. BarkerPlummer, Automated
deduction in set theory, Final Report NSF/ISI90006, 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 MissouriRolla, 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, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 2944.
[Baker 1992] S. Baker, A. Ireland, A. Smaill, On the use of the
constructive Omegarule 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, SpringerVerlag, 1992, pp. 214225.
[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, Semiautomated
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
ATP7, 1973.
[Ballantyne 1975a] M. Ballantyne, Computer generation of
counterexamples in topology, Univ. of Texas at Austin, Math. Dept.
Memo ATP24, 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 nonstandard techniques,
ATP23, Univ. of Texas at Austin; also JACM 24(3):353374, 1977.
[Ballantyne 1979] A.M. Ballantyne, D.S. Lankford, New decision
algorithms for finitely presented commutative semigroups, MTP4,
Dept. of Math., Louisiana Tech. Univ., May 1979; also J. Comput.
Math. with Appl. 7(1981):159165.
[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. 339.
[Ballard 1986] D. Ballard, Parallel logical inference and energy
minimization, Proc. AAAI86, 5th Natl Conf. on Artificial
Intelligence (Philadelphia, PA, 1115 August 1986), pp. 203208.
[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
wellfounded semantics for logic programs, Proc. 10th Intl. Conf.
on Automated Deduction (CADE10, Kaiserslautern, FRG, July 1990),
Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel,
SpringerVerlag, Berlin, 1990, pp. 102116.
*[BarkerPLummer 1992a] D. BarkerPlummer, S.C. Bailin,
Graphical theorem proving: an approach to reasoning with the help
of diagrams, Proc. 10th ECAI (ECAI 92, Vienna, Austria, 37 August
1992), ed. B. Neumann, John Wiley & Sons, Chichester, 1992,
pp. 5559.
*[BarkerPLummer 1992b] D. BarkerPlummer, S.C. Bailin, A.S.
Merrill, &: Automated natural deduction, Proc. 11th Intl.
Conf. on Automated Deduction (CADE11, Saratoga Springs, NY, USA,
June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence
607, SpringerVerlag, Berlin, 1992, pp. 716720.
*[BarkerPLummer 1992b] D. BarkerPlummer, A. Rothenberg, The
GAZER theorem prover, Proc. 11th Intl. Conf. on Automated
Deduction (CADE11, Saratoga Springs, NY, USA, June 1992), ed. D.
Kapur, Lecture Notes in Artificial Intelligence 607,
SpringerVerlag, Berlin, 1992, pp. 726730.
[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.
301318.
[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 (CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk
and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
101110.
[Basin 1989] D. Basin, Generalized rewriting in type theory,
Tech. Report 891031, Cornell Univ., Computer Science Dept., 1989.
*[Basin 1990] D.A. Basin, Equality of terms containing
associativecommutative 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,
SpringerVerlag, Berlin, 1990, pp. 251260.
[Basin 1991] D.A. Basin, M. Kaufmann, The BoyerMoore prover and
Nuprl: An experimental comparison, In Logical Frameworks,
Cambridge University Press, 1991, pp. 89119.
*[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 (CADE11,
Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes
in Artificial Intelligence 607, SpringerVerlag, Berlin, 1992, pp.
295309.
*[Basin 1993a] D.A. Basin, T. Walsh, Difference unification,
Proc. 13th IJCAI (Chambery, France, 28 August3 September 1993),
Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 116122.
[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):113136,
January 1985.
[Bates 1986] J.L. Bates, The PRL mathematics environment: A
knowledge based medium (extended abstract), Tech. Report 86768,
Dept. of Computer Science, Cornell Univ., 1986.
[Bauderon 1986] M. Bauderon, B. Courcelle, Graph Expressions and
Graph Rewritings, Rapport interne no. I8623, 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:1720, 1973.
[Bauer 1984] G. Bauer, F. Otto, Finite complete rewriting
systems and the complexity of the word problem, Acta Informatica
21(1984):521540.
[Bauer 1985] G. Bauer, Nlevel rewriting systems, Theoret.
Comput. Sci. 40(23):8599, 1985.
*[Bauer 1992] M. Bauer, An intervalbased temporal logic in a
multivalued setting, Proc. 11th Intl. Conf. on Automated Deduction
(CADE11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur,
Lecture Notes in Artificial Intelligence 607, SpringerVerlag,
Berlin, 1992, pp. 355369.
[Baxter 1973] L.D. Baxter, An efficient unification algorithm,
Tech. Report CS7323, 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 CS7613, Dept. Computer Science, Univ. of
Waterloo, Waterloo, Ontario, Canada, 1976.
[Baxter 1977] L.D. Baxter, The complexity of unification,
Internal Report CS7725, 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 (CADE8, Oxford,
England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS 230,
SpringerVerlag, Berlin, 1986, pp. 668669.
[Bayerl 1986b] S. Bayerl, F. Kurfess, R. Letz, J. Schumann,
PROTHEO/2; sequential PROLOGlike 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 PROLOGlike theorem prover based
on the connection method, Proc. 2nd Intl. Conf. on Artificial
Intelligence: Methodology, Systems, Applications (AIMSA'86, Varna,
Bulgaria, 1619 September 1986), ed. P. Jorrand and V. Sgurev,
NorthHolland, Amsterdam, 1987, pp. 2936.
*[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,
1619 September 1986), ed. P. Jorrand and V. Sgurev,
NorthHolland, Amsterdam, 1987, pp. 2128.
[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 (CADE11, Saratoga Springs, NY,
USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial
Intelligence 607, SpringerVerlag, Berlin, 1992, pp. 507521.
*[Beckert 1992b] B. Beckert, S. Gerberding, R. Hahnel, W.
Kernig, The tableaubased theorem prover 3TAP for muliplevalued
logics, Proc. 11th Intl. Conf. on Automated Deduction (CADE11,
Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes
in Artificial Intelligence 607, SpringerVerlag, Berlin, 1992,
pp.758760.
[Beeson 1981] M.J. Beeson, Formalizing constructive mathematics,
why and how? in Constructive Mathematics, ed. F. Richman, Lecture
Notes in Mathematics, SpringerVerlag, NY, 1981, pp. 146190.
[Beeson 1983] M.J. Beeson, Proving programs and programming
proofs, In Intl. Congress on Logic, Methodology and Philosophy of
Science (Salzbury, Austria), NorthHolland, Amsterdam, 1983.
[Beeson 1985] M.J. Beeson, Foundations of Contructive
Mathematics, SpringerVerlag, NY, 1985.
[Beetz 1987] M. Beetz, Specifying metalevel architectures for
rulebased systems, SEKI Report SR8706, Universitat
Kaiserslautern, Fachbereich Informatik, Kaiserslautern, 1987.
*[Beetz 1988] M. Beetz, H. Freitag, J. Klug, The MKRP user
manual (ed. Christoph Lingenfelder), SEKI Working Paper SWP8801,
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 (CADE8, Oxford, England, July 27August 1,
1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986,
pp. 670671.
*[Belleannee 1990] C. Belleannee, Improving deduction in a
sequent calculus, Proc. 8th Biennial Conf. of the Canadian Society
for Computational Studies of Intelligence (CSCSI90, Univ. of
Ottawa, Ottawa, Canada, 2225 May 1990), published by CSCSI, 1990,
pp. 220226.
*[Bellegarde 1987] F. Bellegarde, P. Lescanne, Transformation
ordering, Proc. Intl. Joint Conf. on Theory and Practice of
Software Development (TAPSOFT'87, Pisa, Italy, 2327 March 1987),
Vol. I, ed. H. Ehrig, R. Kowalski, G. Levi, and U. Montanari, LNCS
249, SpringerVerlag, Berlin, 1987, pp. 6980.
[Bellin 1990] G. Bellin, Mechanizing proof theory:
Resourceaware logics and proof transformations to extract
implicit information, STANCS901319, Dept. of Computer Science,
Stanford Univ., June 1990.
[BenAri 1980] M. BenAri, A simplified proof that regular
resolution is exponential, Information Processing Letters
10(1980):9698.
[BenAri 1981] M. BenAri, Complexity of proofs and models in
programming logics, PhD, TelAviv Univ., May 1981.
[Benanav 1985] D. Benanav, D. Kapur, P. Narendran, Complexity of
matching problems, Proc. 1st Conf. Rewriting Techniques and
Applications (Dijon, France, 2022 May 1985), ed. J.P. Jouannaud,
LNCS 202, SpringerVerlag, Berlin, 1985, pp. 417479; J. of
Symbolic Computation 3(1 and 2):203216, 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, 2025 August 1989), ed. N.S. Sridharan,
IJCAI Inc., 1989, pp. 366371.
*[Benanav 1990] D. Benanav, Simultaneous paramodulation, Proc.
10th Intl. Conf. on Automated Deduction (CADE10, Kaiserslautern,
FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed.
M.E. Stickel, SpringerVerlag, Berlin, 1990, pp. 442455.
[BenCherifa 1987] A. BenCherifa, P. Lescanne, Termination of
rewriting systems by polynomial interpretations and its
implementation, Science of Computer Programming 9(2):137159,
1987.
*[Benhamou 1992] B. Benhamou, L. Sais, Theoretical study of
symmetries in propositional calculus and applications, Proc. 11th
Intl. Conf. on Automated Deduction (CADE11, Saratoga Springs, NY,
USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial
Intelligence 607, SpringerVerlag, Berlin, 1992, pp. 281294.
[Bennett 1963] J.H. Bennett, W.B. Easton, J.R. Guard, T.H. Mott,
Introduction to semiautomated mathematics, AFCRL 63180, Air
Force Cambridge Res. Lab., Cambridge, MA, April 1963.
[Bennett 1964a] J.H. Bennett, W.B. Easton, A. Guard, T.H. Mott,
Toward semiautomated mathematics: The language and logic of SAM
III, Sci. Rep. 2, AFCRL 64562, Air Force Cambridge Res. Lab.,
Cambridge, MA, May 1964.
[Bennett 1964b] J.H. Bennett, W.B. Easton, J.R. Guard, T.H.
Mott, Semiautomated mathematics: SAM IV, Sci. Rep. 3, AFCRL
64827, Air Force Cambridge Res. Lab., Cambridge, MA, October
1964.
[Bennett 1967] J.H. Bennett, W.B. Easton, J.R. Guard, L.G.
Settle, CRTaided semiautomated mathematics, Final Report, AFCRL
67017, 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 ATP7, Dept. Math.
Univ. of Texas at Austin, 1973.
*[Benninghofen 1987] B. Benninghofen, S. Kemmerich, M.M.
Richter, eds., Systems of Reductions, LNCS 277, SpringerVerlag,
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, 2527 May 1987),
ed. P. Lescanne, LNCS 256, SpringerVerlag, Berlin, 1987, pp.
121132.
*[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):323362, June 1986.
[Bergstra 1987] J.A. Bergstra, J. Heering, P. Klint, ASF  an
algebrai specification formalism, Report CSR8705, 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, PROSPECTRAProject, U. Dortmund, 1987.
*[Bertling 1988b] H. Bertling, H. Ganzinger, R. Schafers, CEC: A
system for conditional equational specifications,
PROSPECTRAReport M.1.3R7.0, Universitat Dortmund, 1988; also
Proc. 1st Intl. Workshop on Conditional Term Rewriting Systems
(Orsay, France, 810 July 1987), ed. S. Kaplan and J.P.
Jouannaud, LNCS 308, SpringerVerlag, Berlin, 1988, pp. 249250.
[Bertling 1988c] H. Bertling, H. Ganzinger, R. Schaefers, CEC: A
system for conditional equational specifications: User Manual
(Version 1.4), PROSPECTRAReport M.a.3R7.0, U. Dortmund, West
Germany, 1988.
[Bertling 1988c] H. Bertling, H. Ganzinger, R. Schafers, A
collection of specifications completed by the CECsystem, Report,
PROSPECTRAProject, U. Dortmund, 1988.
*[Bertling 1989a] H. Bertling, H. Ganzinger, Completiontime
optimization of rewritetime goal solving, Proc. 3rd Intl. Conf.
Rewriting Techniques and Applications (Chapel Hill, North
Carolina, 35 April 1989), ed. N. Dershowitz, SpringerVerlag, NY,
1989, pp. 4558.
[Bertling 1989b] H. Bertling, H. Ganzinger, Completion of
applicationrestricted equations, Report 289, FB Informatik, U.
Dortmund, 1989. [Besnard 1983a] P. Besnard, A proof procedure for
a nonmonotonic 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.
2730.
*[Besnard 1988] P. Besnard, P. Siegal, Suppositionbased logic
for automated nonmonotonic reasoning, Proc. 9th Intl. Conf. on
Automated Deduction (CADE9, Argonne, Illinois, 2326 May 1988),
ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag, Berlin,
1988, pp. 592601.
[Beth 1959] E.W. Beth, The Foundations of Mathematics,
NorthHolland, 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, NorthHolland, Amsterdam,
1963, pp. 2132.
[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, 19571966, ed. J. Siekmann and G. Wrightson,
SpringerVerlag, Berlin, 1983, pp. 7990.
*[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):411428, December 1989.
*[Bevier 1989b] W.R. Bevier, Kit and the short stack, J.
Automated Reasoning 5(4):519530, December 1989.
*[Bezem 1988] M. Bezem, Consistency of rulebased expert
systems, Proc. 9th Intl. Conf. on Automated Deduction (CADE9,
Argonne, Illinois, 2326 May 1988), ed. E. Lusk and R. Overbeek,
LNCS 310, SpringerVerlag, Berlin, 1988, pp. 151161.
[Bibel 1974] W. Bibel, An approach to a systematic
theoremproving procedure in firstorder logic, Computing
12(1974):4355.
[Bibel 1975] W. Bibel, J. Schreiber, Proof search in a
Gentzenlike system of firstorder logic, Proc. Intl. Computing
Symp., ed. E. Gelenbe and D. Potier, NorthHolland, Amsterdam,
1975, pp. 205212.
[Bibel 1977a] W. Bibel, A syntactic connection between proof
procedures and refutation procedures, GI3. Fachtagung
Theoretische Informatik, LNCS 48, SpringerVerlag, Berlin, 1977,
pp. 215225.
[Bibel 1977b] W. Bibel, Tautology testing with an improved
matrix reduction, Research report TUMINFO7706, 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):3144.
*[Bibel 1980a] W. Bibel, R. Kowalski, eds., Proc. 5th Conf. on
Automated Deduction (Les Arcs, France, 811 July 1980), ed. W.
Bibel and R. Kowalski, LNCS 87, SpringerVerlag, Berlin, 1980.
[Bibel 1980b] W. Bibel, The complete theoretical basis for the
systematic proof method, Technische Universitat Munchen, Bericht
ATP6XII80, 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,
SpringerVerlag, Berlin, 1980, pp. 154167.
[Bibel 1980d] W. Bibel, A strong completeness result for the
connection graph proof procedure, Bericht ATP3IV80, Institut
fur Informatic, Technische Universitat, Munchen, 1980.
[Bibel 1981a] W. Bibel, On matrices with connections, JACM
28(4):633645, October 1981.
[Bibel 1981b] W. Bibel, Mating in matrices, Proc. GWAI81,
InformatikFachberichte 47, ed. Siekmann, SpringerVerlag, Berlin,
1981, pp. 171187, revised in Research Contributions, Artificials
Intelligence and Language Processing, ed. C. Montgomery and F.
Fosdick, CACM 26(11):844852, November 1983.
[Bibel 1981c] W. Bibel, On the completeness of connection graph
resolution, Proc. GWAI81, InformatikFachberichte 47, ed. J.H.
Siekmann, SpringerVerlag, Berlin, 1981, pp. 246247.
*[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):269293, May 1982.
[Bibel 1982c] W. Bibel, Computationally imporved versions of
Herbrand's Theorem, Proc. of the Hebrand Symp., Logic Colloquium
'81, ed. J. Stern, NorthHolland Publishing, 1982, pp. 1128.
[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. 920922.
[Bibel 1984] W. Bibel, B. Buchberger, Towards a connection
machine for logical inference, Future Generations Computer Systems
1(19841985):177185.
[Bibel 1985a] W. Bibel, Automated inferencing, J. of Symbolic
Computation 1(3):245260, September 1985.
[Bibel 1985b] W. Bibel, K. Aspetsberger, A bibliography on
parallel inference machines, J. of Symbolic Computation 1:115118,
1985.
*[Bibel 1985c] W. Bibel, B. Buchberger, Towards a connection
machine for logical inference, FGCS 1(3):177185, 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,
SpringerVerlag, Berlin, 1986, pp. 171220. [Bibel 1986b] W.
Bibel, A deductive solution for plan generation, New Generation
Computing 4:115132, 1986.
[Bibel 1987a] W. Bibel, R. Letz, J. Schumann, Bottomup
enhancements of deductive systems, MS, Technische Universitat
Munchen, 1987; also AI and Robotics, ed. I. Plander,
NorthHolland, Amsterdam (to appear).
[Bibel 1987b] W. Bibel, F. Kurfess, et al., Parallel inference
machines, Bericht Nr. ATP68II.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, 610 June 1988), ed.
R. Goebel, Univ. of Alberta Printing Services, 1988, pp. 16.
[Bibel 1988b] W. Bibel, Advanced topics in automated deduction,
In: Fundamentals of Artificial Intelligence II, ed. R. Nossum,
Springer, Berlin, 1988, pp. 4159.
*[Bibel 1990a] W. Bibel, Perspectives on automated deduction,
Proc. 10th Intl. Conf. on Automated Deduction (CADE10,
Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial
Intelligence 449, ed. M.E. Stickel, SpringerVerlag, Berlin, 1990,
p. 426.
*[Bibel 1990b] W. Bibel, Short proofs of the pigeonhole formulas
based on the connection method, J. of Automated Reasoning
6(3):287297, September 1990.
[Bibel 1991] W. Bibel, S. Holldobler, J. Wurtz, Cycle
unification, Forschungsbericht AIDA9115, TH Darmstadt, August
1991.
*[Bibel 1992] W. Bibel, S. Holldobler, J. Wurtz, Cycle
Unification, Proc. 11th Intl. Conf. on Automated Deduction
(CADE11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur,
Lecture Notes in Artificial Intelligence 607, SpringerVerlag,
Berlin, 1992, pp. 94108.
[Bidoit 1982] M. Bidoit, Proofs by induction in 'fairly'
specified equational theories, Proc. GWAI82,
InformatikFachberichte 58, ed. Wahlster, SpringerVerlag, Berlin,
1982, pp. 154166.
[Bidoit 1983] M. Bidoit, J. Corbin, A rehabilitation of
Robinson's unification algorithm, Information Processing 83, ed.
R.E.A. Pavon, NorthHolland, 1983, pp. 909914.
[Bidoit 1985] M. Bidoit, C. Choppy, ASSPEGIQUE: An integrated
environment for algebraic specifications, Proc. TAPSOFT '85: Coll.
on Software Engineering, LNCS 186, SpringerVerlag, Berlin, 1986,
pp. 246260.
*[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, 810 July 1987), ed. S. Kaplan
and J.P. Jouannaud, LNCS 308, SpringerVerlag, Berlin, 1988, pp.
251252.
*[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, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, 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 (CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk
and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
762763.
[Bing 1969] K. Bing, Natural deduction with few restrictions on
variables, Inf. Sciences 1(4):381402, October 1969.
[Binkley 1968] R.W. Binkley, R.L. Clark, A cancellation
algorithm for elementary logic, Theoria 33(1967):7997, corrected
in Theoria, 1968; also Automation Of Reasoning  Classical Papers
On Computational Logic, Vol. II, 19671970, ed. J. Siekmann And G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 2747.
*[Birkhoff 1989] G. Birkhoff, Rewriting ideas from universal
algebra (abstract), Proc. 3rd Intl. Conf. Rewriting Techniques and
Applications (Chapel Hill, North Carolina, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, 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 (CADE8, Oxford, England, July 27August 1,
1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986,
pp. 672674.
*[Biundo 1987] S. Biundo, A synthesis system mechanizing proofs
by induction, Proc. 7th European Conf. on Artificial Intelligence
(EDAI86, Brighton, U.K., 2025 July 1986), In Advances in
Artificial Intelligence  II, ed. B. du Boulay, D. Hogg, and L.
Steels, NorthHolland, Amsterdam, 1987, pp. 287296.
*[Biundo 1988] S. Biundo, Automated synthesis of recursive
algorithms as a theorem proving tool, Proc. 8th ECAI, Institut fur
Informatik der Technischen Universitat Munchen, 15 August 1988,
pp. 553558.
*[Blackburn 1992] K. Blackburn, A report on ICL HOL, Proc. 11th
Intl. Conf. on Automated Deduction (CADE11, Saratoga Springs, NY,
USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial
Intelligence 607, SpringerVerlag, Berlin, 1992, pp. 743747.
[Blaine 1981] L. Blaine, Programs for structured proofs, In
UniversityLevel ComputerAssisted Instruction at Stanford:
19681980, ed. P. Suppes, IMSSS Stanford Univ., pp. 81119, 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. 511518.
[Blasius 1983a] K. Blasius, Equality reasoning in clause
graphics, Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, pp.
936939.
[Blasius 1983b] K.H. Blasius, Equality reasoning based on
graphs, Tech. Report SR8701, 1987.
[Blasius 1985] K.H. Blasius, Equality reasoning with equality
paths, Proc. GWAI85, 9th German Workshop on Artificial
Intelligence (Dassel/Solling, 2327 September 1985),
InformatikFachberichte 118, ed. H. Stoyan, SpringerVerlag,
Berlin, 1985, pp. 5776.
*[Blasius 1986a] K.H. Blasius, Construction of Equality Graphs,
SEKI Report SR8601, Universitat Kaiserslautern, Dept. of
Computer Science, 1986.
*[Blasius 1986b] K.H. Blasius, Against the ``Anti Waltz
Effect'' in equality reasoning, Proc. GWAI86 und 2.
Osterreichische ArtificialIntelligenceTagung
(Ottenstein/Niederosterreich, 2226 September 1986),
InformatikFachberichte 124, SpringerVerlag, Berlin, 1986, pp.
230241.
*[Blasius 1986c] K.H. Blasius, Equality reasoning based on
graphs, PhD thesis, Fachbereich Informatik, Universitat
Kaiserslautern, 1986; also SEKI Report SR8701, 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 (CADE9, Argonne, Illinois, 2326 May 1988),
ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag, Berlin,
1988, pp. 397414.
*[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
proofchecking in set theory: a preliminary report, Sandia Corp.
Rep. SCRR67525, 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):5577;
also Automation Of Reasoning  Classical Papers On Computational
Logic, Vol. II, 19671970, ed. J. Siekmann And G. Wrightson,
SpringerVerlag, Berlin, 1983, pp. 508530.
[Bledsoe 1972] W. Bledsoe, R. Boyer, W. Henneman, Computer
proofs of limit theorems, Artificial Intelligence 3(1):2760,
1972.
[Bledsoe 1973a] W.W. Bledsoe, Discussions on theorem proving,
Dept. Memo ATP10, Univ. of Texas at Austin, 1973.
[Bledsoe 1973b] W.W. Bledsoe, P. Bruell, A manmachine theorem
proving system, Proc. 3rd IJCAI, Stanford Univ., 1973; also
Artificial Intelligence 5(1):5172, 1974.
[Bledsoe 1973c] W.W. Bledsoe, Some ideas on automatic theorem
proving, Memo ATP9, Austin, Texas: Dept of Mathematics, Univ. of
Texas at Austin, 1973. [Bledsoe 1974] W.W. Bledsoe, The supinf
method in Presburger arithmetic, Memo ATP18, Math. Dept., Univ.
of Texas at Austin, 1974.
[Bledsoe 1975a] W.W. Bledsoe, M. Tyson, The UT interactive
prover, Report ATP17a & 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. 1521.
[Bledsoe 1977a] W. Bledsoe, Nonresolution theorem proving,
Artificial Intelligence 9(1):136, 1977; also in Readings in
Artificial Intelligence, ed. B.L. Webber and N.J. Nilsson, Morgan
Kaufmann Publishers, Los Altos, CA, 1981, pp. 91108.
[Bledsoe 1977b] W.W. Bledsoe, Set Variables, Proc. 5th IJCAI,
MIT, Cambridge, MA, 1977, pp. 501510.
[Bledsoe 1977c] W. Bledsoe, A maximal method for set variables
in automatic theorem proving, ATP33, Univ. of Texas, 1977; also
Machine Intelligence 9, ed. Hayes and Michie, Ellis Harwood Ltd.,
Chichester, 1979, pp. 53100.
[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. 3051.
[Bledsoe 1978a] W.W. Bledsoe, M. Tyson, The UT interactive
prover, ATP17A, Univ. of Texas at Austin, Texas, June 1978.
[Bledsoe 1978b] W.W. Bledsoe, M. Ballantyne, Unskolemizing,
ATP41a, Dept. Math. Univ. of Texas at Austin, 1978.
[Bledsoe 1979a] W.W. Bledsoe, P. Bruell, R. Shostak, A prover
for general inequalities, ATP40a, Dept. Math. Univ. of Texas at
Austin, 1979, abridged pp. 6669, Proc. 6th IJCAI, Tokyo, August
2023, 1979.
[Bledsoe 1979b] W.W. Bledsoe, A resolutionbased prover for
general inequalities, Univ. of Texas, Math. Dept. Memo ATP52,
July 1979.
[Bledsoe 1980a] W.W. Bledsoe, L.M. Hines, Variable elimination
and chaining in a resolutionbased prover for inequalities, Memo
ATP56a, Math. Dept., Univ. of Texas at Austin, April 1980; also
Proc. 5th Conf. on Automated Deduction (Les Arcs, France, 811
July 1980), ed. W. Bibel and R. Kowalski, LNCS 87,
SpringerVerlag, Berlin, 1980, pp. 7087.
[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
ATP65, Univ. of Texas at Austin, 1982; also J. of Artificial
Intelligence 27(3):255288, December 1985.
*[Bledsoe 1982b] W.W. Bledsoe, Using examples to generate
instantiations for set variables, Automatic Theorem Proving
Project, Univ. of Texas at Austin, ATP67, July 1982; also Proc.
8th IJCAI, Karlsruhe, W. Germany, 812 August 1983, pp. 892901.
[Bledsoe 1982c] W.W. Bledsoe, Some automatic proofs in analysis,
Automatic Theorem Proving Project, Univ. of Texas at Austin,
ATP71, 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. 89118.
[Bledsoe 1983a] W.W. Bledsoe, The UT natural deduction prover,
Automatic Theorem Proving Project, Univ. of Texas at Austin,
ATP17B, April 1983.
[Bledsoe 1983b] W.W., Ground resolution using anticlauses,
Report No. ATP72, 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):2327, 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 ATP83,
MCCAI15886, November 1985.
[Bledsoe 1986a] W.W. Bledsoe, The use of analogy in proof
discovery, MCC Tech. Report AI215886, 1986.
[Bledsoe 1986b] W.W. Bledsoe, Some thoughts on proof discovery,
MCC Tech. Report AI20886, June 1986; also Proc. IEEE 1986 Symp.
on Logic Programming (Salt Lake City, UT, 2225 September 1986),
1986, pp. 210; also in In Computers in Mathematics, ed. D.V.
Chudnovsky and R.D. Jenks, Marcel Dekker, Inc., New York, 1990,
pp. 83108.
*[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. 483543.
[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):341359, September 1990.
[Bockmayr 1987] A. Bockmayr, A note on a canonical theory with
undecidable unification and matching problem, J. of Automated
Reasoning 3(4):379381, 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 TRARP15/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):563585, December 1991.
*[Bollinger 1991] T. Bollinger, A model elimination calculus for
generalized clauses, IWBSReport, IBM Deutschland, Scientific
Center, 1991; also Proc. 12th Intl. Conf. on Artificial
Intelligence, Vol 1 (IJCAI91, Darling Harbour, Sydney, Australia,
2430 August 1991), Morgan Kaufmann Publ., Inc., 1991, pp.
126131.
*[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, 35
April 1989), ed. N. Dershowitz, SpringerVerlag, NY, 1989, pp.
548550.
[Book 1981] R.V. Book, C.P. O'Dunlaing, Testing for the
ChurchRosser property, Theoretical Computer Science
16(2):223230, November 1981.
[Book 1982a] R.V. Book, The power of the ChurchRosser property
for string rewriting systems, Proc. 6th Conf. on Automated
Deduction, ed. D. Loveland, LNCS 138, SpringerVerlag, Berlin,
1982. pp. 360368.
[Book 1982b] R.V. Book, Confluent and other types of Thue
systems, JACM 29(2):178218, August 1982.
[Book 1982c] R.V. Book, M. Jantzen, C. Wrathall, Monadic Thue
Systems, NorthHolland, Theoretical Computer Science
19(1982):231251.
[Book 1983] R.V. Book, Decidable sentences of ChurchRosser
congruences, Theoret. Comput. Sci. 24(1983):301312.
[Book 1984] R. Book, J.H. Siekmann, On the unification
hierarchy, Memo SEKI84V, Universitat Karlsruhe, Institut fur
Informatik I, W. Germany, 1984; also Proc. GWAI85, 9th German
Workshop on Artificial Intelligence (Dassel/Solling, 2327
September 1985), InformatikFachberichte 118, ed. H. Stoyan,
SpringerVerlag, Berlin, 1985, pp. 111117.
[Book 1985a] R. Book, Thue systems as rewriting systems, Proc.
1st Conf. Rewriting Techniques and Applications (Dijon, France,
2022 May 1985), ed. J.P. Jouannaud, LNCS 202, SpringerVerlag,
Berlin, 1985, pp. 6394; also J. of Symbolic Computation 3(1 and
2):3968, February/April 1987.
[Book 1985b] R.V. Book, F. Otto, Cancellation rules and extended
word problems, Information Processing Letters 20(1):511, 1985.
[Book 1986] R.V. Book, J.H. Siekmann, On unification: Equational
theories are not bounded, J. of Symbolic Computation 2(4):317324,
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. 466471.
[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, SpringerVerlag, Berlin, 1987, pp.
276290.
[Bosco 1987b] P.G. Bosco, E. Giovannetti, G. Levi, C. Moiso, C.
Palamidessi, A complete semantic characterization of KLEAF, a
logic language with partial functions, Proc. 1987 Symp. on Logic
Programming, IEEE Society Press, 1987, pp. 318327.
[Bosco 1988] P.G. Bosco, E. Giovannetti, C. Moiso, Narrowing vs.
SLDresolution, J. of Theoretical Computer Science 59(12):323,
NorthHolland.
*[Bosco 1989] P.G. Bosco, C. Cecchi, C. Moiso, An extension of
WAM for KLEAF: A WAMbased compilation of conditional narrowing,
Logic Programming: Proc. 6th Intl. Conf., ed. G. Levi and M.
Martelli, The MIT Press, Cambridge, MA, 1989, pp. 318333.
*[Bose 1988] S. Bose, E.M. Clarke, D.E. Long, S. Michaylov,
Parthenon, a parallel theorem prover for nonHorn clauses, Tech.
Rept. No. CMUCS88137, Computer Scinece Dept., CarnegieMellon
Univ., Pittsburgh, PA, 1988; Proc. 4th Annual Symp. Logic in
Computer Science (Pacific Grove, CA, 58 June 1989), IEEE, 1989,
pp. 8089.
*[Boudet 1988] A. Boudet, J.P. Jouannaud, M. SchmidtSchauss,
Unification in free extensions of Boolean rings and Abelian
groups, Proc. 3rd Annual Symp. on Logic in Computer Science
(Edinburgh, Scotland, 58 July 1988), IEEE, 1988, pp. 121130.
[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 (CADE10, Kaiserslautern, FRG, July
1990), Lecture Notes in Artificial Intelligence 449, ed. M.E.
Stickel, SpringerVerlag, Berlin, 1990, pp. 292307.
*[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, 47 June 1990), IEEE Computer
Society Press, Los Alamitos, CA, 1990, pp. 289299.
*[Boudet 1992] A. Boudet, Unification in ordersorted algebras
with overloading, Proc. 11th Intl. Conf. on Automated Deduction
(CADE11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur,
Lecture Notes in Artificial Intelligence 607, SpringerVerlag,
Berlin, 1992, pp. 193207.
[Boudol 1983a] G. Boudol, L. Kott, Recursion induction principal
revisited, Theoretical Computer Science 22(1):135174, 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.
169236.
*[Bouhoula 1993] A. Bouhoula, M. Rusinowitch, Automatic case
analysis in proof by induction, Proc. 13th IJCAI (Chambery,
France, 28 August3 September 1993), Vol 1, ed. R. Bajscy, IJCAI,
Inc., 1993, pp. 8894.
*[Bousdira 1988a] W. Bousdira, J.L. Remy, Hierarchical
contextual rewriting with several levels, Proc. 1st Intl. Workshop
on Conditional Term Rewriting Systems (Orsay, France, 810 July
1987), ed. S. Kaplan and J.P. Jouannaud, LNCS 308,
SpringerVerlag, Berlin, 1988, pp. 1530; also Proc. 5th Annual
Symp. on Theoretical Aspects of Computer Science (Bordeaux,
France), ed. R. Cori and M. Wirsing, LNCS 294, SpringerVerlag,
Berlin, 1988, pp. 193206.
*[Bousdira 1988b] W. Bousdira, J.L. Remy, REVEUR4 : A
laboratory for conditional rewriting, Proc. 1st Intl. Workshop on
Conditional Term Rewriting Systems (Orsay, France, 810 July
1987), ed. S. Kaplan and J.P. Jouannaud, LNCS 308,
SpringerVerlag, Berlin, 1988, pp. 253257.
*[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, 1317 July 1987, pp.
9599.
*[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 (CADE9, Argonne, Illinois, 2326 May
1988), ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag,
Berlin, 1988, pp. 744745.
*[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, 48 July 1988), ed. P. Gianni, LNCS 358,
SpringerVerlag, Berlin, 1989, pp. 402406.
[Boy 1989b] T. Boy de la Tour, A locally optimal transformation
into clause form using partial formula renaming, RR 765IIMAG 
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.
101116.
[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. 486493; also JACM 22(1):129144, 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. 511519.
[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. CSL91, 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 CSL108, 1979; also In: The
Correctness Problem in Computer Science, ed. R.S. Boyer and J S.
Moore, Academic Press, London, 1981, pp. 103184.
[Boyer 1982a] R.S. Boyer, J S. Moore, A mechanical proof of the
unsolvability of the halting problem, ICSCACMP28, Univ. of Texas
at Austin, July 1982; also JACM 31(3):441458, 1984.
[Boyer 1982b] R.S. Boyer, J S. Moore, Proof checking the RSA
public key encryption algorithm, ICSCACMP33, Univ. of Texas at
Austin, September 1982.
[Boyer 1983a] R.S. Boyer, J S. Moore, Proofchecking,
theoremproving, 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,
ICSCACMP36, 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, ICSCACMP37, 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 133167.
[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):1722, 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 ICSCACNP44, 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. 83124.
[Boyer 1986a] R.S. Boyer, E. Lushk, W. McCune, R. Overbeek, M.
Stickel, and L. Wos, Set theory in firstorder logic: Clauses for
Godel's axioms, J. of Automated Reasoning 2(3):287327, September
1986.
[Boyer 1986b] R.S. Boyer, J S. Moore, Overview of a
TheoremProver for a Computational Logic, Proc. 8th Intl. Conf. on
Automated Deduction (CADE8, Oxford, England, July 27August 1,
1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986,
pp. 675678.
[Boyer 1986c] R.S. Boyer, Rewrite Rule Compilation, MCC Tech.
Report AI19486, 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, ICSCACMP52, 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):117172, 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 CLI24, 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
CLI23, 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, SpringerVerlag, Berlin, 1990,
pp. 115.
*[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 (CADE11, Saratoga Springs, NY,
USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial
Intelligence 607, SpringerVerlag, Berlin, 1992, pp. 416430.
*[Brackin 1987] S.H. Brackin, Knowledgebased theorem proving
for verification, M8775, 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):233253.
[Branagan 1981] E.J. Branagan, An interactive theorem prover
verification, CES8109, 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):412430, 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 RC7404,
T.J. Watson Research Center, Yorktown Heights, NY, December 1978;
also Proc. 4th Workshop on Automatic Deduction, Austin, Texas, 13
February 1979, pp. 3642.
[Bratko 1982] I. Bratko, Knowledgebased problem solving,
Machine Intelligence 9, ed. Hayes, Michie, and Pao, Ellis Harwood
Ltd., Chichester, 1982, pp. 73100.
*[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):177195, 1981.
[Breben 1982] M. Breban, Decision algorithms for a class of
settheoretic 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):147215, 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 AI34786, 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 ACAAI27487, Microelectronics and Computer
Technology Corporation, Austin, TX, August 1987.
[Brock 1987b] B. Brock, S. Cooper, W. Pierce, Box users manual,
MCC Tech. Rport ACAAI27387, September 1987.
*[Brock 1988] B. Brock, S. Cooper, W. Pierce, Analogical
reasoning and proof discovery, Proc. 9th Intl. Conf. on Automated
Deduction (CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk
and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
454468.
*[Brock 1989] B. Brock, An experimental implementation of
equivalence reasoning in the BoyerMoore theorem prover, Internal
note 104, Computational Logic Inc., Draft, 25 January 1989.
[Broda 1980] K. Broda, The relation between semantic tableaux
and resolution theoremprovers, 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, 610 August 1990), ed. L.C. Aiello, Pitman
Publishing, London, 1990, pp. 111116.
[Brotz 1974a] D.K. Brotz, Embedding heuristic problem solving
methods in a mechanical theorem prover, STANCS74443, 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 designmethod 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):175200, 1977.
[Brown 1977b] R. Brown, Use of analogy to achieve new expertise,
AITR403, Artificial Intelligence Lab., MIT, 1977.
*[Brown 1977c] F.M. Brown, A theorem prover for elementary set
theory, Proc. 5th IJCAI, MIT, Cambridge, MA, 2225 August 1977,
pp. 534540.
[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):281316, 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 metatheory, Proc.
4th Workshop on Automated Deduction (CADE4, Austin, Texas, 13
February 1979), ed. W.H. Joyner, 1979.
[Brown 1979b] F.M. Brown, S.A. Tarnlund, Inductive reasoning on
recursive equation, Artificial Intelligence 12(1979): 207229.
[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):221242, 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 selfmodifying theorem prover, Proc.
AAAI84, Natl Conf. on Artificial Intelligence, Univ. of Texas at
Austin, 610 August 1984, pp. 3841.
[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, 1823 August 1985.
[Brown 1986] F.M. Brown, An experimental logic based on the
fundamental deduction principle, AIRIT TR865, also Artificial
Intelligence 30(2):117263, 1986.
[Brown 1986b] R.M. Brown, A commonsense theory of nonmonotonic
reasoning, Proc. 8th Intl. Conf. on Automated Deduction (CADE8,
Oxford, England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS
230, SpringerVerlag, Berlin, 1986, pp. 209228.
[Brown 1986c] R.M. Brown, Automatic deduction in set theory,
Dept. of Computer Science TR866, 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 (CADE9, Argonne, Illinois, 2326 May
1988), ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag,
Berlin, 1988, pp. 756757.
*[Brown 1988b] F.M. Brown, S.S. Park, J. Phelps, ZPLAN: An
automatic reasoning system for situations, Proc. 9th Intl. Conf.
on Automated Deduction (CADE9, Argonne, Illinois, 2326 May
1988), ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag,
Berlin, 1988, pp. 758759.
*[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, 48
July 1988), ed. P. Gianni, LNCS 358, SpringerVerlag, Berlin,
1989, pp. 364377.
*[Brown 1990a] F.M. Brown, C. Araya, Schemata (abstract), Proc.
10th Intl. Conf. on Automated Deduction (CADE10, Kaiserslautern,
FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed.
M.E. Stickel, SpringerVerlag, Berlin, 1990, pp. 643644.
*[Brown 1990b] F.M. Brown, C. Araya, Cylindric algebra equation
solver (abstract), Proc. 10th Intl. Conf. on Automated Deduction
(CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes in
Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, pp. 645646.
[Bruell 1973] P. Bruell, A description of the functions of the
manmachine topology theorem prover, Univ. of Texas at Austin,
Math. Dept. Memo ATP8, 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, SpringerVerlag, Berlin, 1970, pp. 2961; also Symp. on
Automatic Demonstration (IRIA, Versailles, 1968), SpringerVerlag,
NY, Lecture Notes in Mathematics 125(1970):2961.
[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 ChurchRosser theorem, Indagationes
Mathematicae 34(5):381392, 1972.
[Bruijn 1974] N.G. de Bruijn, Some extensions of Automath: the
AUT4 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 197506, 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. 579606.
[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, 19671970, ed. J. Siekmann and G. Wrightson,
SpringerVerlag, Berlin, 1983, pp. 159200.
[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
topdown logical reasoning through intelligent backtracking,
Report CIUNL8/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
firstorder theories, Internal Report KB27, ECRC, 1986.
*[Bryant 1986] R. E. Bryant, Graphbased algorithms for Boolean
functions manipulations, IEEE Transactions on Computers
C35(8):677691, August 1986. [Buchanan 1985] B.G. Buchanan,
Expert Systems, J. of Automated Reasoning 1(1):2834, 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):2427, April 1991.
[Buchberger 1965] B. Buchberger, An algorithm for finding a
basis for the residue class ring of a zerodimensional 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):374383.
[Buchberger 1976a] B. Buchberger, A theoretical basis for the
reduction of polynomials to canonical forms, ACMSIGSAM Bulletin
10(3):1927, August 1976.
[Buchberger 1976b] B. Buchberger, Some properties of Grobner
bases for polynomial ideals, JACM SIGSAM Bull. 10(4):1924, 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,
SpringerVerlag, Berlin, pp. 321.
[Buchberger 1982a] B. Buchberger, G.E. Collins, R. Loos, eds.,
Computer Algebra: Symbolic and Algebraic Computations, Computing
Suppl. 4, SpringerVerlag, 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, SpringerVerlag, NY, 1982, 2nd edition 1983, pp.
1143.
[Buchberger 1983] B. Buchberger, A note on the complexity of
constructing Grobner bases, Proc. EUROCAL 83, LNCS 162,
SpringerVerlag, Berlin, 1983, pp. 137145.
[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, SpringerVerlag,
Berlin, 1984, pp. 137161.
[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. 184232.
[Buchberger 1985b] B. Buchberger, Basic features and development
of the criticalpair/completion approach, Proc. 1st Conf.
Rewriting Techniques and Applications (Dijon, France, 2022 May
1985), ed. J.P. Jouannaud, LNCS 202, SpringerVerlag, Berlin,
1985, pp. 145.
[Buchberger 1985c] B. Buchberger, A survey on the method of
Grobner bases for solving problems in connection with systems of
multivariate polynomials, 2nd RIKEN Intl. Symp. on Symbolic and
Algebraic Computation by Computers, ed. N. Inada and T. Soma,
World Scientific Publishing Co., 1985, pp. 6983.
[Buchberger 1985d] B. Buchberger, History and basic features of
the criticalpair/completion procedure, Proc. 1st Intl. Conf.
Rewriting Techniques and Applications, LNCS 202, SpringerVerlag,
Berlin, 1985, pp. 301324; also J. of Symbolic Computation 3(1 and
2):338, February/April 1987.
*[Buchberger 1987] B. Buchberger, Applications of Grobner bases
in nonlinear computational geometry, Proc. Trends in Computer
Algebra, Intl. Symp. (Bad Neuenahr, 1921 May 1987), ed. R.
Janssen, LNCS 296, SpringerVerlag, Berlin, pp. 5280.
*[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. 85119.
[Buchen 1979] H. Buchen, Reduction systems and small
cancellation theory, Proc. 4th Workshop on Automated Deduction
(CADE4, Austin, Texas, 13 February 1979), ed. W.H. Joyner, 1979,
pp. 5359.
[Buchholz 1981] W. Buchholz, S. Feferman, W. Pohlers, W. Sieg,
Iterated inductive definitions and subsystems of analysis, In
Recent ProofTheoretical Studies, Lecture Notes in Mathematics
897, SpringerVerlag, 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. 111.
[BuinesRozas 1979] J. BuinesRozas, GOAL: A goaloriented
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 AIM328,
1979.
[Bundgen 1987] R. Bundgen, Design, implementation, and
application of an extended groundreducibility test, Master's
thesis, Computer and Information Sciences, Univ. of Delaware,
Newark, DE 19716, 1987; also Tech. Report 8805, 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, 35 April 1989), ed. N. Dershowitz, SpringerVerlag, NY,
1989, pp. 5975.
[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. 130138.
[Bundy 1975] A. Bundy, Analysing mathematical proofs (or reading
between the lines), Proc. 4th IJCAI, Tbilisi, Georgia, USSR, 1975.
pp. 2228.
[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 metalevel
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):189211, May 1981.
[Bundy 1979b] A. Bundy, L. Byrd, G. Luger, C. Mellish, R. Milne,
M. Palmer, Solving mechanics problems using metalevel inference,
Proc. IJCAI79 (6th IJCAI), ed. B.G. Buchanan, Tokyo, August 1979,
pp. 10171027; reprinted in Expert Systems in the Microelectronic
Age, ed. D. MIchie, pp. 5064, Edinburgh Univ. Press, 1979; also
available from Edinburgh Univ., DAI Research Paper 112.
[Bundy 1980] A. Bundy, B. Welham, Metalevel inference, Proc.
5th Conf. on Automated Deduction (Les Arcs, France, 811 July
1980), ed. W. Bibel and R. Kowalski, LNCS 87, SpringerVerlag,
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. 551553.
[Bundy 1981b] A. Bundy, Bob Welhan, Using metalevel inference
for selective application of multiple rewrite rule sets in
algebraic manipulation, DAI Research Paper 121, Edinburgh, 1981;
also Artificial Intelligence 16(2):189212, May 1981.
[Bundy 1981c] A. Bundy, L.S. Sterling, Metalevel 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, Specialpurpose,
but domainindependent, inference mechanisms, DAI Research Paper
179, Dept. of Artificial Intelligence, Univ. of Edinburgh,
Edinburgh; also Proc. ECAI82, ParisSud, Orsay, France, 1214
July 1982, pp. 6774; also Progress in Artificial Intelligence,
ed. L. Steels and J.A. Campbell, Ellis Horwood Limited,
Chichester, West Sussex, 1985. pp. 93111.
[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. 109116.
[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. 12211230.
[Bundy 1985b] A. Bundy, Metalevel 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. Capri85 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. AISB85, ed. P. Ross,
1985, pp. 7886.
*[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, 1012 April 1985), In: Artificial Intelligence and its
applications, ed. A.G. Cohn and J.R. Thomas, John Wiley &
Sons, Chichester, 1986, pp. 5159.
[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 (CADE9, Argonne, Illinois, 2326 May
1988), ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag,
Berlin, 1988, pp. 111120.
*[Bundy 1988a] A. Bundy, L. Sterling, Metalevel inference two
applications, Research Paper No. 273, Dept. of AI, Univ. of
Edinburgh; also J. of Automated Reasoning 4(1):1527, 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):303324, 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,
2025 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp.
359365;
[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. 178198.
*[Bundy 1989c] A. Bundy, F. van Harmelen, A. Smaill, Extensions
to the ripplingout 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 (CADE10, Kaiserslautern,
FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed.
M.E. Stickel, SpringerVerlag, Berlin, 1990, pp. 132146.
*[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, 2025 August
1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 359365.
*[Bundy 1990a] A. Bundy, A science of reasoning: extended
abstract, Proc. 10th Intl. Conf. on Automated Deduction (CADE10,
Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial
Intelligence 449, ed. M.E. Stickel, SpringerVerlag, Berlin, 1990,
pp. 633640.
*[Bundy 1990b] A. Bundy, F. van Harmelen, C. Horn, A. Smaill,
The oysterclam system (abstract), DAI Research Paper No. 507,
Univ. of Edinburgh; Proc. 10th Intl. Conf. on Automated Deduction
(CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes in
Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, pp. 647648.
[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 1012 April
1990), LNCS 429, ed. A Miola, SpringerVerlag, 1990, pp. 151153.
[Bundy 1990e] A. Bundy, G. Giunchiglia, T. Walsh, Building
abstractions, In Proc. of the AAAI90 Workshop on automatic
Generation of Approximations and Abstractions, pp. 221232,
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:185253, 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. 149166; 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):319335, September 1990.
*[Buntine 1988] W. Buntine, Generalized subsumption and its
applications to induction and redundancy, Artificial Intelligence
36(2):149177, September 1988.
[Buntine 1989] W. Buntine, H.J. Burchert, On solving equations
and disequations, SEKI Report SR8903, Fachbereich Informatik,
Universitat Kaiserslautern, Kaiserslautern, 1989.
[Burckert 1983] H.J. Burckert, H. Wang, R. Zheng, MKRP: A
performance test by working mathematics, Memo SEKI83I, Institut
fur Informatik I, Universitat Karlsruhe, W. Germany, 1983.
[Burckert 1986a] H.J. Burckert, Some relationships between
unification, restricted unification, and matching, SEKI Report
SR8605, Universitat Kaiserslautern, 1986; also Proc. 8th Intl.
Conf. on Automated Deduction (CADE8, Oxford, England, July
27August 1, 1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag,
Berlin, 1986, pp. 514524.
[Burckert 1986b] H.J. Burckert, A. Herold, M. SchmidtSchauss,
On equational theories, unification and decidability, SEKI Report
SR8620, Universitat Kaiserslautern, 1986; also Proc. 2nd Intl.
Conf. on Rewriting Techniques and Applications (Bordeaux, France,
2527 May 1987), ed. P. Lescanne, LNCS 256, SpringerVerlag,
Berlin, 1987, pp. 204215; 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 SR8708, Universitat Kaiserslautern,
1987; also J. Symbolic Computation 8(1989):523536.
*[Burckert 1987b] H.J. Burckert, Lazy Eunification  A method
to delay alternative solutions, SEKI Working Paper SWP8707,
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 SR8715, Universitat
Kaiserslautern, 1987; also Proc. 9th Intl. Conf. on Automated
Deduction (CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk
and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
517526.
*[Burckert 1988] H.J. Burckert, A. Herold, D. Kapur, J.H.
Siekmann, M.E. Stickel, M. Tepp, H. Zhang, Opening the
ACUnification Race, SEKI Report SR8811, Universitat
Kaiserslautern, July 1988; also J. Automated Reasoning
4(4):465474, December 1988.
[Burckert 1989a] H.J. Burckert, M. SchmidtSchauss, On the
solvability of equational problems, SEKI Report SR8907,
Universitat Kaiserslautern, 1989.
[Burckert 1989b] H.J. Burckert, A. Herold, and M.
SchmidtSchauss, On equational theories, unification, and
(un)decidability, J. of Symbolic Computation 8(1 and 2):349, 1989
(special issue on unification. part 2).
*[Burckert 1990] H.J. Burckert, A resolution principle for
clauses with constraints, Research Report RR9002, Deutsches
Forschungszentrum fur Kunstliche Intelligenz GmbH, Kaiserslautern,
March 1990; also Proc. 10th Intl. Conf. on Automated Deduction
(CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes in
Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, pp. 178192.
[Bursky 1968] P. Bursky, J. Slagle, Experiments with a
multipurpose theorem proving heuristic program, JACM 15(1):8599,
January 1968.
[Burstall 1968] R.M. Burstall, A scheme for indexing and
retrieving clauses for a resolution theoremprover, MIPR45,
Univ. of Edinburgh, 1968.
[Burstall 1969] R. Burstall, Proving properties of programs by
structural induction, Computer J. 12(1):4148, 1969.
[Burstall 1970] R.M. Burstall, Formalising semantics of first
order logic in first order logic, and application to planning for
robots, MIPR73, Dept. of Machine Intelligence, Univ. of
Edinburgh, Edinburgh, March 1970.
[Burstall 1986] R.M. Burstall, Research in interactive theorem
proving at Edinburgh University, ECSLFCS8612, Laboratory for
Foundations of Computer Science, Univ. of Edinburgh, Edinburgh,
1986; also published as CSR21886.
[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):916927, 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 MTP7,
Math. Dept., Louisiana Tech. Univ., Ruston, LA, August 1980.
[Butler 1986] R. Butler, E. Lusk, W. McCune, R. Overbeek, Paths
to highperformance automated theorem proving, Proc. 8th Intl.
Conf. on Automated Deduction (CADE8, Oxford, England, July
27August 1, 1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag,
Berlin, 1986, pp. 588597.
*[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 (CADE9, Argonne, Illinois, 2326 May
1988), ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag,
Berlin, 1988, pp. 323332.
*[Butler 1988] R.M. Butler, N.T. Karonis, Exploitation of
parallelism in prototypical deduction problems, Proc. 9th Intl.
Conf. on Automated Deduction (CADE9, Argonne, Illinois, 2326 May
1988), ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag,
Berlin, 1988, pp. 333343.
*[Butler 1990] R. Butler, I. Foster, A. Jindal, R. Overbeek, A
highperformance parallel theorem prover, Proc. 10th Intl. Conf.
on Automated Deduction (CADE10, Kaiserslautern, FRG, July 1990),
Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel,
SpringerVerlag, Berlin, 1990, pp. 649650.
[Buttner 1985] W. Buttner, Unification in data structure
multisets, Report, Siemens AG, Corporate Laboratories for
Information Technology, Munchen, 1985; also SEKIReport Memo
SEKI85VKL, Fachbereich Informatik, Universitat Kaiserslautern,
1985; also J. of Automated Reasoning 2(1):7588, D. Reidel Publ.
Co., Dordrecht, Holland, 1986.
[Buttner 1986a] W. Buttner, Unification in data structure sets,
Proc. 8th Intl. Conf. on Automated Deduction (CADE8, Oxford,
England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS 230,
SpringerVerlag, Berlin, 1986, pp. 470488.
*[Buttner 1986b] W. Buttner, H. Simonis, Embedding Boolean
expressions into logic programming, preprint, Siemens AG, Munchen,
1986; also J. of Symbolic Computation 4(2):191205, October 1987.
*[Buttner 1988] W. Buttner, Unification in finite algebras in
unitary, Proc. 9th Intl. Conf. on Automated Deduction (CADE9,
Argonne, Illinois, 2326 May 1988), ed. E. Lusk and R. Overbeek,
LNCS 310, SpringerVerlag, Berlin, 1988, pp. 368377.
