ORA Canada Bibliography of Automated Deduction: Authors H to J
*[Hadzikadic 1986] M. Hadzikadic, F. Lichtenberger, D.Y.Y. Yun,
An application of knowledgebase technology in education: A
geometry theorem prover, 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. 141147.
[Hager 1985] G.D. Hager, Computational aspects of proofs in
modal logic, MsCIS8557, Univ. of Pennsylvania, 1985.
[Hager 1988] J. Hager, M. Moser, PASTE  A parallel system for
term unification, Fortgeschrittenenpraktikum, TUM, December 1988.
*[Hager 1989] J. Hager and M. Moser, An approach to parallel
unification using transputers, Proc. 13 German Workshop on
Artificial Intelligence (GWAI89, Eringerfeld, 1822 September
1989), ed. D. Metzing, SpringerVerlag, Berlin, 1989, pp. 8391.
[Hagiya 1985] M. Hagiya, S. Hayashi, Some experiments on EKL,
ICOT TM101, 1985.
*[Hagiya 1990] M. Hagiya, Programming by example and proving by
example using higherorder unification, 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. 588602.
*[Hagiya 1991] M. Hagiya, Higherorder unification as a theorem
proving procedure, In Logic Programming: Proc. 8th Intl. Conf.,
ed. K. Furukawa, The MIT Press, Cambridge, MA, 1991, pp. 270284.
[Hahnie 1986] R. Hahnie, M. Heisel, W. Reif, W. Stephen, An
interactive verification system based on dynamic 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. 306315.
[Haken 1984] A. Haken, The intractability of resolution, PhD
thesis, Univ. of Illinois at UrbanaChampaign, 1984; also
Theoretical Computer Science 39(1985):297308.
[Hall 1966] D. Hall, Semantic heuristics in a firstorder
problem solver, PhD thesis, Carnegie Inst. of Tech., Pittsburgh,
1966.
[Hall 1985] R.P. Hall, Analogical reasoning in artificial
intelligence and related disciplines, Irvine Computational
Intelligence Project, Univ. of California, Irvine.
[Hallnas 1983] L. Hallnas, On normalization of proofs in set
theory, PhD thesis, Filosofiska istitutionen, Stockhoms
universitet, 1983.
[Halpern 1982] H. Halpern, Inductive inference in finite
algebraic structures, Proc. GWAI82, InformatikFachberichte 58,
ed. Wahlster, SpringerVerlag, Berlin, 1982, pp. 167176.
[Halpern 1987] H. Halpern, S. Owre, N. Proctor, W.P. Wilson,
Muse  A computer assisted verification system, IEEE Transactions
on Software Engineering SE13(2):151156, February 1987.
[Halpern 1990] J.Y. Halpern, J.H. Williams, E.L. Wimmers,
Completeness of rewrite rules and rewrite strategies for FP, JACM
37(1):86143, 1990.
[Hanna 1985] F.K. Hanna, N. Daeche, The Veritas theorem prover:
Part 1 tutorial exposition, Univ. of Kent at Canterbury
Electronics Lab. tech. report, draft, August 1985.
[Hanna 1986] F.K. Hanna, N. Daeche, Purely functional
implementation of 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.
598607.
[Haralick 1980] R.M. Haralick, G.L. Elliott, Increasing tree
search efficiency for constraint satisfaction problems, Artificial
Intelligence 14(1980):263313.
[Harel 1980] Harel, Kozen, Parikh, Process logic,
expressiveness, decidability, completeness, FOCS 80(1980):129142.
[Harmelen 1989] F. van Harmelen, The CLAM proof planner, user
manual and programmer manual: version 1.4, Tech. Paper TP4, Dept.
of Artificial Intelligence, Edinburgh, 1989.
*[Harmelen 1991] F. van Harmelen, Metalevel Inference Systems,
Pitman Publishing, London, and Morgan Kaufmann Publishers, Inc.,
San Mateo, CA, 1991.
[Harper 1985] R.W. Harper, Aspects of the implementation of type
theory, Doctoral dissertation, Computer Science Department,
Cornell University, June 1985. [Harper 1986] R. Harper, K.
Mitchell, Introduction to Standard ML, Laboratory for the
Foundations of Computer Science, Univ. of Edinburgh, 1986.
*[Harper 1987] R. Harper, F. Honsell, G. Plotkin, A framework
for defining logics, ECSLFCS8723, Laboratory for the
Foundations of Computer Science, Univ. of Edinburgh, 1987; also
Proc. 2nd ACMIEEE Symp. on Logic in Computer Science (Ithaca, NY,
June 1987), IEEE Computer Society Press, 1987, pp. 194204.
[Harrison 1977] M.C. Harrison, A hierarchical approach to
theorem proving, Proc. 5th IJCAI, MIT, Cambridge, MA, 1977, pp.
529533.
[Harrison 1978] M.C. Harrison, N. Rubin, Another generalization
of resolution, JACM 25(3):341351, July 1978.
[Hart 1963] T.P. Hart, A proposal for a geometry TP program,
MIT, Memo 56, Cambridge, MA, 1963.
[Hart 1965] T.P. Hart, A useful algebraic property of Robinson's
unification algorithm, AI Memo 91, Artificial Intelligence
Project, MIT, Cambridge, MA, 1965.
[Hascoet 1988] L. Hascoet, A tacticdriven system for building
proofs, Report No.770, INRIA, December 1987; also in Proc. 7th
Seminar ``Programmation en Logique,'' Tregastel, May 1988.
*[Hasegawa 1992] R. Hasegawa, M. Koshimura, H. Fujita, MGTP: A
parallel theorem prover based on lazy model generation, 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. 776780.
[Hayes 1969] P. Hayes, A machineoriented formulation of the
extended functional calculus, Stanford Artificial Intelligence
Project, Memo 86, Stanford Univ., Stanford, 1969.
[Hayes 1971] P. Hayes, R. Kowalski, Automatic theoremproving,
DCL Memo 40, Univ. of Edinburgh, Edinburgh, 1971.
[Hayes 1973] P. Hayes, Computation and deduction, Proc. 2nd
Symp. on Mathematical Foundations of Computer Science (MFCS),
Czechoslovakian Academy of Sciences, Prague, 1973, pp. 105118.
[Hearn 1967] A.C. Hearn, REDUCE: A useroriented interactive
system for algebraic simplification, Interactive Systems for
Experimental Applied Mathematics, NY: Academic Press, 1967, pp.
7990.
[Hearn 1968] A.C. Hearn, The problem of substitution, IFIP 68,
SRIMemo70, 1968.
*[Hearn 1976] A.C. Hearn, A new reduce model for algebraic
simplification, Proc. 1976 ACM Symp. on Symbolic and Algebraic
Computation (SYMSAC '76, Yorktown Heights, NY, 1012 August 1976),
ed. R.D. Jenks, ACM, 1133 Avenue of the Americas, NY, NY 10036,
1976, pp. 4652.
[Hearn 1980] A.C. Hearn, Algebraic manipulation, in What Can be
Automated, ed. Arden, The MIT Press, Cambridge, MA, 1980.
[Heering 1986] J. Heering, P. Klint, The efficiency of the
equation interpreter compared with the UNH Prolog interpreter
(extended abstract), SIGPLAN Notices 21(2):1821, 1986.
[Heering 1988] J. Heering, P. Klint, Towards shorter algebraic
specifications: a smiple language definition and its compilation
to Prolog, Reprot CSR8814, Centre for Mathematics and Computer
Science, Amsterdam, 1988.
[Heijenoort 1967] J. van Heijenoort, From Frege to Godel: A
source book in mathematical logic, Harvard Univ. Press, Cambridge,
MA, 1967.
*[Heilbrunner 1986] S. Heilbrunner, S. Holldobler, The
undecidability of the unification and matching problem for
canonical theories, Tech. Report, Univ. of the Federal Armed
Forces, Munchen, 1986; also Acta Informatica 24(April
1987):157171. *[Heintze 1990] N. Heintze, J. Jaffar, A decision
procedure for a class of set constraints, Proc. 5th Annual IEEE
Symp. on Logic Computer Science (Philadelphia, PA, 47 June 1990),
IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 4257.
[Heisel 1986] M. Heisel, W. Reif, W. Stephan, A functional
language to construct proofs, Interner Bericht 1/86, Fakultat fur
Informatik, Universitat Karlsruhe, 1986.
*[Heisel 1987] M. Heisel, W. Reif, W. Stephan, Program
verification by symbolic execution and induction, Proc. 11th
German Workshop on Artificial Intelligence (GWAI87, Geseke,
September 28October 2, 1987), ed. K. Morik, SpringerVerlag,
Berlin, 1987, pp. 201210.
*[Heisel 1988] M. Heisel, W. Reif, W. Stephan, Implementing
verification strategies in the KIVsystem, 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. 131140.
*[Heisel 1990] M. Heisel, W. Reif, W. Stephan, Tactical theorem
proving in program verification, 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. 117131.
*[Helman 1988] P. Helman, R. Veroff, Designing deductive
databases, J. of Automated Reasoning 4(1):2968, March 1988.
*[Hendriks 1988] P.R.H. Hendriks, ASF system user's guide,
Report CSR8823, Centre for Mathematics and Computer Science,
Amsterdam, May 1988.
[Henschen 1968] L.J. Henschen, Some new results on resolution in
automated theorem proving, Illinois Univ., Urbana, Master's
thesis, Rep. 261, May 1968.
[Henschen 1969] L.J. Henschen, Resolution, merging, set of
support and tautologies, Rep. 817, Dept. of Computer Science,
Univ. of Illinois., 1969.
[Henschen 1971] L.J. Henschen, A resolution style proof
procedure for higher order logic, PhD, Univ. of Illinois at
UrbanaChampaign, Illinois, 1971.
[Henschen 1972] L.J. Henschen, Nsorted logic for automatic
theorem proving in higherorder logic, Proc. ACM Conf., Boston,
MA, 1972.
[Henschen 1974a] L. Henschen, L. Wos, Unit refutations and Horn
sets, JACM 21(October 1974):590605.
[Henschen 1974b] L. Henschen, R. Overbeek, L. Wos, A
theoremproving language for experimentation, CACM 17(6):308314,
June 1974.
[Henschen 1976] L. Henschen, Semantic resolution for Horn sets,
IEEE Trans. on Computers C25, August 1976.
[Henschen 1977] L.J. Henschen, W.M. Evangelist, Theorem proving
by covering expressions, Proc. 5th IJCAI, MIT, Cambridge, MA,
1977, pp. 541542; also JACM 26(3):385400, July 1979.
[Henschen 1978] L.J. Henschen, An analysis of theorem proving by
covering expressions, Proc. 2nd Conf. Canadian Soc. for
Computational Studies of Intelligence, Univ. of Toronto, July
1978, pp. 3037.
[Henschen 1980] L. Henschen, Challenge problem I, SIGART
Newsletter 72(July 1980):3031.
[Henschen 1981] L.J. Henschen, S.A. Naqvi, An improved filter
for literal indexing in resolution systems, Proc. 7th IJCAI, Univ.
of British Columbia, Vancouver, August 1981, pp. 528531.
[Henschen 1982] L.J. Henschen, S.A. Naqvi, Representing infinite
sequences of resolvents in recursive firstorder Horn databases,
Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138,
SpringerVerlag, Berlin, 1982, pp. 342359.
[Henschen 1984] L.J. Henschen, S.A. Naqvi, Compiling queries in
recursive first order databases, JACM 31(1):4785, 1984.
[Henschen 1986] L. Henschen, H. Park, Indefinite and GCWA
inference in indefinite deduction databases, Proc. AAAI86, 5th
Natl Conf. on Artificial Intelligence, Philadelphia, PA, 1115
August 1986, pp. 191197.
[Henzinger 1985] T.A. Henzinger, H. Hofbauer, PROOFPAD: An
interactive proof generating system using natural deduction, Proc.
Osterreichische Artificial IntelligenceTagung, Wien (2427
September 1985), InformatikFachberichte 106, SpringerVerlag,
Berlin, 1985, pp. 173184.
[Hermann 1985] M. Hermann, I. Privara, On nontermination of
KnuthBendix algorithm, Research Report VUSEIAROPS3/85,
Institute of SocioEconomic Information and Automation, CS842 21,
Bratislava, Czechoslovakia, 1985; also Proc. Intl. Colloquium on
Automata, Languages and Programming (Rennes, France, July 1986),
ed. L. Kott, LNCS 226, SpringerVerlag, Berlin, 1986, pp. 146156.
*[Hermann 1991] M. Hermann, C. Kirchner, H. Kirchner,
Implementation of term rewriting systems, The Computer Journal
34(1):2033, February 1991.
[Herold 1982] A. Herold, Universal unification and a class of
equational theories, Proc. GWAI82, InformatikFachberichte 58,
ed. Wahlster, SpringerVerlag, Berlin, 1982, pp. 177190.
[Herold 1983] A. Herold, Some basic notions of first order
unification theory, Interner Bericht 15/83, Memo SEKI83II,
Institut fur Informatik I, Universitat Karlsruhe, W. Germany,
1983.
[Herold 1985a] A. Herold, J.H. Siekmann, Unification in Abelian
semigroups, SEKI Memo 85IIIKL, Fachbereich Informatik,
Universitat Kaiserslautern, 1985; also J. of Automated Reasoning
3(3):247283, September 1987.
[Herold 1985b] A. Herold, Combination of unification algorithms,
MemoSEKI86VIIIKL, Universitat Kaiserslautern, 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. 450469.
*[Herold 1986] A. Herold, Narrowing techniques applied to
idempotent unification, SEKI Report SR8616, Fachbereich
Informatik, Universitat Kaiserslautern, August 1986; also Proc.
11th German Workshop on Artificial Intelligence (GWAI87, Geseke,
September 28October 2, 1987), ed. K. Morik, SpringerVerlag,
Berlin, 1987, pp. 231240.
*[Herold 1987] A. Herold, Combination of unification algorithms
in equational theories, PhD thesis, SEKI Report SR8705,
Universitat Kaiserslautern, FRG, 1987.
[Hesketh 1991] J.T. Hesketh, Using middleout reasoning to guide
inductive theorem proving, PhD thesis, Univ. of Edinburgh, 1991.
*[Hesketh 1992] J. Hesketh, A. Bundy, A. Smaill, Using
middleout reasoning to control the synthesis of tailresursive
programs, 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.
310324.
*[Heuillard 1988] T. Heuillard, Compiling conditional rewriting
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. 111128.
[Hewitt 1969] C. Hewitt, PLANNER: A language for proving
theorems in robots, Proc. 1st IJCAI, Washington, D.C., 1969, pp.
295301.
[Hewitt 1970] C. Hewitt, PLANNER: a language for manipulating
models and proving theorems in a robot, AI Memo 168, Project MAC,
MIT, 1970.
[Hewitt 1972] C. Hewitt, Description and theoretical analysis
(using schemata) of PLANNER: A language for proving theorems and
manipulating models in a robot, PhD thesis, MIT, 1971; also
MITAILab report AITR258, 1972.
[Hickey 1989] T. Hickey, S. Mudambi, Global compilation of
Prolog, J. of Logic Programming 7(3):193230, November 1989.
[Hill 1974] R. Hill, LUSH resolution and its completeness, DCL
Memo 78, School of Artificial Intelligence, Univ. of Edinburgh,
August 1974.
*[Hindley 1986] J.R. Hindley, J.P. Seldin, Introduction to
combinators and lambdacalculus, Cambridge Univ. Press, Cambridge,
1986.
[Hines 1988a] L.M. Hines, Buildingin Knowledge of Axioms, PhD
Dissertation, Univ. of Texas, 1988.
*[Hines 1988b] L. Hines, Hyperchaining and knowledgebased
theorem proving, 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. 469486.
[Hines 1989a] L.M. Hines, W.W. Bledsoe, The STRIVE prover, Tech.
report ATP100, Univ. of Texas at Austin, August 1989.
[Hines 1989b] L. Hines, Completeness for a prover for dense
linear orders, Univ. of Texas CS Dept. Report ATP 86, March 1989;
to appear in J. Automated Reasoning.
*[Hines 1990] L.M. Hines, Strive: The Strivebased subset
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. 193206.
*[Hines 1992] L.M. Hines, 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. 3549.
*[Hintikka 1988] J. Hintikka, Model minimization  An
alternative to circumscription, J. of Automated Reasoning
4(1):114, March 1988.
[Hirata 1979] M. Hirata, T. Nishimura, A prover for parallel
processes, Proc. 6th IJCAI, Tokyo, August 2023, 1979, pp.
284389.
*[Hirose 1986] K. Hirose, An approach to proof checker, Proc.
12th Symp. Mathematical Foundations of Computer Science
(Bratislava, Czechoslovakia, 2529 August 1986), ed. J. Gruska, B.
Rovan and J Wiedermann, LNCS 233, SpringerVerlag, Berlin, pp.
113127.
[Hmelevskij 1964] J.I. Hmelevskij, The solution of certain
systems of word equations, Dokl. Akad. Nauk SSSR, 1964, 749 Soviet
Math. Dokl. 5, 1964, 724.
[Hmelevskij 1966] J.I. Hmelevskij, Word equations without
coefficients, Dokl. Akad. Nauk SSSR, 171, 1966, 1047 Soviet Math.
Dokl. 7, 1966, 1611.
[Hmelevskij 1967] J.I. Hmelevskij, Solution of word equations in
three unknowns, Dokl. Akad. Nauk. SSSR 177, 1967, no. 5, Soviet
Math. Dokl. 8, 1967, no. 6.
*[Hodes 1971] L. Hodes, Solving problems by formula manipulation
in logic and linear inequalities, Proc. 2nd IJCAI, Imperial
College, London, 13 September 1971, pp. 553559; also Artificial
Intelligence 3(1972):165174.
*[Hofbauer 1989] D. Hofbauer, C. Lautemann, Termination proofs
and the length of derivations (preliminary version), Proc. 3rd
Intl. Conf. Rewriting Techniques and Applications (Chapel Hill,
North Carolina, 35 April 1989), ed. N. Dershowitz,
SpringerVerlag, NY, 1989, pp. 167177.
[Hoffman 1971] G.R. Hoffman, G. Veenker, The unitclause proof
procedure with equality, Computing 7(1971):91105.
[Hoffmann 1979] C.M. Hoffmann, M.J. O'Donnell, An interpreter
generator using tree pattern matching, Proc. 6th Annual Symp. on
PoPL, San Antonio, Texas, 1979, pp. 169179.
[Hoffmann 1982a] C.M. Hoffmann, M.J. O'Donnell, Pattern matching
in trees, JACM 29(1):6895, January 1982.
[Hoffmann 1982b] C.M. Hoffmann, M.J. O'Donnell, Programming with
equations, ACM ToPLaS 4(1):83112, January 1982.
[Hoffmann 1984] C.M. Hoffmann, M.J. O'Donnell, Implementation of
an interpreter for abstract equations, Proc. 11th ACM Principles
of Programming Languages, Salt Lake City, Utah, January 1984, pp.
111121.
[Hoffmann 1985a] C.M. Hoffmann, M.J. O'Donnell, R. Strandh,
Programming with equations, Software, Practice and Experience,
December 1985.
[Hoffmann 1985b] C.M. Hoffmann, M.J. O'Donnell, R. Strandh,
Implementation of an interpreter for abstract equations, Software
 Practice and Experience 15(12):11851203, 1985.
[Holldobler 1985] S. Holldobler, U. Furbach, T. Laussermair,
Extended unification and its implementation, GWAI '85, IFB 118,
1986, pp. 176185.
*[Holldobler 1987a] S. Holldobler, A unification algorithm for
confluent theories, Proc. 14th Intl. Colloquium on Automata,
Languages, and Programming (ICALP '87, Karlsruhe, W. Germany,
1317 July 1987), ed. T. Ottmann, LNCS 267, SpringerVerlag,
Berlin, pp. 3141.
[Holldobler 1987b] S. Holldobler, From paramodulation to
narrowing, Univ. der Bundeswehr, Munchen, 1987.
*[Holldobler 1987c] S. Holldobler (ed.), Foundations of
Equational Logic Programming, Lecture Notes in Artificial
Intelligence 353, SpringerVerlag, Berlin, 1987.
*[Holldobler 1990] S. Holldobler, A structured connectionist
unification algorithm, Proc. 8th National Conf. on Artificial
Intelligence (AAAI90, July 29August 3, 1990, 1990), Vol. 2, AAAI
Press/The MIT Press, Menlo Park/Cambridge, pp. 587593.
[Honda 1979] M. Honda, R. Nakajima, Interactive theorem proving
for hierarchically and modularly structured sets of very many
axioms, Proc. 6th IJCAI, Tokyo, 1979, pp. 400402.
[Hong 1985] R. Hong, Research in intelligent robots, J. of
Automated Reasoning 1(1):1316, D. Reidel Publ. Co., Dordrecht,
Holland, 1985.
[Hook 1989] J. Hook and G. Pottinger, Ulysses theories: the
modular implementation of mathematics, Tech. Report TR 1114,
Odyssey Research Associates, Ithaca, NY, February 1989.
[Horn 1951] A. Horn, On sentences which are true of direct
unions of algebras, J. Symbolic Logic 16(March 1951):1421.
[Horn 1988] C. Horn, The NurPRL proof development system,
Working paper 214, Dept. of Artificial Intelligence, Edinburgh,
1988; The Edinburgh version of NurPRL has been renamed Oyster.
[Horn 1990] C. Horn, A. Smaill, Theorem proving with Oyster, DAI
Research Paper 505, Dept. of Artificial Intelligence, Univ. of
Edinburgh, 1990; To appear in Proc. IMA Unified Computation
Laboratory, Stirling.
[Hornig 1981] K.M. Hornig, Generating small models of first
order axioms, Proc. GWAI81, InformatikFachberichte 47, ed.
Siekmann, SpringerVerlag, Berlin, 1981, pp. 248255.
[Hornig 1982] K.M. Hornig, W. Bibel, Improvements of a
tautologytesting program, Proc. 6th Conf. on Automated Deduction,
ed. D. Loveland, LNCS 138, SpringerVerlag, Berlin, 1982, pp.
326341.
[Hornung 1981] G. Hornung, A. Knapp, and U. Knapp, A parallel
connection graph proof procedure, German Workshop on Artificial
Intelligence, LNCS, SpringerVerlag, Berlin, 1981, pp. 160167.
[Howe 1986] D.J. Howe, Implementing number theory: An experiment
with Nupri, Report 86752, Dept. of Computer Science, Cornell
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. 404415.
[Howe 1988a] D.J. Howe, Automating reasoning in an
implementation of constructive type theory, PhD thesis, Cornell
Univ., 1988.
*[Howe 1988b] D.J. Howe, Computational metatheory in Nuprul,
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. 238257.
*[Hsiang 1982] J. Hsiang, Topics in automated theorem proving
and program generation, PhD thesis, Report No. UIUCDCSR821113,
Dept. of Computer Science, Univ. of Illinois at UrbanaChampaign,
December 1982; also Artificial Intelligence 25(1985):255300.
[Hsiang 1983] J. Hsiang, N. Dershowitz, Rewrite methods for
clausal and nonclausal theorem proving, Proc. 10th EATCS Intl.
Conf. on Automata, Languages and Programming (Barcelona, Spain,
July 1983), LNCS 154, SpringerVerlag, Berlin, pp. 361373.
[Hsiang 1984] J. Hsiang, N.A. Josephson, TeRSe: A term rewriting
theorem prover, Proc. 6th Rewrite Rule Laboratory Workshop,
Schenectady, NY, 1983; also 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.
229243.
[Hsiang 1985a] J. Hsiang, Two results in term rewriting theorem
proving, Proc. 1st Conf. Rewriting Techniques and Applications
(Dijon, France, 2022 May 1985), ed. J.P. Jouannaud, LNCS 202,
SpringerVerlag, Berlin, 1985, pp. 301324.
*[Hsiang 1985b] J. Hsiang, Refutational theorem proving using
termrewriting systems, J. of Artificial Intelligence
25(3):255300, March 1985.
[Hsiang 1986a] J. Hsiang, M. Rusinowitch, A new method for
establishing refutational completeness in 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. 141152.
[Hsiang 1986b] J. Hsiang, M. Srivas, Prologbased inductive
theorem proving, Proc. 5th Conf. Foundations of Software
Technology and Theoretical Computer Science (New Delhi, India,
December 1985), ed. S.N. Maheshwari, LNCS 206, SpringerVerlag,
Berlin, 1985, pp. 129149.
*[Hsiang 1987a] J. Hsiang, M. Rusinowitch, On word problems in
equational theories, Department of Computer Science, SUNY at Stony
Brook, December 1986; also Proc. 14th Intl. Colloquium on
Automata, Languages, and Programming (ICALP '87, Karlsruhe, W.
Germany, 1317 July 1987), ed. T. Ottmann, LNCS 267,
SpringerVerlag, Berlin, 1987, pp. 5471.
[Hsiang 1987b] J. Hsiang, Rewrite method for theorem proving in
first order theory with equality, J. of Symbolic Computation 3(1
and 2):133151, February/April 1987.
[Hsiang 1987c] J. Hsiang,M. Rusinowitch, K. Sakai, Complete set
of inference rules for the cancellation laws, IJCAI 87, Milano,
Italy, 1987.
[Hsiang 1988a] J. Hsiang, J.P. Jounnaud, Complete sets of
inference rules for Eunification, Proc. 2nd Unificiation
Workshop, Val d'Ajol, France, 1988; also CRIN Report, Univ. de
Nancy, France.
[Hsiang 1988b] J. Hsiang, J. Mzali, SbReve user's guide,
Research report 457, Laboratoire du Recherche en Informatique,
Orsay, France, 1988.
*[Hsiang 1990] J. Hsiang, J.P. Jouannaud, Rewritebased theorem
proving (tutorial abstract), Proc. 10th Intl. Conf. on Automated
Deduction (CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes
in Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, p. 684.
[Hsiang 1991] J. Hsiang, M. Rusinowitch, Proving refutational
completeness of theoremproving strategies: the transfinite
semantic tree method, JACM 38(3):558586, July 1991.
*[Hua 1992] X. Hua, H. Zhang, FRI: FailureResistant Induction
in RRL, 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.
691695.
*[Huang 1989a] X. Huang, Proof transformation towards human
reasoning style, Proc. 13th German Workshop on Artificial
Intelligence (GWAI89, Eringerfeld, 1822 September 1989),
InformatikFachberichte 216, ed. D. Metzing, SpringerVerlag,
Berlin, 1989, pp. 3742.
[Huang 1989b] X. Huang, A human oriented proof presentation
model, SEKI Report SR8911, 1989.
[Huang 1990] X. Huang, Reference choices in mathematical proofs,
Proc. 9th European Conf. on Artificial Intelligence, ed. L.C.
Aiello, Pitman Publishing, London, 1990, pp. 720725.
[Huange 1984] Huange, C.H., Lengauer, C., The automated proof
of a trace transformation for a bitonic sort, TR8430, Dept. of
Computer Sciences, Univ. of Texas at Austin, October 1984.
[Huber 1971] H.G.M. Huber, A.H. Morris, Primary paramodulation,
NWL Tech. Rep. TR2552, Warfare Analysis Dept., Naval Weapons
Lab., Dahlgram, Virginia, 1971.
[Huet 1970] G. Huet, Experiments with an interactive prover for
logic with equality, Rep. 1106, Jennings Comput. Center, Case
Western Reserve Univ., Cleveland, Ohio, 1970.
[Huet 1972a] G.P. Huet, Constrained resolution: A complete
method for higher order logic, PhD thesis, Rep. 1117, Jennings
Comput. Center, Case Western Reserve Univ., Cleveland, 1972.
[Huet 1972b] G.P. Huet, The undecidability of the existence of a
unifying substitution between two terms in the simple theory of
types, Rep. 1120, Jennings Comput. Center, Case Western Reserve
Univ., Cleveland, Ohio, 1972.
[Huet 1973a] G.P. Huet, A mechanization of type theory, Proc.
3rd IJCAI, Stanford Univ., August 1973, pp. 139146; also
Theoretical Computer Science 1(1975):2558.
[Huet 1973b] G.P. Huet, The undecidability of unification in
third order logic, Information and Control 22(3):257267, 1973.
[Huet 1975] G.P. Huet, A unification algorithm for typed
lambdacalculus, Note de travail A055, Institut de Recherche
d'Informatique et d'Automatique, March 1974; also Rapport de
Recherche No. 23, INRIA, Le Chesnay; also Theoretical Computer
Science 1(1):2757, June 1975; also Proc. Symp. on lambdaCalculus
and Computer Science Theory (Rome, 1975), LNCS 37.
[Huet 1976] G. Huet, Algebraic aspects of unification, Automatic
Theorem Proving Workshop, Oberwolfach, W. Germany, 1976.
[Huet 1977] G. Huet, Confluent reductions: Abstract properties
and applications to term rewriting systems, Rapport de Recherche
250, Laboratoire de Recherche en Informatique et Automatique,
IRIA, France, August 1977; also Proc. 20th Symp. Foundations of
Computer Science, Providence, 1978, 3045; also JACM
27(4):797821, October 1980.
[Huet 1978a] G. Huet, D.S. Lankford, On the uniform halting
problem for term rewriting systems, TR 283, INRIA, Le Chesnay,
France, March 1978.
[Huet 1978b] G. Huet, An algorithm to generate the basis of
solutions to homogeneous linear diophantine equations, IRIA
Laboria, Rapport de Recherche No. 174, January 1978; also
Information Processing Letters 7(3):144147, 1978.
[Huet 1979] G. Huet, J.J. Levy, Callbyneed computations in
nonambiguous linear term rewriting systems, Tech. report 359,
INRIA, Le Chesnay, France, August 1979.
[Huet 1980a] G. Huet, A complete proof of correctness of the
KnuthBendix completion algorithm, INRIA Report 25, Le Chesnay,
France, July 1980; also J. of Computer and System Sciences
23(1):1121, August 1981.
[Huet 1980b] G. Huet, JM. Hullot, Proofs by induction in
equational theories with constructors, Rept. INRIA 28,
Rocquencourt, 1980; also Proc. 21st IEEE Symp. on Foundations of
Computer Science, Los Angeles, October 1980, pp. 96107; also in
J. of Computer and Science Systems 25(2):239266, 1982.
[Huet 1980c] G. Huet, D.C. Oppen, Equations and rewrite rules: A
survey, SRI Technical Report CSL111, 1980; also in Formal
Languages: Perspectives and Open Problems, ed. R. Book, NY:
Academic Press, 1980, pp. 349405.
[Huet 1982] G. Huet, J.M. Hullot, Proofs by induction in
equational theories with constructors, JComputer and System
Sciences 25(2):239266, 1982.
[Huet 1986a] G. Huet, Theorem proving systems of the formal
project, Proc. 8th Intl. Conf. on Automated Deduction (CADE8,
Oxford, England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS
230, SpringerVerlag, Berlin, 1986, pp. 687688.
[Huet 1986b] G. Huet, Formal structures for computation and
deduction, Tech. Report, INRIA, May 1986.
*[Huet 1986c] G. Huet, Deduction and computation, In
Fundamentals of Artificial Intelligence, ed. W. Bibel and Ph.
Jorrand, LNCS 232, SpringerVerlag, Berlin, 1986, pp. 3974.
*[Huet 1987] G. Huet, Induction principles formalized in the
calculus of constructions, 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. 276286;
also in Programming of Future Generation Computers, Elsevier,
1988, pp. 205216.
[Hullot 1979] J.M. Hullot, Associativecommutative pattern
matching, Proc. 6th IJCAI, Vol I, Tokyo, August 1979, pp. 406412.
[Hullot 1980a] J.M. Hullot, A catalogue of canonical term
rewriting systems, Research Rep. CSL113, SRI International, Menlo
Park, CA, April 1980.
[Hullot 1980b] J.M. Hullot, Canonical forms and unification,
Proc. 5th Workshop on Automated Deduction, ed. W. Bibel and R.
Kowalski, LNCS 87, SpringerVerlag, Berlin, July 1980, pp.
318334.
[Hunt 1966] E.H. Hunt, J. Marin, P.J. Stone, Experiments in
induction, Academic Press, NY, 1966.
[Hunt 1968] F.M. Hunt, J.R. Quinland, A formal deductive problem
solving system, JACM 15(4):625546, 1968.
[Hunt 1987] W.A. Hunt Jr., The mechanical verification of
microprocessor design, in From HDA Description to Guaranteed
Correct Circuit Designs, ed. D. Borrione, NorthHolland, IFIP,
1987, pp. 89129.
*[Hunt 1989] W.A. Hunt Jr., Microprocessor design verification,
J. Automated Reasoning 5(4):429460, December 1989.
[Hurt 1970] M. Hurt, C. Waid, A generalized inverse which gives
all the integer solutions, SIAM J. Appl. Math. 19(1970):547550.
*[Hussmann 1985a] H. Hussmann, Unification in conditional
equational theories, Report MIP8502, Universitat Passau, January
1985; also short version in 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. 543553.
[Hussmann 1985b] H. Hussmann, Rapid prototyping for algebraic
specifications  RAP system user's manual, Report MIP8504,
Universitat Passau, Passau, 1985; Second edition, February 1987.
[Hussmann 1986a] H. Hussmann, The Passau RAP System: Prototyping
algebraic specifications using conditional narrowing, Proc. 8th
Intl. Conf. on Automated Deduction (CADE8, Oxford, England, July
27August 1, 1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag,
Berlin, 1986, pp. 689690.
[Hussmann 1986b] H. Hussmann, Rapid prototyping for algebraic
specifications  RAP system user's manual Version 2.0, Draft,
Universitat Passau, 1986.
*[Hussmann 1988] H. Hussmann, The Passau RAP system: Rapid
prototyping 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. 264265.
*[Hutter 1986] D. Hutter, Using resolution and paramodulation
for induction proofs, Interner Bericht 6/86, Universitat
Karlsruhe, Institut fur Informatik I, 1986; also Proc. 10th GWAI
und 2. Osterreichische ArtificialIntelligenceTagung
(Ottenstein/Niederosterreich, 2226 September 1986),
InformatikFachberichte 124, SpringerVerlag, Berlin, 1986, pp.
265276.
[Hutter 1989] D. Hutter, Complete induction, In Deduction
Systems in Artificial Intelligence, ed. K.H. Blasius and H.J.
Burckert, Ellis Horwood, 1989.
*[Hutter 1990] D. Hutter, Guiding induction proofs, 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. 147161.
*[Hutter 1992] D. Hutter, Adapting a resolution calculus for
inductive proofs, Proc. 10th ECAI (ECAI 92, Vienna, Austria, 37
August 1992), ed. B. Neumann, John Wiley & Sons, Chichester,
1992, pp. 6569.
[Iba 1990] H. Iba, Reasoning of geometric concepts based on
algebraic methods, PhD Thesis, University of Tokyo, 1990.
*[Iba 1991] H. Iba, H. Inoue, Reasoning of geometric concepts
based on algebraic constraintdirected methods, Proc. 12th Intl.
Conf. on Artificial Intelligence, Vol 1 (IJCAI91, Darling
Harbour, Sydney, Australia, 2430 August 1991), Morgan Kaufmann
Publ., Inc., 1991, pp. 143149.
[ICOT 1984] ICOT Working Group 5, Several Aspects of
Unification, ICOT TM46, 1984.
*[Inoue 1990a] K. Inoue, N. Helft, On theorem provers for
circumscription, 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. 212219.
*[Inoue 1990b] K. Inoue, Consequencefinding based on ordered
linear resolution, Tech. Report, ICOT Research Center, 1990; also
Proc. 12th Intl. Conf. on Artificial Intelligence, Vol 1
(IJCAI91, Darling Harbour, Sydney, Australia, 2430 August 1991),
Morgan Kaufmann Publ., Inc., 1991, pp. 158164.
*[Inoue 1992] K. Inoue, M. Koshimura, R. Hasegawa, Embedding
negation as failure into a model generation 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.
400415.
*[Inoue 1993] K. Inoue, Y. Ohta, R. Hasegawa, M. Nakashima,
Bottomup abduction by model generation, Proc. 13th IJCAI
(Chambery, France, 28 August3 September 1993), Vol 1, ed. R.
Bajscy, IJCAI, Inc., 1993, pp. 102108.
[Irani 1985] K.B. Irani, D.G. Shin, A manysorted resolution
based on extension of a firstorder language, Proc. 9th IJCAI, Los
Angeles, CA, August 1985, W. Kaufmann, Inc., pp. 11751177.
[Ireland 1992a] A. Ireland, A. Bundy, Using failure to guide
inductive proof, DAI Research Paper no. 613, Dept. of Artificial
Intelligence, Univ. of Edinburgh, 1992.
[Ireland 1992b] A. Ireland, A. Bundy, The use of planning
critics in mechanizing inductive proofs, Proc. Internat. Conf. on
Logic Programming and Automated Reasoning (LPAR 92, St.
Petersburg), Lecture Notes in Artificial Intelligence 624,
SpringerVerlag, 1992, pp. 178189; also DAI Research Paper 592,
Dept. of Artificial Intelligence, Univ. of Edinburgh.
[Isakowitz 1988] T. Isakowitz, J. Gallier, Rewriting in
ordersorted equational logic, Proc. of Logic Programming Conf.,
ed. R. Kowalski and K. Bowen, MIT Press, Seattle, USA, 1988.
*[Issar 1990] S. Issar, Pathfocused duplication: A search
procedure for general matings, Tech. Report, CarnegieMellon
Univ., Pittsburgh, February 1990; also Proc. 8th National Conf. on
Artificial Intelligence (AAAI90, July 29August 3, 1990), AAAI
Press/MIT Press, 1990, pp. 221226.
[Iturriaga 1967] R. Iturriaga, Contributions to mechanical
mathematics, PhD thesis, CarnegieMellon Univ., 1967.
[Jackson 1987] P. Jackson, H. Reichgelt, A general proof method
for firstorder modal logic, Proc. 10th IJCAI (Los Altos, CA), ed.
J. McDermott, Morgan Kaufmann Inc., 1987, pp. 942944.
[Jackson 1988a] P. Jackson, H. Reichgelt, A general proof method
for modal predicate logic without Barcan formula or its converse,
DAI Research Report No. 370, Dept. of Artificial Intelligence,
Edinburgh Univ., 1988.
*[Jackson 1988b] P. Jackson, A general proof method for modal
predicate logic without the Barcan formula, Proc. AAAI88, 7th
National Conf. on Artificial Intelligence, Vol. 1, St. Paul,
Minnesota, 2126 August 1988, pp. 177181.
*[Jackson 1990] P. Jackson, J. Pais, Computing prime implicants,
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. 543557.
*[Jackson 1992] P. Jackson, Computing prime implicates
incrementally, 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. 253267.
*[Jacquet 1988] P. Jacquet, Program synthesis by completion with
dependent subtypes, 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. 550562.
[Jaffar 1981a] J. Jaffar, Presburger arithmetic with array
segments, Information Processing Letters 12(2):7982, April 1981.
[Jaffar 1981b] J. Jaffar, J.L. Lassez, A decision procedure for
theorems about multisets, Tech. Report 81/0, Dept. of Computer
Science, Univ. of Melbourne, November 1981, Submitted for
publication.
*[Jaffar 1982] J. Jaffar, J.L. Lassez, Reasoning about array
segments, Proc. ECAI82, Univ. ParisSud, Orsay, France, 1214
July 1982, pp. 6266.
[Jaffar 1984] J. Jaffar, Efficient unification over infinite
terms, New Generation Computing 2(3):207219, OHMSHA, Ltd., Tokyo,
1984.
[Jaffar 1985] J. Jaffar, Minimal and complete word unification,
Tech. Report 51, Dept. of Computer Science, Monash Univ., Clayton,
Victoria, Australia, March 1985.
[Jantke 1988] K. P. Jantke, M. Thomas, Inductive inference for
solving divergence in KnuthBendix completion, Internal report,
Univ. of Glasgow, 1988.
[Jantzen 1984] M. Jantzen, Thue Systems and the ChurchRosser
property, Proc. Mathematical Foundations of Computer Science
(Praha, Czechoslovakia), ed. M.P. Chytil and V. Koubek, LNCS 176,
SpringerVerlag, Berlin, 1984, pp. 8095.
*[Jantzen 1988] M. Jantzen, Confluent string rewriting,
SpringerVerlag, Berlin, Heidelberg, 1988.
*[Jenks 1976] R.D. Jenks, A pattern compiler, Proc. 1976 ACM
Symp. on Symbolic and Algebraic Computation (SYMSAC '76, Yorktown
Heights, NY, 1012 August 1976), ed. R.D. Jenks, ACM, 1133 Avenue
of the Americas, NY, NY 10036, 1976, pp. 6065.
[Jenks 1986] R.D. Jenks, Scratchpad II computer algebra system,
IBM Thomas J. Watson Research Center, Yorktown Heights, NY 10598,
1986.
[Jensen 1973] D. Jensen, T. Pietrzykowski, Mechanizing omega
order type theory through unification, Rep CS7316, Dept. of
Applied Analysis and Computer Science, Univ. of Waterloo, Ontario,
1973. also Theoretical Computer Science 3(1976):123171.
[Jerrum 1985] M. Jerrum, Random generation of combinatorial
structures for a uniform distribution (extended abstract), Proc.
Automata, Languages and Programming, LNCS, SpringerVerlag,
Berlin, 1985, pp. 290299.
[Jirku 1981] P. Jirku, Logical and linguistic aspects of
computerbased inference processes, Prague Bull. Math. Linguist
35(1981):4153, Czechoslovakia.
*[Johnson 1982] S.D. Johnson, A Computer System for Checking
Proofs, UMI Research Press, Ann Arbor, Michigan, 1982.
[Jones 1985] N.D. Jones, P. Sestoft, H. Sondergaad, An
experiment in partial evaluation: The generation of a compiler
generator, Proc. 1st Conf. Rewriting Techniques and Applications
(Dijon, France, 2022 May 1985), ed. J.P. Jouannaud, LNCS 202,
SpringerVerlag, Berlin, 1985. pp. 124140.
*[Jongh 1991] D. De Jongh, L. Hendriks, G.R. Renardel de
Lavalette, Computations in fragments of intuitionistic
propositional logic, J. Automated Reasoning 7(4):537561, December
1991.
*[Josephson 1986a] A. Josephson, N. Dershowitz, Efficient
implementations of narrowing: the RITE way, Internal Report, Univ.
of Illinois, 1986.
[Josephson 1986b] A. Josephson, N. Dershowitz, An implementation
of Narrowing: The RITE way, Report, Univ. of Illinois at Urbana,
1986; also Proc. 3rd IEEE Symp. on Logic Programming (Salt Lake
City, Utah, 2225 September 1986), pp. 187197 (revised version to
appear in J. of Logic Programming).
[Jouannaud 1981] J.P. Jouannaud, H. Kirchner, C. Kirchner,
Algebraic manipulations as a unification and matching strategy for
equations in signed binary trees, Proc. 7th IJCAI, Vancouver,
Canada, 1981.
[Jouannaud 1982a] J.P. Jouannaud, P. Lescanne, F. Reinig,
Recursive decompositions ordering and multiset ordering, Technical
Memo TM219, MIT Lab. for Computer Science, June 1982;
[Jouannaud 1982b] J.P. Jouannaud, P. Lescanne, F. Reinig,
Recursive decompositions ordering, Proc. 2nd IFIP Workshop on
Formal Description of Programming Concepts II
(GarmischPartenkirchen, W. Germany, June 1982), ed. D. Bjorner,
NorthHolland, 1982, pp. 331346.
[Jouannaud 1982c] J.P. Jouannaud, P. Lescanne, On multiset
ordering, Information Processing Letters 15(2):5763, 1982.
[Jouannaud 1982d] J. Jouannaud, C. Kirchner, H. Kirchner,
Incremental unification in equational theories, Universite de
Nancy, Informatique, 82R047, 1982; also Proc. of the Allerton
Conf. on Communication, Control and Computation, Univ. of
Illinois, Urbana Champaign, pp. 396405.
[Jouannaud 1983a] J.P. Jouannaud, H. Kirchner, C. Kirchner,
Incremental construction of unification algorithms in equational
theories, Proc. 10th EATCS Intl. Conf. on Automata, Languages and
Programming (Barcelona, Spain), ed. J. Diaz, LNCS 154,
SpringerVerlag, 1983, pp. 361373; also Internal Report 82R047,
Centre de Recherche en Informatique de Nancy, France.
[Jouannaud 1983b] J.P. Jouannaud, Confluent and coherent
equational term rewriting systems: Application to proofs in
abstract data types, Centre de Recherche en Informatique de Nancy
et Greco de Programmation, 1983; also in Proc. 8th Colloquium on
Trees in Algebra and Programming (CAAP'83), LNCS 59,
SpringerVerlag, Berlin, 1983.
[Jouannaud 1983c] J.P. Jouannaud, ChurchRosser computations
with equational term rewriting systems, Tech. report, CRIN, Nancy,
France, January 1983. Preliminary version in Proc. 5th CAAP, 1983,
to appear LNCS, SpringerVerlag, 1983.
[Jouannaud 1983d] J. Jouannaud, H. Kirchner, J. Remy,
ChurchRosser properties of weakly terminating term rewriting
systems, Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, pp.
909915.
[Jouannaud 1984a] J.P. Jouannaud, H. Kirchner, Completion of a
set of rules modulo a set of equations, Tech. report, SRI
International, 1984; also Proc. 11th ACM Principles of Programming
Languages Conf., Salt Lake City, Utah, January 1984, pp. 8392;
also SIAM J. of Computing, 15(4):11551194, 1986; also 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. 207228.
[Jouannaud 1984b] J.P. Jouannaud, M. Munoz, Termination of a set
of rules modulo a set of equations, Proc. 7th Intl. Conf. on
Automated Deduction (CADE7, Napa, CA, May 1984), ed. R.E.
Shostak, LNCS 170, SpringerVerlag, NY, 1984, pp. 175193.
[Jouannaud 1985a] J.P. Jouannaud, ed., Proc. 1st Conf. Rewriting
Techniques and Applications (Dijon, France, 2022 May 1985), LNCS
202, SpringerVerlag, Berlin, 1985.
[Jouannaud 1985b] J.P. Jouannaud, E. Kounalis, Proofs by
induction in equational theories without constructors, CRIN,
Nancy, France, May 1985; also Proc. IEEE Symp. on Logic in
Computer Science, Cambridge, MA, June 1986, pp. 358366. also
Information and Computation 82(1):133, 1989.
[Jouannaud 1986] J.P. Jouannaud, P. Lescanne, Rewriting
systems, Tech. Sci. Inform. 6(3):181199, 1987; translation from
French ``La reecriture'', Tech. Sci. Inform 5(6):433452, 1986.
[Jouannaud 1987] J.P. Jouannaud, B. Waldmann, Reductive
conditional term rewriting systems, Proc. 3rd IFIP Conf. on Formal
Description of Programming Concepts (Ebberup, Denmark, 1986), ed.
M. Wirsing, Elsevier Science Publishers, Amsterdam, 1987, pp.
223244.
[Jouannaud 1990a] J.P. Jouannaud, C. Kirchner, Solving
equations in abstract algebras: A rulebased survey of
unification, Research report, CRIN, 1990.
[Jouannaud 1990b] J.P. Jouannaud, C. Marche, Completion modulo
associativity, commutativity and identity (AC1). Proc. Int. Symp.
DISCO '90, LNCS 429, SpringerVerlag, Berlin, 111120.
[Joyner 1973] W.H. Joyner, Automatic theorem proving and the
decision problem, PhD dissertation, Harvard Univ., Cambridge, MA,
1973; also IEEE 14th Annual Symp. on Switching Automata Theory,
Iowa City, October 1973.
[Joyner 1976] W.H. Joyner jr., Resolution strategies as decision
procedures, JACM 23(1976):398417.
[Joyner 1979] W.H. Joyner, ed., Proc. 4th Workshop on Automated
Deduction, CADE4, Austin, Texas, 13 February 1979.
[Justen 1981] K. Justen, A note on regular resolution, Computing
26:8789, 1981.
[Jutting 1970a] L.S. Jutting, Definition of the language
AUTOMATH, Report, Tech. Hochschule Eindhoven, 1970.
[Jutting 1970b] L.S. Jutting, Example of a text written in
AUTOMATH, Report, Tech. Hochschule Eindhoven, 1970.
[Jutting 1976] L.S. Jutting, A translation of Landau's "Grundlagen"
in AUTOMATH, Eindhoven Univ. of Technology, Dept. of Math.,
October 1976.
[Jutting 1977] L.S. van Benthem Jutting, Checking Landau's
`Grundlagen' in the AUTOMATH system, Doctoral Thesis, Eindhoven
U., Eindhoven, The Netherlands, 1977; also in Mathematical Centre
Tracts 83, Mathematisch Centrum, Amsterdam, 1979.
