ORA Canada

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

ORA Canada Bibliography of Automated Deduction: Authors H to J

*[Hadzikadic 1986] M. Hadzikadic, F. Lichtenberger, D.Y.Y. Yun, An application of knowledge-base technology in education: A geometry theorem prover, Proc. 1986 ACM-SIGSAM Symp. on Symbolic and Algebraic Computation (SYMSAC '86, Univ. of Waterloo, Waterloo, Ontario, 21-23 July 1986), ed. B.W. Char, ACM, New York, NY, 1986, pp. 141-147.

[Hager 1985] G.D. Hager, Computational aspects of proofs in modal logic, Ms-CIS-85-57, 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 (GWAI-89, Eringerfeld, 18-22 September 1989), ed. D. Metzing, Springer-Verlag, Berlin, 1989, pp. 83-91.

[Hagiya 1985] M. Hagiya, S. Hayashi, Some experiments on EKL, ICOT TM-101, 1985.

*[Hagiya 1990] M. Hagiya, Programming by example and proving by example using higher-order unification, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 588-602.

*[Hagiya 1991] M. Hagiya, Higher-order unification as a theorem proving procedure, In Logic Programming: Proc. 8th Intl. Conf., ed. K. Furukawa, The MIT Press, Cambridge, MA, 1991, pp. 270-284.

[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 (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 306-315.

[Haken 1984] A. Haken, The intractability of resolution, PhD thesis, Univ. of Illinois at Urbana-Champaign, 1984; also Theoretical Computer Science 39(1985):297-308.

[Hall 1966] D. Hall, Semantic heuristics in a first-order 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. GWAI-82, Informatik-Fachberichte 58, ed. Wahlster, Springer-Verlag, Berlin, 1982, pp. 167-176.

[Halpern 1987] H. Halpern, S. Owre, N. Proctor, W.P. Wilson, Muse - A computer assisted verification system, IEEE Transactions on Software Engineering SE-13(2):151-156, 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):86-143, 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 (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 598-607.

[Haralick 1980] R.M. Haralick, G.L. Elliott, Increasing tree search efficiency for constraint satisfaction problems, Artificial Intelligence 14(1980):263-313.

[Harel 1980] Harel, Kozen, Parikh, Process logic, expressiveness, decidability, completeness, FOCS 80(1980):129-142.

[Harmelen 1989] F. van Harmelen, The CLAM proof planner, user manual and programmer manual: version 1.4, Tech. Paper TP-4, Dept. of Artificial Intelligence, Edinburgh, 1989.

*[Harmelen 1991] F. van Harmelen, Meta-level 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, ECS-LFCS-87-23, Laboratory for the Foundations of Computer Science, Univ. of Edinburgh, 1987; also Proc. 2nd ACM-IEEE Symp. on Logic in Computer Science (Ithaca, NY, June 1987), IEEE Computer Society Press, 1987, pp. 194-204.

[Harrison 1977] M.C. Harrison, A hierarchical approach to theorem proving, Proc. 5th IJCAI, MIT, Cambridge, MA, 1977, pp. 529-533.

[Harrison 1978] M.C. Harrison, N. Rubin, Another generalization of resolution, JACM 25(3):341-351, 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 tactic-driven 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 (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 776-780.

[Hayes 1969] P. Hayes, A machine-oriented formulation of the extended functional calculus, Stanford Artificial Intelligence Project, Memo 86, Stanford Univ., Stanford, 1969.

[Hayes 1971] P. Hayes, R. Kowalski, Automatic theorem-proving, 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. 105-118.

[Hearn 1967] A.C. Hearn, REDUCE: A user-oriented interactive system for algebraic simplification, Interactive Systems for Experimental Applied Mathematics, NY: Academic Press, 1967, pp. 79-90.

[Hearn 1968] A.C. Hearn, The problem of substitution, IFIP 68, SRI-Memo-70, 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, 10-12 August 1976), ed. R.D. Jenks, ACM, 1133 Avenue of the Americas, NY, NY 10036, 1976, pp. 46-52.

[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):18-21, 1986.

[Heering 1988] J. Heering, P. Klint, Towards shorter algebraic specifications: a smiple language definition and its compilation to Prolog, Reprot CS-R8814, 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):157-171. *[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, 4-7 June 1990), IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 42-57.

[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 (GWAI-87, Geseke, September 28-October 2, 1987), ed. K. Morik, Springer-Verlag, Berlin, 1987, pp. 201-210.

*[Heisel 1988] M. Heisel, W. Reif, W. Stephan, Implementing verification strategies in the KIV-system, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 131-140.

*[Heisel 1990] M. Heisel, W. Reif, W. Stephan, Tactical theorem proving in program verification, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 117-131.

*[Helman 1988] P. Helman, R. Veroff, Designing deductive databases, J. of Automated Reasoning 4(1):29-68, March 1988.

*[Hendriks 1988] P.R.H. Hendriks, ASF system user's guide, Report CS-R8823, 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 Urbana-Champaign, Illinois, 1971.

[Henschen 1972] L.J. Henschen, N-sorted logic for automatic theorem proving in higher-order logic, Proc. ACM Conf., Boston, MA, 1972.

[Henschen 1974a] L. Henschen, L. Wos, Unit refutations and Horn sets, JACM 21(October 1974):590-605.

[Henschen 1974b] L. Henschen, R. Overbeek, L. Wos, A theorem-proving language for experimentation, CACM 17(6):308-314, June 1974.

[Henschen 1976] L. Henschen, Semantic resolution for Horn sets, IEEE Trans. on Computers C-25, August 1976.

[Henschen 1977] L.J. Henschen, W.M. Evangelist, Theorem proving by covering expressions, Proc. 5th IJCAI, MIT, Cambridge, MA, 1977, pp. 541-542; also JACM 26(3):385-400, 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. 30-37.

[Henschen 1980] L. Henschen, Challenge problem I, SIGART Newsletter 72(July 1980):30-31.

[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. 528-531.

[Henschen 1982] L.J. Henschen, S.A. Naqvi, Representing infinite sequences of resolvents in recursive first-order Horn databases, Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982, pp. 342-359.

[Henschen 1984] L.J. Henschen, S.A. Naqvi, Compiling queries in recursive first order databases, JACM 31(1):47-85, 1984.

[Henschen 1986] L. Henschen, H. Park, Indefinite and GCWA inference in indefinite deduction databases, Proc. AAAI-86, 5th Natl Conf. on Artificial Intelligence, Philadelphia, PA, 11-15 August 1986, pp. 191-197.

[Henzinger 1985] T.A. Henzinger, H. Hofbauer, PROOF-PAD: An interactive proof generating system using natural deduction, Proc. Osterreichische Artificial Intelligence-Tagung, Wien (24-27 September 1985), Informatik-Fachberichte 106, Springer-Verlag, Berlin, 1985, pp. 173-184.

[Hermann 1985] M. Hermann, I. Privara, On nontermination of Knuth-Bendix algorithm, Research Report VUSEI-AR-OPS-3/85, Institute of Socio-Economic Information and Automation, CS-842 21, Bratislava, Czechoslovakia, 1985; also Proc. Intl. Colloquium on Automata, Languages and Programming (Rennes, France, July 1986), ed. L. Kott, LNCS 226, Springer-Verlag, Berlin, 1986, pp. 146-156.

*[Hermann 1991] M. Hermann, C. Kirchner, H. Kirchner, Implementation of term rewriting systems, The Computer Journal 34(1):20-33, February 1991.

[Herold 1982] A. Herold, Universal unification and a class of equational theories, Proc. GWAI-82, Informatik-Fachberichte 58, ed. Wahlster, Springer-Verlag, Berlin, 1982, pp. 177-190.

[Herold 1983] A. Herold, Some basic notions of first order unification theory, Interner Bericht 15/83, Memo SEKI-83-II, Institut fur Informatik I, Universitat Karlsruhe, W. Germany, 1983.

[Herold 1985a] A. Herold, J.H. Siekmann, Unification in Abelian semigroups, SEKI Memo 85-III-KL, Fachbereich Informatik, Universitat Kaiserslautern, 1985; also J. of Automated Reasoning 3(3):247-283, September 1987.

[Herold 1985b] A. Herold, Combination of unification algorithms, Memo-SEKI-86-VIII-KL, Universitat Kaiserslautern, 1985; also Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 450-469.

*[Herold 1986] A. Herold, Narrowing techniques applied to idempotent unification, SEKI Report SR-86-16, Fachbereich Informatik, Universitat Kaiserslautern, August 1986; also Proc. 11th German Workshop on Artificial Intelligence (GWAI-87, Geseke, September 28-October 2, 1987), ed. K. Morik, Springer-Verlag, Berlin, 1987, pp. 231-240.

*[Herold 1987] A. Herold, Combination of unification algorithms in equational theories, PhD thesis, SEKI Report SR-87-05, Universitat Kaiserslautern, FRG, 1987.

[Hesketh 1991] J.T. Hesketh, Using middle-out reasoning to guide inductive theorem proving, PhD thesis, Univ. of Edinburgh, 1991.

*[Hesketh 1992] J. Hesketh, A. Bundy, A. Smaill, Using middle-out reasoning to control the synthesis of tail-resursive programs, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 310-324.

*[Heuillard 1988] T. Heuillard, Compiling conditional rewriting systems, Proc. 1st Intl. Workshop on Conditional Term Rewriting Systems (Orsay, France, 8-10 July 1987), ed. S. Kaplan and J.-P. Jouannaud, LNCS 308, Springer-Verlag, Berlin, 1988, pp. 111-128.

[Hewitt 1969] C. Hewitt, PLANNER: A language for proving theorems in robots, Proc. 1st IJCAI, Washington, D.C., 1969, pp. 295-301.

[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 MIT-AI-Lab report AI-TR-258, 1972.

[Hickey 1989] T. Hickey, S. Mudambi, Global compilation of Prolog, J. of Logic Programming 7(3):193-230, 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 lambda-calculus, Cambridge Univ. Press, Cambridge, 1986.

[Hines 1988a] L.M. Hines, Building-in Knowledge of Axioms, PhD Dissertation, Univ. of Texas, 1988.

*[Hines 1988b] L. Hines, Hyper-chaining and knowledge-based theorem proving, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 469-486.

[Hines 1989a] L.M. Hines, W.W. Bledsoe, The STRIVE prover, Tech. report ATP-100, 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 Strive-based subset prover, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 193-206.

*[Hines 1992] L.M. Hines, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 35-49.

*[Hintikka 1988] J. Hintikka, Model minimization -- An alternative to circumscription, J. of Automated Reasoning 4(1):1-14, March 1988.

[Hirata 1979] M. Hirata, T. Nishimura, A prover for parallel processes, Proc. 6th IJCAI, Tokyo, August 20-23, 1979, pp. 284-389.

*[Hirose 1986] K. Hirose, An approach to proof checker, Proc. 12th Symp. Mathematical Foundations of Computer Science (Bratislava, Czechoslovakia, 25-29 August 1986), ed. J. Gruska, B. Rovan and J Wiedermann, LNCS 233, Springer-Verlag, Berlin, pp. 113-127.

[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, 1-3 September 1971, pp. 553-559; also Artificial Intelligence 3(1972):165-174.

*[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, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 167-177.

[Hoffman 1971] G.R. Hoffman, G. Veenker, The unit-clause proof procedure with equality, Computing 7(1971):91-105.

[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. 169-179.

[Hoffmann 1982a] C.M. Hoffmann, M.J. O'Donnell, Pattern matching in trees, JACM 29(1):68-95, January 1982.

[Hoffmann 1982b] C.M. Hoffmann, M.J. O'Donnell, Programming with equations, ACM ToPLaS 4(1):83-112, 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. 111-121.

[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):1185-1203, 1985.

[Holldobler 1985] S. Holldobler, U. Furbach, T. Laussermair, Extended unification and its implementation, GWAI '85, IFB 118, 1986, pp. 176-185.

*[Holldobler 1987a] S. Holldobler, A unification algorithm for confluent theories, Proc. 14th Intl. Colloquium on Automata, Languages, and Programming (ICALP '87, Karlsruhe, W. Germany, 13-17 July 1987), ed. T. Ottmann, LNCS 267, Springer-Verlag, Berlin, pp. 31-41.

[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, Springer-Verlag, Berlin, 1987.

*[Holldobler 1990] S. Holldobler, A structured connectionist unification algorithm, Proc. 8th National Conf. on Artificial Intelligence (AAAI-90, July 29-August 3, 1990, 1990), Vol. 2, AAAI Press/The MIT Press, Menlo Park/Cambridge, pp. 587-593.

[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. 400-402.

[Hong 1985] R. Hong, Research in intelligent robots, J. of Automated Reasoning 1(1):13-16, D. Reidel Publ. Co., Dordrecht, Holland, 1985.

[Hook 1989] J. Hook and G. Pottinger, Ulysses theories: the modular implementation of mathematics, Tech. Report TR 11-14, 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):14-21.

[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. GWAI-81, Informatik-Fachberichte 47, ed. Siekmann, Springer-Verlag, Berlin, 1981, pp. 248-255.

[Hornig 1982] K.M. Hornig, W. Bibel, Improvements of a tautology-testing program, Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982, pp. 326-341.

[Hornung 1981] G. Hornung, A. Knapp, and U. Knapp, A parallel connection graph proof procedure, German Workshop on Artificial Intelligence, LNCS, Springer-Verlag, Berlin, 1981, pp. 160-167.

[Howe 1986] D.J. Howe, Implementing number theory: An experiment with Nupri, Report 86-752, Dept. of Computer Science, Cornell Univ., May 1986; also Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 404-415.

[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 (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 238-257.

*[Hsiang 1982] J. Hsiang, Topics in automated theorem proving and program generation, PhD thesis, Report No. UIUCDCS-R-82-1113, Dept. of Computer Science, Univ. of Illinois at Urbana-Champaign, December 1982; also Artificial Intelligence 25(1985):255-300.

[Hsiang 1983] J. Hsiang, N. Dershowitz, Rewrite methods for clausal and non-clausal theorem proving, Proc. 10th EATCS Intl. Conf. on Automata, Languages and Programming (Barcelona, Spain, July 1983), LNCS 154, Springer-Verlag, Berlin, pp. 361-373.

[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. 229-243.

[Hsiang 1985a] J. Hsiang, Two results in term rewriting theorem proving, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985, pp. 301-324.

*[Hsiang 1985b] J. Hsiang, Refutational theorem proving using term-rewriting systems, J. of Artificial Intelligence 25(3):255-300, 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 (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 141-152.

[Hsiang 1986b] J. Hsiang, M. Srivas, Prolog-based 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, Springer-Verlag, Berlin, 1985, pp. 129-149.

*[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, 13-17 July 1987), ed. T. Ottmann, LNCS 267, Springer-Verlag, Berlin, 1987, pp. 54-71.

[Hsiang 1987b] J. Hsiang, Rewrite method for theorem proving in first order theory with equality, J. of Symbolic Computation 3(1 and 2):133-151, 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 E-unification, 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, Rewrite-based theorem proving (tutorial abstract), Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, p. 684.

[Hsiang 1991] J. Hsiang, M. Rusinowitch, Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method, JACM 38(3):558-586, July 1991.

*[Hua 1992] X. Hua, H. Zhang, FRI: Failure-Resistant Induction in RRL, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 691-695.

*[Huang 1989a] X. Huang, Proof transformation towards human reasoning style, Proc. 13th German Workshop on Artificial Intelligence (GWAI-89, Eringerfeld, 18-22 September 1989), Informatik-Fachberichte 216, ed. D. Metzing, Springer-Verlag, Berlin, 1989, pp. 37-42.

[Huang 1989b] X. Huang, A human oriented proof presentation model, SEKI Report SR-89-11, 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. 720-725.

[Huange 1984] Huange, C.-H., Lengauer, C., The automated proof of a trace transformation for a bitonic sort, TR-84-30, 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. TR-2552, 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. 139-146; also Theoretical Computer Science 1(1975):25-58.

[Huet 1973b] G.P. Huet, The undecidability of unification in third order logic, Information and Control 22(3):257-267, 1973.

[Huet 1975] G.P. Huet, A unification algorithm for typed lambda-calculus, 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):27-57, June 1975; also Proc. Symp. on lambda-Calculus 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, 30-45; also JACM 27(4):797-821, 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):144-147, 1978.

[Huet 1979] G. Huet, J.J. Levy, Call-by-need computations in non-ambiguous linear term rewriting systems, Tech. report 359, INRIA, Le Chesnay, France, August 1979.

[Huet 1980a] G. Huet, A complete proof of correctness of the Knuth-Bendix completion algorithm, INRIA Report 25, Le Chesnay, France, July 1980; also J. of Computer and System Sciences 23(1):11-21, August 1981.

[Huet 1980b] G. Huet, J-M. 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. 96-107; also in J. of Computer and Science Systems 25(2):239-266, 1982.

[Huet 1980c] G. Huet, D.C. Oppen, Equations and rewrite rules: A survey, SRI Technical Report CSL-111, 1980; also in Formal Languages: Perspectives and Open Problems, ed. R. Book, NY: Academic Press, 1980, pp. 349-405.

[Huet 1982] G. Huet, J.M. Hullot, Proofs by induction in equational theories with constructors, JComputer and System Sciences 25(2):239-266, 1982.

[Huet 1986a] G. Huet, Theorem proving systems of the formal project, Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 687-688.

[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, Springer-Verlag, Berlin, 1986, pp. 39-74.

*[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, 23-27 March 1987), Vol. I, ed. H. Ehrig, R. Kowalski, G. Levi, and U. Montanari, LNCS 249, Springer-Verlag, Berlin, 1987, pp. 276-286; also in Programming of Future Generation Computers, Elsevier, 1988, pp. 205-216.

[Hullot 1979] J.M. Hullot, Associative-commutative pattern matching, Proc. 6th IJCAI, Vol I, Tokyo, August 1979, pp. 406-412.

[Hullot 1980a] J.M. Hullot, A catalogue of canonical term rewriting systems, Research Rep. CSL-113, 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, Springer-Verlag, Berlin, July 1980, pp. 318-334.

[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):625-546, 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, North-Holland, IFIP, 1987, pp. 89-129.

*[Hunt 1989] W.A. Hunt Jr., Microprocessor design verification, J. Automated Reasoning 5(4):429-460, December 1989.

[Hurt 1970] M. Hurt, C. Waid, A generalized inverse which gives all the integer solutions, SIAM J. Appl. Math. 19(1970):547-550.

*[Hussmann 1985a] H. Hussmann, Unification in conditional equational theories, Report MIP-8502, Universitat Passau, January 1985; also short version in Proc. European Conf. on Computer Algebra (EUROCAL '85, Linz, Austria, 1-3 April 1985), Vol. 2: Research Contributions, ed. B.F. Caviness, LNCS 204, Springer-Verlag, Berlin, pp. 543-553.

[Hussmann 1985b] H. Hussmann, Rapid prototyping for algebraic specifications - RAP system user's manual, Report MIP-8504, 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 (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 689-690.

[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, 8-10 July 1987), ed. S. Kaplan and J.-P. Jouannaud, LNCS 308, Springer-Verlag, Berlin, 1988, pp. 264-265.

*[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 Artificial-Intelligence-Tagung (Ottenstein/Niederosterreich, 22-26 September 1986), Informatik-Fachberichte 124, Springer-Verlag, Berlin, 1986, pp. 265-276.

[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 (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 147-161.

*[Hutter 1992] D. Hutter, Adapting a resolution calculus for inductive proofs, Proc. 10th ECAI (ECAI 92, Vienna, Austria, 3-7 August 1992), ed. B. Neumann, John Wiley & Sons, Chichester, 1992, pp. 65-69.

[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 constraint-directed methods, Proc. 12th Intl. Conf. on Artificial Intelligence, Vol 1 (IJCAI-91, Darling Harbour, Sydney, Australia, 24-30 August 1991), Morgan Kaufmann Publ., Inc., 1991, pp. 143-149.

[ICOT 1984] ICOT Working Group 5, Several Aspects of Unification, ICOT TM-46, 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 (CSCSI-90, Univ. of Ottawa, Ottawa, Canada, 22-25 May 1990), published by CSCSI, 1990, pp. 212-219.

*[Inoue 1990b] K. Inoue, Consequence-finding based on ordered linear resolution, Tech. Report, ICOT Research Center, 1990; also Proc. 12th Intl. Conf. on Artificial Intelligence, Vol 1 (IJCAI-91, Darling Harbour, Sydney, Australia, 24-30 August 1991), Morgan Kaufmann Publ., Inc., 1991, pp. 158-164.

*[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 (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 400-415.

*[Inoue 1993] K. Inoue, Y. Ohta, R. Hasegawa, M. Nakashima, Bottom-up abduction by model generation, Proc. 13th IJCAI (Chambery, France, 28 August-3 September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 102-108.

[Irani 1985] K.B. Irani, D.G. Shin, A many-sorted resolution based on extension of a first-order language, Proc. 9th IJCAI, Los Angeles, CA, August 1985, W. Kaufmann, Inc., pp. 1175-1177.

[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, Springer-Verlag, 1992, pp. 178-189; also DAI Research Paper 592, Dept. of Artificial Intelligence, Univ. of Edinburgh.

[Isakowitz 1988] T. Isakowitz, J. Gallier, Rewriting in order-sorted equational logic, Proc. of Logic Programming Conf., ed. R. Kowalski and K. Bowen, MIT Press, Seattle, USA, 1988.

*[Issar 1990] S. Issar, Path-focused duplication: A search procedure for general matings, Tech. Report, Carnegie-Mellon Univ., Pittsburgh, February 1990; also Proc. 8th National Conf. on Artificial Intelligence (AAAI-90, July 29-August 3, 1990), AAAI Press/MIT Press, 1990, pp. 221-226.

[Iturriaga 1967] R. Iturriaga, Contributions to mechanical mathematics, PhD thesis, Carnegie-Mellon Univ., 1967.

[Jackson 1987] P. Jackson, H. Reichgelt, A general proof method for first-order modal logic, Proc. 10th IJCAI (Los Altos, CA), ed. J. McDermott, Morgan Kaufmann Inc., 1987, pp. 942-944.

[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. AAAI-88, 7th National Conf. on Artificial Intelligence, Vol. 1, St. Paul, Minnesota, 21-26 August 1988, pp. 177-181.

*[Jackson 1990] P. Jackson, J. Pais, Computing prime implicants, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 543-557.

*[Jackson 1992] P. Jackson, Computing prime implicates incrementally, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 253-267.

*[Jacquet 1988] P. Jacquet, Program synthesis by completion with dependent subtypes, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 550-562.

[Jaffar 1981a] J. Jaffar, Presburger arithmetic with array segments, Information Processing Letters 12(2):79-82, 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. ECAI-82, Univ. Paris-Sud, Orsay, France, 12-14 July 1982, pp. 62-66.

[Jaffar 1984] J. Jaffar, Efficient unification over infinite terms, New Generation Computing 2(3):207-219, 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 Knuth-Bendix completion, Internal report, Univ. of Glasgow, 1988.

[Jantzen 1984] M. Jantzen, Thue Systems and the Church-Rosser property, Proc. Mathematical Foundations of Computer Science (Praha, Czechoslovakia), ed. M.P. Chytil and V. Koubek, LNCS 176, Springer-Verlag, Berlin, 1984, pp. 80-95.

*[Jantzen 1988] M. Jantzen, Confluent string rewriting, Springer-Verlag, 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, 10-12 August 1976), ed. R.D. Jenks, ACM, 1133 Avenue of the Americas, NY, NY 10036, 1976, pp. 60-65.

[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 CS73-16, Dept. of Applied Analysis and Computer Science, Univ. of Waterloo, Ontario, 1973. also Theoretical Computer Science 3(1976):123-171.

[Jerrum 1985] M. Jerrum, Random generation of combinatorial structures for a uniform distribution (extended abstract), Proc. Automata, Languages and Programming, LNCS, Springer-Verlag, Berlin, 1985, pp. 290-299.

[Jirku 1981] P. Jirku, Logical and linguistic aspects of computer-based inference processes, Prague Bull. Math. Linguist 35(1981):41-53, 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, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985. pp. 124-140.

*[Jongh 1991] D. De Jongh, L. Hendriks, G.R. Renardel de Lavalette, Computations in fragments of intuitionistic propositional logic, J. Automated Reasoning 7(4):537-561, 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, 22-25 September 1986), pp. 187-197 (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 TM-219, 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 (Garmisch-Partenkirchen, W. Germany, June 1982), ed. D. Bjorner, North-Holland, 1982, pp. 331-346.

[Jouannaud 1982c] J.P. Jouannaud, P. Lescanne, On multiset ordering, Information Processing Letters 15(2):57-63, 1982.

[Jouannaud 1982d] J. Jouannaud, C. Kirchner, H. Kirchner, Incremental unification in equational theories, Universite de Nancy, Informatique, 82-R-047, 1982; also Proc. of the Allerton Conf. on Communication, Control and Computation, Univ. of Illinois, Urbana Champaign, pp. 396-405.

[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, Springer-Verlag, 1983, pp. 361-373; also Internal Report 82-R-047, 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, Springer-Verlag, Berlin, 1983.

[Jouannaud 1983c] J.P. Jouannaud, Church-Rosser computations with equational term rewriting systems, Tech. report, CRIN, Nancy, France, January 1983. Preliminary version in Proc. 5th CAAP, 1983, to appear LNCS, Springer-Verlag, 1983.

[Jouannaud 1983d] J. Jouannaud, H. Kirchner, J. Remy, Church-Rosser properties of weakly terminating term rewriting systems, Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, pp. 909-915.

[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. 83-92; also SIAM J. of Computing, 15(4):1155-1194, 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. 207-228.

[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 (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 175-193.

[Jouannaud 1985a] J.P. Jouannaud, ed., Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), LNCS 202, Springer-Verlag, 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. 358-366. also Information and Computation 82(1):1-33, 1989.

[Jouannaud 1986] J.-P. Jouannaud, P. Lescanne, Rewriting systems, Tech. Sci. Inform. 6(3):181-199, 1987; translation from French ``La reecriture'', Tech. Sci. Inform 5(6):433-452, 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. 223-244.

[Jouannaud 1990a] J.-P. Jouannaud, C. Kirchner, Solving equations in abstract algebras: A rule-based 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, Springer-Verlag, Berlin, 111-120.

[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):398-417.

[Joyner 1979] W.H. Joyner, ed., Proc. 4th Workshop on Automated Deduction, CADE-4, Austin, Texas, 1-3 February 1979.

[Justen 1981] K. Justen, A note on regular resolution, Computing 26:87-89, 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.


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