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 F to G

[Evans 1968] T.G. Evans, A heuristic program to solve geometry analogy problems, Semantic Inform. Proc., ed. Minsky, MIT Press, 1968.

[Fages 1983a] F. Fages, G. Huet, Complete sets of unifiers and matchers in equational theories, Proc. 8th CAAP (L'Aquila, Italy, March 1983), ed. G. Ausiello and M. Protasi, LNCS 159, Springer-Verlag, Berlin, pp. 205-220; also Theoretical Computer Science 43(1):189-200, 1986.

[Fages 1983b] F. Fages, G. Huet, Unification and matching in equational theories, Proc. 8th CAAP (l'Aquilla, Italy, March 1983), ed. G. Ausiello and M. Protasi, LNCS 159, Springer-Verlag, Berlin, pp. 205-220; also in Theoretical Computer Science 43(1986):189-200.

[Fages 1984] F. Fages, Associative-communative unification, 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, p. 75; also Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 194-208; also INRIA Report CNRS-LITP4, 1983; also Technical report, INRIA, BP 105, 78153 le Chesnay, 1985; also J. of Symbolic Computation 3(3):257-275, June 1987.

[Farinas 1982a] L. Farinas del Cerro, A simple deduction method for modal logic, Information Processing Letters 14(2):49-51, 20 April 1982.

*[Farinas 1982b] L. Farinas del Cerro, A deduction method for modal logic, Proc. ECAI-82, Univ. Paris-Sud, Orsay, France, 12-14 July 1982, pp. 60-61.

[Farinas 1983] L. Farinas del Cerro, Temporal reasoning and termination of programs, Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, pp. 926-929.

[Farinas 1984] L. Farinas del Cerro, Resolution modal logics, Proc. of Advanced NATO Study Institute on Logics and Models for Verification and Specification of Concurrent Systems (La Colle-sur-Loup, France), October 1984, pp. 46-78.

[Farinas 1985] L. Farinas del Cerro, M. Orlowska, eds., Automated reasoning in non-classical logic, Special double issue of Logique et Analyse 28(1985):115-294.

[Farinas 1986] L. Farinas del Cerro, Molog, a system that extends Prolog with modal logic, New Generation Computing 4(1986):35-50.

[Farinas 1987] L. Farinas del Cerro, M. Pentonen, A note on the complexity of satisfiability of modal Horn clauses, J. of Logic Program 4(1), March 1987.

*[Farinas 1988a] L. Farinas del Cerro, A. Herzig, Linear modal deductions, 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. 487-499.

[Farinas 1988b] L. Farinas, A. Herzig, Quantified modal logic and unification theory, Rapport Technique LSI no. 293, Universite P. Sabatier, Toulouse, France, 1988.

*[Farinas 1990] L. Farinas del Cerro, A. Herzig, Deterministic modal logics for automated deduction, Proc. 9th ECAI (Stockholm, Sweden, 6-10 August 1990), ed. L.C. Aiello, Pitman Publishing, London, 1990, pp. 262-267.

[Farmer 1984] W. Farmer, Length of proofs and unification theory, PhD thesis, University of Wisconsin, Madison, 1984.

[Farmer 1988a] W.M. Farmer, A unification algorithm for second-order monadic terms, Annals of Pure and Applied Logic 39(1988):131-174.

[Farmer 1988b] W.M. Farmer, A partial functions version of Church's simple theory of types, Tech. Report M88-52, The MITRE Corporation, 1988. Revised 1990; to appear in J. of Symbolic Logic.

[Farmer 1990a] W.M. Farmer, J.D. Guttman, F.J. Thayer, IMPS: An interactive mathematical proof system, Tech. Report M90-19, The MITRE Corporation, 1990.

*[Farmer 1990b] W.M. Farmer, J.D. Guttman, F.J. Thayer, IMPS: An interactive mathematical proof system (abstract), Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 653-654.

*[Farmer 1992a] W.M. Farmer, J.D. Guttman, F.J. Thayer, Little theories, 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. 567-581.

*[Farmer 1992b] W.M. Farmer, J.D. Guttman, F.J. Thayer, IMPS: System description, 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. 701-705.

*[Farreny 1982] H. Farreny, H. Prade, About flexible matching and its use in analogical reasoning, Proc. ECAI-82, Univ. Paris-Sud, Orsay, France, 12-14 July 1982, pp. 43-47.

*[Farreny 1988] H. Farreny, AI and Expertise: Heuristic Search, Inference Engines, Automatic Proving, Trans. J. Barchan, Ellis Horwoord Limited, Chichester, West Sussex, 1988.

*[Fateman 1971] R. Fateman, The user-level semantic matching capability in MACSYMA, Proc. 2nd Symp. on Symbolic and Algebraic Manipulation (Los Angeles, CA, March 23-25), ed. S.R. Petrick, ACM, NY, 1971, pp. 311-323.

[Fateman 1972] R.J. Fateman, Essays in algebraic simplification, PhD thesis, 1972; also Tech. Rep. MAC-TR-95, MIT, 545 Technology Square, Cambridge, MA, 1972.

[Fateman 1979] R.J. Fateman, MACSYMA's general simplifier: philosophy and operation, Proc. of the 1979 MACSYMA User's Conf. (MUC-79, Washington, DC, 20-22 June 1979), MIT Laboratory for Computer Science, 545 Technology Square, Cambridge, MA, 1979, pp. 563-582.

*[Fateman 1988] R. Fateman, A. Bundy, R. O'Keefe, I. Sterling, Commentary on: Solving symbolic equations with PRESS, SIGSAM Bulletin 22(2):27-40, issue 84, April 1988.

[Fateman 1989] R.J. Fateman, C. Ponder, Speed and data structures in computer algebra systems, ACM SIGSAM Bulletin 23(2):8-11, April 1989.

*[Fateman 1991] R.J. Fateman, Canonical representations in Lisp and applications to computer algebra systems, Proc. 1991 Intl. Symp. on Symbolic and Algebraic Computation (ISSAC '91, Bonn, Germany, 15-17 July 1991), ACM Press, NY, NY, 1991, pp. 360-369.

[Fay 1979] M. Fay, First order unification in an equational theory, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979, pp. 161-167.

[Fearnley-Sander 1985] D. Fearnley-Sander, Using and computing symmetry in geometry proofs, DAI Research Paper 257, Dept. of Artificial Intelligence, Edinburgh, 1985; also Proc. AISB-85, ed. P. Ross, Warwick, 1985.

*[Fearnley-Sander 1989] D. Fearnley, Sander, The idea of a diagram, In: Resolution of Equations in Algebraic Structures: Vol 1, Algebraic Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 127-150.

*[Fehrer 1990] D. Fehrer, A resolution calculus for a logic based on vaguely defined predicates, Proc. 9th ECAI (Stockholm, Sweden, 6-10 August 1990), ed. L.C. Aiello, Pitman Publishing, London, 1990, pp. 268-273.

*[Fegaras 1992] L. Fegaras, T. Sheard, D. Stemple, Uniform traversal combinators: definition, use and properties, 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. 148-162.

[Feigenbaum 1963] E. Feigenbaum, J. Feldman, eds., Computers and Thought, McGraw-Hill, NY, 1963.

[Feldman 1988a] Y.A. Feldman, C. Rich, Bread, frappe, and cake: The gourmet's guide to automated deduction, Porc. 5th Israeli Sypm. on Artificial Intelligence, Vision, and Pattern Recognition, Tel Aviv, Israel, December 1988.

[Feldman 1988b] Y.A. Feldman, C. Rich, Pattern-directed invocation with changing equalities, Memo 1017, MIT Artificial Intelligence Lab., May 1988.

[Feldman 1989] Y.A. Feldman, C. Rich, Principles of knowledge representation and reasoning in the FRAPPE system, Proc. 6th Israeli Symp. on Artificial Intelligence and Computer Vision, Tel Aviv, Israel, December 1989.

*[Feldman 1991] Y.A. Feldman, C. Rich, Pattern-directed invocation with changing equations, J. Automated Reasoning 7(3):403-433, September 1991.

*[Feldman 1993] Y.A. Feldman, H. Schneider, Simulating reactive systems by deduction, ACM Trans. on Software Engineering and Methodology 2(2):128-175, April 1993.

[Felty 1986] A.P. Felty, Using extended tactics to do proof transofrmations, Tech. Report MS-CIS-86-89, Dept. of Computer and Information Science, Univ. of Pennsylvania, 1986. *[Felty 1988a] A. Felty, D. Miller, Specifying theorem provers in a higher-order logic programming language, 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. 61-80.

*[Felty 1988b] A. Felty, et al., Lambda Prolog: an extended logic programming language, 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. 754-755.

*[Felty 1990a] A. Felty, D. Miller, Encoding a dependent-type lambda-calculus in a logic programming language, 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. 221-235.

*[Felty 1990b] A. Felty, E. Gunter, D. Miller, F. Pfenning, Lambda Prolog (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. 682.

[Ferrante 1975] J. Ferrante, C. Rackoff, A decision procedure for the first order theory of real addition with order, SIAM J. Comput. 4(1):69-76, 1975.

[Ferro 1978] A. Ferro, E.G. Omodeo, An efficient validity test for formulae in extensional two-level syllogistic, Le Matematiche (Catania, Italy) 33(1978):130-137.

*[Ferro 1980a] A. Ferro, E.G. Omodeo, J.T. Schwartz, Decision procedures for some fragments of set theory, Proc. 5th Conf. on Automated Deduction (Les Arcs, France, 8-11 July 1980), ed. W. Bibel and R. Kowalski, LNCS 87, Springer-Verlag, Berlin, 1980, pp. 88-96.

*[Ferro 1980b] A. Ferro, E.G. Omodeo, J.T. Schwartz, Decision procedures for elementary sublanguages of set theory. I: Multi-level syllogistic and some extensions, Commun. Pure and Appl. Math. 33(5):599-608, 1980.

[Ferro 1980c] A. Ferro, E.G. Omodeo, J.T. Schwartz, Decision procedures for some fragments of set theory, Proc. 5th Conf. on Automated Deduction (Les Arcs, France, 8-11 July 1980), ed. W. Bibel and R. Kowalski, LNCS 87, Springer-Verlag, Berlin, 1980, pp. 88-96.

[Ferro 1981] A. Ferro, Decision procedures for some classes of unquantified set theoretic formulae, PhD thesis, Courant Institute, New York Univ., 1981.

[Ferro 1985] A. Ferro, A note on the decidability of MLS extended by the powerset operator, Comm. Pure Appl. Math. 38(1985): 367-374.

[Ferro 1987] A. Ferro, E.Omodeo, Decision procedures for elementary sublanguages of set theory. VII. Validity in set theory when a choice operator is present, Comm. Pure Appl. Math. 40(1987):265-280.

*[Ferro 1990] G.C. Ferro, G. Gallo, A procedure to prove statements in differential geometry, J. Automated Reasoning 6(2):203-209, June 1990.

*[Ferro 1991] A. Ferro, Decision procedures for elementary sublanguages of set theory: XII. Multilevel syllogistic extended with singleton and choice operators, J. of Automated Reasoning 7(2):257-270, June 1991.

*[Ferscha 1987] A. Ferscha, A matrix-approach for proving inequalities, Proc. European Conf. on Computer Algebra (EUROCAL '87, Leipzig, GDR, 2-5 June 1987), ed. J.H. Davenport, LNCS 378, Springer-Verlag, Berlin, 1989, pp. 403-411.

[Feyock 1972] S. Feyock, A theorem proving system that learns from its failures, Canadian Comput. Conf. Session 1972, Montreal, 1972.

[Fiby 1979] R. Fiby, J. Sokol, M. Sudolsky, Efficient resolution theorem proving in the propositional logic, Comput. Linguist. and Comput. Lang. 13(1979):151-168, Hungary.

[Fikes 1970] R.E. Fikes, REF-ARF: A system for solving problems stated as procedures, Artificial Intelligence 1(1970):27-120.

[Fikes 1971] R.E. Fikes, N.J. Nilsson, STRIPS: A new approach to the application of theorem proving to problem solving, Proc. 2nd IJCAI, Imperial College, London, 1971, pp. 608-620; also Artificial Intelligence 2(Winter):189-208, 1971.

[Fikes 1977] R. Fikes, G. Hendrix, A network-based knowledge representation and its natural deduction system, Proc. 5th IJCAI, MIT, Cambridge, MA, 1977, pp. 235-246.

*[Fisher 1991] M. Fisher, A resolution method for temporal logic, 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. 99-104.

*[Fisher 1992] M. Fisher, A normal form for first-order temporal formulae, 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. 370-384.

[Fishman 1976] D.H. Fishman, Problem-oriented search procedure for theorem proving, IEEE Trans. on Computers 25(8):807-815, August 1976.

[Fitting 1972] M.C. Fitting, Tableau methods of proof for modal logics, Notre Dame J. of Formal Logic 13(1972):237-247.

[Fitting 1977] M.C. Fitting, A tableau system for propositional SS, Notre Dame J. of Formal Logic 18(1977):292-294.

[Fitting 1983] M.C. Fitting, Proof methods for modal and intuitionistic logics, Vol. 169 of Synthese Library, D. Reidel, Dordrecht, Holland, 1983.

[Fitting 1986] M. Fitting, A tableaux based automated theorem prover for classical logic, Tech. Report, CUNY, June 1986.

*[Fitting 1987] M.C. Fitting, Resolution for intuitionistic logic, Proc. 2nd Intl. Symp., Methodologies for Intelligent Systems (14-17 October 1987, Charlotte, North Carolina), ed. Z.W. Ras and M. Zemankova, North-Holland, Amsterdam, 1987, pp. 400-407.

*[Fitting 1988] M. Fitting, First-order modal tableux, J. Automated Reasoning 4(2):191-213, June 1988.

[Fitting 1989] M.C. Fitting, Negation as refutation, Proc. 4th Annual Symp. on Logic in Computer Science, IEEE Computer Society Press, 1989, pp. 63-70.

*[Fitting 1990] M. Fitting, First-Order Logic and Automated Theorem Proving, Springer-Verlag New York, Inc., New York, 1990.

[Fleisig 1974] S. Fleisig, D. Loveland, A.K. Smiley, D.L. Yarmash, An implementation of the model elimination proof procedure, JACM 21(January 1974):124-139.

[Foderaro 1981] J. Foderaro, R. Fatemen, Characterization of VAX Macsyma, Proc. 1981 ACM Symp. on Symbolic and Algebraic Comp. (Snowbird, Utah), ed. P.S. Wang, August 1981, pp. 14-19.

*[Forgaard 1984a] R. Forgaard, D. Detlefs, A program for generating and analyzing term rewriting systems, Tech. Report MIT/LCS/TR-343, Master's Thesis, MIT Lab. for Computer Science, September 1984.

[Forgaard 1984b] R. Forgaard, J.V. Guttag, A term rewriting system generator with failure resistant Knuth-Bendix, Tech report, MIT Laboratory for Computer Science, MIT, Cambridge, MA, 1984.

[Forgaard 1984c] R. Forgaard, J.V. Guttag, REVE: A term rewriting system generator with failure-resistant Knuth-Bendix, 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. 5-31.

[Forgaard 1986] R. Forgaard, A program for generating and analyzing term rewriting systems, MIT/LCS/TR-343, Laboratory for Computer Science, MIT, 1986.

[Forgy 1980] C.L. Forgy, RETE: A fast algorithm for the many pattern/many object pattern match problem, Tech. Rep. 309, Carnegie-Mellon Univ., Pittsburgh, PA 15213, 1980; also Artificial Intelligence 19(1):17-38, 1982.

[Forster 1980] D. Forster, GTP: A graph-based theorem prover, Master's thesis, Univ. of Waterloo, Ontario, Canada, 1980.

[Forsythe 1984] K. Forsythe, S. Matwin, Implementation strategies for plan-based deduction, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 426-444.

[Fortenbacher 1981] A. Fortenbacher, M. Schreck, G. Wrightson, Implementation and results of a proof procedure for first-order modal logic, Interner Bericht, Institut fur Informatik, Univ. of Karlsruhe, 1981.

[Fortenbacher 1985] A. Fortenbacher, An algebraic approach to unification under associativity and commutativity, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985, pp. 381-397; also J. of Symbolic Computation 3(3):217-229, June 1987.

[Franova 1984] M. Franova, CM-Strategy-driven deductions for automatic programming, in ECAI-84, Advances in Artificial Intelligence, ed. T. O'Shea, Elsevier Science Publ. B.V. (North-Holland), 1984, pp. 573-576.

[Franova 1985] M. Franova, CM-Strategy: A methodology for inductive theorem proving or constructive well-generalize proofs, Proc. 9th IJCAI, Vol. 2, Los Angeles, CA, 18-23 August 1985, pp. 1214-1220.

*[Franova 1988] M. Franova, Fundamentals for a new methodology for inductive theorem proving: CM-construction of atomic formulae, Proc. 8th ECAI, Institut fur Informatik der Technischen Universitat Munchen, 1-5 August 1988. pp. 136-141.

[Franova 1993a] M. Franova, Y. Kodratoff, M. Gross, Constructive matching methodology: Formally creative or intelligent inductive theorem proving, Research note 837 of L.R.I., Univ. Paris-Sud, Bat. 490, 91405 Orsay Cedex, France, 1993.

[Franova 1993b] M. Franova, Y. Kodratoff, M. Gross, Constructive matching methodology: an extension and an application to a planning problem, Research note 838 of L.R.I., Univ. Paris-Sud, Bat. 490, 91405 Orsay Cedex, France, 1993.

*[Franova 1993c] M. Franova, Constructive matching methodology and automatic plan-construction revisited, Rapport de Recherche no. 874, Univ. de Paris Sud, Centre d'Orsay, Laboratoire de Recherche en Informatique, Bat. 490, 91405 Orsay, France, November 1993.

*[Franzen 1987] M. Franzen, L.J. Henschen, A new approach to universal unification and its application to AC-unification, Internal Report, Dept. of Comp. Sci., Northwestern Univ., Illinois, 1987; also Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 643-657.

[Franzen 1988] M. Franzen, L.J. Henschen, A unification algorithm for simple equational theories, Doctoral thesis, Northwestern Univ., forthcoming.

*[Freitag 1987] H. Freitag, M. Reinfrank, An efficeint interpreter for a rule-based non-monotonic deduction system, Proc. 11th German Workshop on Artificial Intelligence (GWAI-87, Geseke, September 28-October 2, 1987), ed. K. Morik, Springer-Verlag, Berlin, 1987, pp. 170-174.

[Fribourg 1983] L. Fribourg, A superposition oriented theorem prover, Tech. Report 11, LITP, 1983; also Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, pp. 923-925; also Theoretical Computer Science 35(1985):129-164.

[Fribourg 1984a] L. Fribourg, A narrowing procedure for theories with constructors, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 259-281.

[Fribourg 1984b] L. Fribourg, Oriented equational clauses as a programming language, Report 84002, Laboratories de Marcoussis, Marcoussis; also short version in Proc. 11th Intl. Colloquium on Automata, Languages and Programming (ICALP, Antwerpen, The Netherlands), LNCS 172, 1984, pp. 162-172.

[Fribourg 1984c] L. Fribourg, Handling function definition through innermost superposition and rewriting, Report 84-69 LITP, Universite Paris 7, 1984; also Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985, pp. 325-344.

*[Fribourg 1985] L. Fribourg, SLOG: A logic programming language interpreter based on clausal superposition and rewriting, Proc. 1985 Symp. Logic Programming, Boston, MA, 15-18 July 1985, pp. 172-184.

[Fribourg 1986a] L. Fribourg, A strong restriction of the inductive completion procedure, Proc. 13th Intl. Colloquium on Automata, Languages and Programming (Rennes, France, July 1986), ed. L. Kott, LNCS 226, Springer-Verlag, Berlin, 1986, pp. 105-115; revised appeared in J. Symbolic Computation 8(3):253-276, 1989.

[Fribourg 1986b] L. Fribourg, A strong restriction of the completion procedure for theories with constructors, In Intl. Colloquium on Automata, Languages and Programming, ed. L. Kott, LNCS 226, Springer-Verlag, 1986, pp. 105-115.

*[Fribourg 1988] L. Fribourg, On the use of conditional rewrite rules in inductive theorem proving, 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. 56-61.

[Fribourg 1989a] L. Fribourg, A strong restriction of the inductive completion procedure, J. Symbolic Computation 8(3):253-276, 1989.

*[Fribourg 1989b] L. Fribourg, Proofs by combinatory induction on recursively reducible expressions, In: Resolution of Equations in Algebraic Structures: Vol 2, Rewriting Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 117-140.

*[Fribourg 1991] L. Fribourg, Automatic generation of simplification lemmas for inductive proofs, In Logic Programming: Proc. 1991 Intl. Symp., ed. V. Saraswat and K. Ueda, The MIT Press, Cambridge, MA, 1991, pp. 103-116.

[Friedland 1985] P.E. Friedland, Y. Iwasaki, The concept and implementation of skeletal plans, J. of Automated Reasoning 1(2):161-208, D. Reidel Publ. Co., Dordrecht, Holland, 1985.

[Friedman 1954] J. Friedman, A new decision procedure in logic and its computer realization, PhD thesis, Harvard Univ., Cambridge, MA, 1954.

[Friedman 1963a] J. Friedman, A semi-decision procedure for functional calculus, JACM 10(1):1-24, 1963; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 331-354.

[Friedman 1963b] J. Friedman, A computer program for a solvable case of the decision problem, JACM 10(3):348-356, 1963; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 355-363.

[Friedman 1964] J. Friedman, A new decision procedure in logic and its computer realization, PhD, Harvard Univ., Cambridge, MA, 1964.

[Friedman 1965] J. Friedman, Computer realization of a decision procedure in logic, Proc. IFIP Congr. 65, 1965, pp. 327-328.

[Frisch 1985] A.M. Frisch, An investigation into inference with restricted quantification and a taxonomic representation, SIGART Newsletter 91(1985):28-31.

[Frisch 1989] A.M. Frisch, A general framework for sorted deduction: Fundamental results on hybrid reasoning. Proc. 1st Intl.. Conf. on Principles of Knowledge Representation and Reasoning, ed. R.J. Brachman, H.J. Levesque, and R. Reiter, Toronto, Ontario, May 1989, pp. 126-136.

[Frisch 1990] A.M. Frisch, A.G. Cohn, A universal algorithm for sorted unification, Proc. Unif`90, Leeds, England, 1990.

*[Frisch 1991] A.M. Frisch, The substitutional framework for sorted deduction: fundamental results on hybrid reasoning, Artificial Intelligence 49(1-3):161-198, May 1991.

*[Frisch 1992] A.M. Frisch, An abstract view of sorted unification, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 178-192.

[Fronhofer 1986] B. Fronhofer, On refinements of the connection method, Proc. Algebra, Combinatorics and Logic in Computer Science (Gyor, Hungary, 1983), Colloq. Math. Soc., Vol. 42., North-Holland, Amsterdam-New York, 1986, pp. 391-401.

[Fuchs 1988] H. Fuchs, M. Pegueno, M. Sadler, A dialogic framework for theorem proving, Research report 88/4, Dept. of Computing, Imperial College of Science, Technology and Medicine, 180 Queen's Gate, London SW7 2BZ, England, 1988.

*[Fujita 1993] M. Fujita, J. Slaney, F. Bennett, Automatic generation of some results in finite algebra, Proc. 13th IJCAI (Chambery, France, 28 August-3 September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 52-59.

[Funt 1973] B.V. Funt, P procedural approach to constructions in Euclidean geometry, Unpublished MSc thesis, Univ. of British Columbia, October 1973.

*[Furbach 1987] Ulrich Furbach, Oldy but goody - paramodulation revisited, Proc. 11th German Workshop on Artificial Intelligence (GWAI-87, Geseke, September 28-October 2, 1987), ed. K. Morik, Springer-Verlag, Berlin, 1987, pp. 195-200.

*[Furbach 1989a] U. Furbach, S. Holldobler, J. Schreiber, Linear paramodulation modulo equality, Proc. 13 German Workshop on Artificial Intelligence (GWAI-89, Eringerfeld, 18-22 September 1989), ed. D. Metzing, Springer-Verlag, Berlin, 1989, pp. 107-116.

*[Furbach 1989b] U. Furbach, S. Holldobler, J. Schreiber, Horn equational theories and paramodulation, J. Automated Reasoning 5(3):309-337, September 1989.

*[Furukawa 1986] A. Furukawa, T. Sasaki, H. Kobayashi, The Grobner basis of a module over K[X1,...Xn] and polynomial solutions of a system of linear equation, 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. 222-224.

[Futatsugi 1985] K. Futatsugi, J. Goguen, J.-P. Jouannaud, J. Meseguer, Principles of OBJ2, Proc. 12th ACM Symp. on Principles of Programming Languages, ed. B. Reid, New Orleans, Louisiana, ACM, 1985, pp. 52-66.

[Gabbay 1988] D.M. Gabbay, Elements of algorithmic proof, Research report, Dept. of Computing, Imperial College, London, 1988; To appear in Handbook of Logic in Theoretical Computer Science, ed. S. Abramsky, D. Gabbay, and T. Maibaum, Oxford University Press.

*[Gabbay 1991] D.M. Gabbay, F. Kriwaczek A family of goal directed theorem provers based on conjunction and implication: Part I, J. Automated Reasoning 7(4):511-536, December 1991.

[Gabow 1976] H. Gabow, An efficient implementation of Edmond's algorithm for maximum matching on graphs, JACM 23(1976):221-234.

*[Gabriel 1985] J. Gabriel, T. Lindholm, E.L. Lusk, R.A. Overbeek, A tutorial on the Warren abstract machine for computational logic, Tech. Report ANL-84-84, Argonne National Laboratory, Argonne, IL, June 1985.

[Gabriel 1986] J.R. Gabriel, SARA - A small automated reasoning assistant, Preprint, Argonne National Laboratory, 1986.

[Galil 1975] Z. Galil The complexity of resolution procedures for theorem proving in the propositional calculus, TR 75-239, PhD thesis, Dept. of Computer Science, Cornell Univ., 1975.

[Galil 1977a] Z. Galil, On the complexity of regular resolution and the Davis-Putnam procedure, Theoretical Computer Science 4(1977):23-46.

[Galil 1977b] Z. Galil, On resolution with clauses of bounded size, SIAM J. Computing 6(1977):44-459.

*[Galil 1991] Z. Galil, G. Italiano, Data structures and algorithms for disjoint set union problems, ACM Computing Surveys 23(3):319-344, September 1991.

[Gallaire 1978] H. Gallaire, J. Minker, Logic and Data Bases, Plenum, 1978.

*[Gallier 1984] J.H. Gallier, R.V. Book, Reductions in tree replacement systems, in Papers on Combinatorics of Words, Tech. Rep., Dept. of Math., UCSB Santa Barbara, 1984; also in Theoretical Computer Science 37(2):123-150, November 1985.

[Gallier 1985] J.H. Gallier, S. Raatz, Logic programming and graph rewriting, Proc. 2nd Symp. on Logic Programming, Boston, MA, 1985, pp. 208-219.

[Gallier 1986a] J.H. Gallier, A fast algorithm for testing unsatisfiability of Ground Horn clauses, MS-CIS-86-06, Univ. of Pennsylvania, 1986.

[Gallier 1986b] J.H. Gallier, S. Raatz, Extending SLD-Resolution to equational Horn clauses using E-Unification, MS-CIS-86-44, Univ. of Pennsylvania, 1986; also J. Logic Programming, 1986.

[Gallier 1986c] J.H. Gallier, S. Raatz, Horning: A graph based interpreter for general Horn clauses, MS-CIS-86-10, Univ. of Pennsylvania, 1986.

[Gallier 1986d] J.H. Gallier, S. Raatz, Refutation methods for Horn clauses with equality based on unification, MS-CIS-86-59, Univ. of Pennsylvania, 1986.

[Gallier 1986e] J.H. Gallier, Logic for computer science: Foundations of automatic theorem proving, New York, Harper and Row, 1986.

*[Gallier 1986f] J.H. Gallier, S. Raatz, SLD-resolution methods for Horn clauses with equality based on E-unification, Proc. Symp. on Logic Programming, Salt Lake City, Utah, 22-25 September 1986, pp. 168-179.

[Gallier 1987a] J.H. Gallier, S. Raatz, W. Snyder, Theorem proving using rigid E-unification: Equational matings, Proc. IEEE Symp. on Logic in Computer Science, Ithaca, NY, 22-25 June 1987, pp. 338-346; also Internal Report, Dept. of Computer and Information Science, Univ. of Pennsylvania, Philadelphia.

[Gallier 1987b] J.H. Gallier, W. Snyder, A general complete E-unification procedure, Proc. 2nd Intl. Conf. on Rewriting Techniques and Applications (Bordeaux, France, 25-27 May 1987), ed. P. Lescanne, LNCS 256, Springer-Verlag, Berlin, 1987, pp. 216-227.

*[Gallier 1987c] J.H. Gallier, Fast algorithms for testing unsatisfiability of Ground Horn clauses, J. of Symbolic Computation 4(2):233-254, October 1987.

*[Gallier 1988a] J. Gallier, W. Snyder, P. Narendran, D. Plaisted, Rigid E-unification is NP-complete, Proc. 3rd IEEE Symp. on Logic in Computer Science, Edinburgh, Scotland, 5-8 July 1988, pp. 218-227.

*[Gallier 1988b] J. Gallier, P. Narendran, D. Plaisted, S. Raatz, W. Snyder, Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time, 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. 182-196.

*[Gallier 1989a] J. Gallier, W. Snyder, S. Raatz, Rigid E-unification and its applications to equational matings, In: Resolution of Equations in Algebraic Structures: Vol 1, Algebraic Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 151-216.

[Gallier 1989b] J. Gallier, W. Snyder, Completion sets of transformations for general E-unification, Theor. Comput. Sci. 67(1989): 203-260.

[Gallier 1990] J. Gallier, W. Snyder, Designing unification procedures using transformations: A survey, EATCS Bulletin, 40(February 1990): 273-326.

[Gallier 1993] J. Gallier, P. Narendran, D. Plaisted, S. Raatz, W. Snyder, An algorithm for finding canonical sets of ground rewrite rules in polynomial time, J. ACM 40(1):1-16, January 1993.

*[Ganzinger 1987a] H. Ganzinger, Ground term confluence in parametric conditional equational specifications, Proc. 4th Annual Symp. on Theoretical Aspects of Computer Science (STACS'87, Passau, FRG, 19-21 February 1987), ed. F.J. Brandenburg, G. Vidal-Naquet and M. Wirsing, LNCS 247, 1987, pp. 286-298.

[Ganzinger 1987b] H. Ganzinger, A completion procedure for conditional equations Tech. Report 234, Univ. of Dortmund, 1987; also Proc. 1st Intl. Workshop on Conditional Term Rewriting Systems (Orsay, France, 8-10 July 1987), ed. S. Kaplan and J.-P. Jouannaud, LNCS 308, Springer-Verlag, Berlin, 1988, pp. 62-83; revised version to appear in J. Symb. Computation.

[Ganzinger 1987c] H. Ganzinger, R. Giegerich, A note on termination in combinations of heterogeneous term rewriting systems, EATCS Bulletin 31(1987):22-28.

[Ganzinger 1988a] H. Ganzinger, Completion with history-dependent complexities for generated equations, In Recent Trends in Data Type Specification, ed. Sannella and Tarlecki, Springer LNCS 332, 1988, pp. 73-91.

[Ganzinger 1988b] H. Ganzinger, Order-sorted completion: The many-sorted way, Report 274, FB Informatik, Univ. Dortmund, 1988. Extended abstract to appear in Proc. TAPSOFT(CAAP)'89, Barcelona.

*[Garland 1988] S.J. Garland, J.V. Guttag, LP: The Larch Prover, 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. 748-749.

[Garland 1988] S.J. Garland, J.V. Guttag, Inductive methods for reasoning about abstract data types, Proc. POPL '88, 1988, pp. 219-228.

*[Garland 1989] S.J. Garland, J.V. Guttag, An overview of LP, The Larch Prover, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 137-151.

[Garson 1980] J. Garson, P. Mellema, Computer-Assisted Instruction on Logic: EMIL, Teaching Philosophy, 1980, pp. 453-478.

[Gasteren 1988] A.J.M. van Gasteren, On the shape of mathematical arguments, PhD thesis, Eindhoven Univ. of Technology, 1988.

*[Gao 1990] X. Gao, Transcendental functions and mechanical theorem proving in elementary geometries, J. Automated Reasoning 6(4):403-417, December 1990.

[Gebauer 1984] R. Gebauer, H. Kredel, Buchberger algorithm system, SIGSAM Bulletin 18(1), 1984.

*[Gebauer 1986] R. Gebauer, H.M. Moller, Buchberger's algorithm and staggered linear bases, 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. 218-221.

*[Geissler 1986] C. Geissler, K. Konolege, A resolution method for quantified modal logics of knowledge and belief, Proc. Conf. on Theoretical Aspects of Reasoning about Knowledge, Monterey, CA, 19-22 March 1986, pp. 309-324.

[Gelder 1984] A. Van Gelder, A satisfiability tester for non-clausal propositional calculus, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 101-112; also UCSC-CRL-88-32, Univ. of California at Santa Clara, June 1988; also Information and Computation 79(1), October 1988.

[Gelernter 1958] H. Gelernter, N. Rochester, Intelligent behaviour in problem solving machines, IBM J. 2(October 1958):336-345.

[Gelernter 1959a] H. Gelernter, A note on syntactic symmetry and the manipulation of formal systems, Information and Control 2(March 1959).

[Gelernter 1959b] H.L. Gelernter, Realization of a geometry-theorem proving machine, Proc. Intl. Conf. on Information Processing, UNESCO House, 1959, pp. 273-282; also in Computers and Thought, ed. E.A. Feigenbaum and J. Feldman, McGraw-Hill, NY, 1963; also reprinted in Siekmann and Wrightson, 1983, pp. 99-117.

[Gelernter 1963a] H. Gelernter, Machine-generated problem-solving graphs, Proc. Symp. Math. Theory Automata, Polytechnic Press, NY, 1963, pp. 179-203; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 288-312.

[Gelernter 1963b] H. Gelernter, Realization of a geometry-theorem proving machine, Proc. Intl. Conf. Information Proc., UNESCO House, Paris, 1959, pp. 273-283; also in Computers and Thought, ed. E.A. Feigenbaum and J. Feldman, McGraw-Hill, NY, 1963, pp. 134-152; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 99-122.

[Gelernter 1963c] H. Gelernter, J. Hansen, D. Loveland, Empirical explorations of the geometry-theorem proving machine, Proc. West Joint Computer Conf., 1960, pp. 143-147, in Computers and Thought, ed. E.A. Feigenbaum and J. Feldman,, McGraw-Hill, NY, 1963, pp. 153-167; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 140-150.

[Gelperin 1973] D. Gelperin, Deletion directed search in resolution-based proof procedures, Proc. 3rd IJCAI, Stanford Univ., 1973, pp. 47-50.

[Gelperin 1976] D. Gelperin, A resolution-based proof procedure using deletion-directed search, IEEE Trans. on Computers C-25(4):323-327, April 1976.

[Genesereth 1983] M.R. Genesereth, R. Greiner, D.E. Smith, A meta-level representation system, Stanford, Memo HPP-83-28, May 1983.

*[Genesereth 1987] M.R. Genesereth, N.J. Nilsson, Logical Foundations of Artificial Intelligence, Morgan Kaufmann Publishers, Inc., Los Altos, CA 94022, 1987.

[Gentner 1983] D. Gentner, Structure mapping: A theoretical framework for analogy, Cognitive Science 7(2):155-170, April 1983.

[Gentzen 1935] G. Gentzen, Investigations into logical deduction, 1935, In The Collected Papers of Gerhard Gentzen, ed. M.E. Szabo, North-Holland, Amsterdam, 1969, pp. 68-131.

[Gergely 1978] T. Gergely, K.P. Vershinin, Model theoretical investigation of theorem proving methods, Notre Dame J. Formal Logic 19(4):523-542, October 1978.

[Gergely 1983] T. Gergely, K. Vershinin, Negative Hyper-resolution for proving statements containing transistive relations, Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, pp. 877-881.

[Gerhart 1980] S.L. Gerhart, et al., An overview of AFFIRM: a specification and verification system, Information Processing 80(October 1980):343-348, ed. S.H. Lavington, North-Holland.

[Geser 1985] A. Geser, H. Hussmann, Rapid prototyping for algebraic specifications - Examples for the use of the RAP system, MIP-8517, Universitat Passau, 1985.

*[Geser 1986] A. Geser, H. Hussmann, Experiences with the RAP System - A specification interpreter combining term rewriting and resolution, Proc. ESOP 86, 1st European Symp. on Programming (Saarbrucken, FRG, 17-19 March 1986), ed. B. Robinet and R. Wilhelm, LNCS 213, Springer-Verlag, Berlin, 1986, pp. 339-350.

*[Geser 1988] A. Geser, H. Hussmann, A. Mueck, A compiler for a class of conditional term 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. 84-90.

*[Geupel 1989] Oliver Geupel, Overlap closures and termination of term rewriting systems, Reprot MIP-8922, Fakultat fur Mathematik und Informatik, Universitat Passau, July 1989.

[Ghallab 1981] M. Ghallab, Decision trees for optimizing pattern-matching algorithms in production systems, Proc. IJCAI-81, Vancouver, BC, 1981, pp. 310-312.

*[Ghelfo 1985] S. Ghelfo, E.G. Omodeo, Towards practical implementations of syllogistic (Full paper), 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. 40-49.

[Gianni 1988] P. Gianni, B. Trager, G. Zacharias, Grobner bases and primary decomposition of polynomial ideals, J. Symbolic Computation 6(1988):149-169.

*[Gibbins 1988] P. Gibbins, Logic with Prolog, Clarendon Press, Oxford, 1988.

[Gibert 1986] J. Gibert, The J.Machine: Functional programming with combinators, 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. 683-684.

[Gilmore 1959] P.C. Gilmore, A procedure for the production from axioms of proofs for theories derivable within the first order predicate calculus, Proc. Intl. Conf. on Information Processing, UNESCO House, Paris, 1959, pp. 265-273.

[Gilmore 1960] P.C. Gilmore, A proof method for quantification theory: Its justification and realization, IBM J. Research and Development 4(January 1960):28-35; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 151-161.

[Gilmore 1970] P. Gilmore, An examination of the geometry theorem machine, Artificial Intelligence 1(Fall 1970):171-187.

[Ginsberg 1989] M.L. Ginsberg, A circumscriptive theorem prover, Artif. Intell. 39(2):209-230, June 1989.

*[Ginsberg 1990] M.L. Ginsberg, W.D. Harvey, Iterative broadening, Proc. 8th National Conf. on Artificial Intelligence (AAAI-90, July 29-August 3, 1990), AAAI Press/MIT Press, 1990, pp. 216-220; also Artif. Intell. 55(2-3):367-383, June 1992.

*[Giovannetti 1986] E. Giovannetti, C. Moiso, A completeness result for E-unification algorithms based on conditional narrowing, Proc. Foundations of Logic and Functional Programming (Trento, Italy, 15-19 December 1986), ed. M. Boscarol, L.C. Aiello, and G. Levi, LNCS 306, Springer-Verlag, 1988, pp. 157-167.

*[Giovannetti 1988] E. Giovannetti, C. Moiso, Notes on the elimination of conditions, 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. 91-97.

[Girard 1987] J.Y. Girard, Linear logic, Theoret. Comput. Sci. 50(1987):1-102.

*[Giunchiglia 1988] F. Giunchiglia, A. Giunchiglia, Building complex derived inference rules: a decider for the class of Prenex universal-existential formulas, Proc. 8th ECAI, Institut fur Informatik der Technischen Universitat, Munchen, 1-5 August 1988, pp. 607-609; Extended version available as DAI Research paper 359, Dept. of Artificial Intelligence, Edinburgh.

*[Giunchiglia 1989a] F. Giunchiglia, T. Walsh, Theorem proving with definitions, DAI Research Paper 429, Dept. of Artificial Intelligence, Univ. of Edinburgh, 1989; also Proc. 7th Conf. of the Society for the Study of Artificial Intelligence and Simulation Behaviour (AISB-89, Univ. of Sussex, 18-21 April 1989), ed. A.G. Cohn, Pitman Publ., London, 1989, pp. 175-183.

*[Giunchiglia 1989b] F. Giunchiglia, T. Walsh, Abstract theorem proving, Research paper 430, Dept. of Artificial Intelligence, Univ. of Edinburgh, 1989; also Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 372-377.

[Giunchiglia 1989c] F. Giunchiglia, A. Smaill, Reflection in constructive and non-constructive automated reasoning, Proc. Workshop on Meta-Programming in Logic Programming, ed. H. Abramson and M.H. Rogers, MIT Press, 1989, pp. 123-140; IRST Tech. Report 8902-04; also DAI Research Paper 375, Dept. of Artificial Intelligence, Edinburgh.

[Giunchiglia 1989d] F. Giunchiglia, T. Walsh, Abstract theorem proving: mapping back, DAI Research paper 460, Dept. of Artificial Intelligence, Univ. of Edinburgh, 1989.

[Giunchiglia 1989e] F. Giunchiglia, T. Walsh, Abstracting into inconsistent spaces (or, the "false proof" problem), In Proc. of 1st conf. of AI*IA, Associazione Italiana per l'Inteligenza Artificiale, 1989; also DAI Research Paper No. 429, Univ. of Edinburgh.

[Giunchiglia 1990a] F. Giunchiglia, T. Walsh, The use of abstraction in automatic inference, Research paper 454, Dept. of Artificial Intelligence, Univ. of Edinburgh, 1990.

[Giunchiglia 1990b] F. Giunchiglia, P. Traverso, Plan formation and execution in a uniform architecture of declarative metatheories, Proc. Workshop on Meta-Programming in Logic, ed. M. Bruynooghe, MIT Press, 1990; also IRST Tech. Report 9003-12.

[Giunchiglia 1990c] F. Giunchiglia, T. Walsh, A theory of abstraction, Research paper 516, Dept. of AI, Univ. Edinburgh, 1990; to be published in Artificial Intelligence.

[Giunchiglia 1990d] F. Giunchiglia, T. Walsh, Abstraction in automatic inference, In Proc. of the UK-IT 90 Conference, 1990, pp. 365-370.

*[Giunchiglia 1991a] F. Giunchiglia, P. Traverso, Reflective reasoning with and between a declarative metatheory and the implementation code, 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. 111-117.

[Giunchiglia 1991b] F. Giunchiglia, R.W. Weyhrauch, FOL user manual - FOL version 2, Tech. report 9107-05, DIST, Univ. of Genova, Genova, Italy, 1991.

[Giunchiglia 1991c] F. Giunchiglia, T. Walsh, Using abstractions, In Proc. of Society for the Study of Artificial Intelligence and Simulation of Behaviour (AISB-91, Leeds, UK), 1991; also IRST-Technical Report no. 9010-08; also DAI Research paper no. 515, Univ. of Edinburgh.

*[Giunchiglia 1992] F. Giunchiglia, T. Walsh, Tree subsumption: reasoning with outlines, Proc. 10th ECAI (ECAI 92, Vienna, Austria, 3-7 August 1992), ed. B. Neumann, John Wiley & Sons, Chichester, 1992, pp. 77-81.

[Glickfeld 1986] B. Glickfeld, R. Overbeek, A foray into combinatory logic, J. of Automated Reasoning 2(4):419-431, December 1986.

[Gloess 1980] P.Y. Gloess, An experiment with the Boyer-Moore theorem prover: A proof of the correctness of a simple parser of expressions, Proc. 5th Conf. on Automated Deduction (Les Arcs, France, 8-11 July 1980), ed. W. Bibel and R. Kowalski, LNCS 87, Springer-Verlag, Berlin, 1980, pp. 154-169.

[Glushkov 1972] V.M. Glushkov, Y.V. Kapitonova, Automatic search for proofs of mathematical theorems and intelligent computers, Kibernetika 8(5):2-6, USSR, September 1972.

[Gnaedig 1986] L. Gnaedig, P. Lescanne, Proving termination of associative commutative rewriting systems by rewriting, 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. 52-61.

[Gnaedig 1988] I. Gnaedig, Knuth-Bendix procedure and nondeterministic behavior - An example, Bulletin of the European Association for Theoretical Computer Science 32(1988):86-92.

[Gnaedig 1990] I. Gnaedig, H. Kirchner, Equational completion in order-sorted algebras, Theor. Comput. Sci. 72(2,3):169-202, May 1990.

[Goad 1980a] C. Goad, Proofs as descriptions of computation. Proc. 5th Conf. on Automated Deduction (Les Arcs, France), LNCS 87, Springer-Verlag, Berlin, 1980, pp. 39-52.

[Goad 1980b] C. Goad, Computational uses of the manipulation of formal proofs, Tech. report STAN-CS-80-819, Stanford Univ., 1980

[Gobel 1983] R. Gobel, Rewrite rules with conditions for algebraic specifications, Proc. 2nd Workshop on Theory and Applications of Abstract Data Types (Abstract), Passau, W. Germany, 1983.

[Gobel 1984] R. Gobel, A completion procedure for globally finite term rewriting systems, 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. 155-203.

*[Gobel 1985a] R. Gobel, Completion of globally finite term rewriting systems for inductive proofs, Proc. GWAI-85, 9th German Workshop on Artificial Intelligence (Dassel/Solling, 23-27 September 1985), Informatik-Fachberichte 118, ed. H. Stoyan, Springer-Verlag, Berlin, 1985, pp. 101-110; also SEKI Report SR-86-06, Universitat Kaiserslautern, 1986.

[Gobel 1985b] R. Gobel, A specialized Knuth-Bendix algorithm for inductive proofs, Proc. Conf. on Combinatorial Algorithms in Algebraic Structures, Universitat Kaiserslautern, West Germany, 1985.

*[Gobel 1986a] R. Gobel, Ground Confluence, SEKI Report SR-86-18, Universitat Kaiserslautern, 1986; also Proc. 2nd Intl. Conf. on Rewriting Techniques and Applications (Bordeaux, France, 25-27 May 1987), ed. P. Lescanne, LNCS 256, Springer-Verlag, Berlin, 1987, pp. 156-167.

[Gobel 1986b] R. Gobel, Completion of globally finite term rewriting systems for inductive proofs, Universitat Kaiserslautern SEKI Report SR-86-06, June 1986.

[Gobel 1987] R. Gobel, Completion methods for obtaining ground confluent rule systems and their applications for inductive proofs, Dissertation, FB Informatik, Universitat Kaiserslautern, 1987.

[Gobel 1988] R. Gobel, A completion procedure for generating gound confluent term rewriting systems, PhD thesis, FB Informatik, Universitat Kaiserslautern, Germany, 1988.

[Goguen 1979] J.A. Goguen, J.J. Tardo, An introduction to OBJ, a language for writing and testing formal algebraic specifications, Proc. Conf. on Specifications of Reliable Software, ed. M. Zelkowitz, Boston, IEEE Press, 1979, pp. 170-189; reprinted in Software Specification Techniques, ed. N. Gehani and A. McGettrick, Addison-Wesley, 1985, pp. 391-420.

[Goguen 1980] J.A. Goguen, How to prove algebraic inductive hypotheses without induction, with applications to the correctness of data type implementation, Proc. 5th Conf. on Automated Deduction (Les Arcs, France, July 1980), LNCS 87, Springer-Verlag, Berlin, 1980, pp. 356-372.

[Goguen 1981] J.A. Goguen, J. Meseguer, Completeness of many-sorted equational logic, ACM Sigplan Notices 16(7):24-32, January 1981; also Houston J. of Mathematics 11(1985):307-334.

[Goguen 1984] J.A. Goguen, J. Meseguer, Equality, types, modules and generics for logic programming, SRI International, Publication, Menlo Park, 1984.

[Goguen 1986] J. Goguen, C. Kirchner, J. Meseguer, A rewrite rule machine: Models of computation for the rewrite rule machine, SRI International, July 1986.

[Goguen 1987] J. Goguen, C. Kirchner, J. Meseguer, Concurrent term rewriting as a model of computation, Proc. Graph Reduction Workshop, ed. R. Keller and J. Fasel, LNCS 279, Springer-Verlag, 1987, pp. 53-93.

*[Goguen 1988a] J. Goguen, C. Kirchner, H. Kirchner, A. Megrelis, J. Meseguer, T. Winkler, An introduction to OBJ3, 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. 258-263.

[Goguen 1988b] J.A. Goguen, What is unification? A categorical view, SRI-CSL-88-2, Comp. Sci. Lab., SRI International, 1988.

*[Goguen 1989a] J.A. Goguen, OBJ as a theorem prover with application to hardware verification, Computer Science Lab, SRI International, 333 Ravenswood Ave., Menlo Park, CA 94025, USA; also In Current Trends in Hardware Verification and Automated Theorem Proving, ed. G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, NY, 1989, pp. 218-267.

*[Goguen 1989b] J. Goguen, What is unifications?, In: Resolution of Equations in Algebraic Structures: Vol 1, Algebraic Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 217-261.

[Goldberg 1979a] A. Goldberg, Average complexity of the satisfiability problem, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979, pp. 1-6.

[Goldberg 1979b] A.T. Goldberg, On the complexity of the satisfiability problem, NSO-16, Courant Institute of Mathematical Sciences, New York Univ., 1979.

[Goldfarb 1981] W.D. Goldfarb, The undecidability of the second-order unification problem, Theoretical Computer Science 13(2):225-230, 1981.

[Goldstein 1973] I. Goldstein, Elementary geometry theorem proving, MIT, AI Lab memo no. 280, April 1973.

[Gonnet 1986] G. Gonnet, New results for random determination of equivalence of expression, Proc. 1986 ACM Symp. on Symbolic and Algebraic Comp., ed. B.W. Char, Waterloo, Ontario, July 1986, pp. 127-131.

[Good 1975] D.I. Good, R.L. London, W.W. Bledsoe, An interactive program verifier, IEEE Trans. on Software Eng. SE-I(March 1975):59-67; also Proc. 1975 Intl. Conf. on Reliable Software, Los Angeles, CA, pp. 482-492.

[Gordon 1977a] M. Gordon, R. Milner, C. Wadsworth, Edinburgh LCF, Internal report CSR-11-77, Dept. of Comput. Sci., Univ. of Edinburgh, September 1977.

[Gordon 1977b] M. Gordon, R. Milner, L. Morris, N. Newey, C. Wadsworth, A metalanguage for interactive proof in LCF, Internal report CSR-16-77, Dept. of Comput. Sci., Univ. of Edinburgh, September 1977; also Proc. 5th ACM SIGACT-SIGPLAN Conf. on Principles of Programming Languages, Tucson, Arizona, 1978.

[Gordon 1979a] M.J. Gordon, A.J. Milner, C.P. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation, LNCS 78, Springer-Verlag, NY, 1979.

[Gordon 1979b] M. Gordon, R. Milner, L. Morris, N. Newey, C. Wadsworth, LCF: A way of doing proofs with a machine, Proc. 8th MFCS Symp., Olomouc, Czechoslovakia, 1979.

[Gordon 1982] M.J.C. Gordon, Representing a logic in the LCF metalanguage, In: Tools and Notions for program Construction, ed. D. Neel, Cambridge Univ. Press, 1982, pp. 163-185.

[Gordon 1985] M.J.C. Gordon, HOL: A machine oriented formulation of higher order logic, Tech. Report 68, Computer Lab., Univ. of Cambridge, revised version, July 1985.

*[Gordon 1987] M.J.C. Gordon, HOL: A proof generating system for higher-order logic, Tech. Report 103, Computer Lab., Univ. of Cambridge, 1987; also revised version in VLSI Specification, Verification, and Synthesis, ed. G. Birtwistle and P.A. Subrahmanyam, Kluwer International Series in Engineering and Computer Science, SECS35, Kluwer Academic Publishers, Norwell, MA, 1988, pp. 73-128.

*[Gordon 1988] M.J.C. Gordon, Programming language theory and its implementation: Applicative and imperative paradigms, Prentice Hall, London, 1988.

*[Gordon 1989] M.J.C. Gordon, Mechanizing programming logics in higher order logic, In Current Trends in Hardware Verification and Automated Theorem Proving, ed. G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, NY, 1989, pp. 387-439.

[Goto 1976] E. Goto, Y. Kanada, Hashing lemmas on time complexities with applications to formula manipulation, Proc. 1976 ACM Symp. on Symbolic and Algebraic Comp. (Yorktown Heights, NY), ed. R.D. Jenks, August 1976, pp. 154-158.

[Goto 1991] S. Goto, Proof normalization with nonstandard objects, Theor. Comput. Sci. 85(2):333-351, August 1991.

*[Gottler 1989] H. Gottler, Graph grammars, a new paradigm for implementing visual languages, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 152-166.

[Gottlob 1985a] G. Gottlob, A. Leitsch, On the efficiency of subsumption algorithms, JACM 32(2):280-295, April 1985.

*[Gottlob 1985b] G. Gottlob, A. Leitsch, Fast subsumption algorithms (full paper), 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. 64-77.

[Gottlob 1987] G. Gottlob, Subsumption and implication, Information Processing Letters 24 (1987):109-111.

[Gould 1966] W.E. Gould, A matching procedure for omega-order logic, AFCRL-66-781-4 (thesis), Air Force Cambridge Research Laboratories, Princeton, NJ, 1966.

*[Gramlich 1988a] B. Gramlich, J. Denzinger, AC-matching using constraint propagation, SEKI Report SR-88-15, Universitat Kaiserslautern, 1988.

[Gramlich 1988b] B. Gramlich, Unification of term schemes - theory and application, SEKI Report SR-88-18, Artificial Intelligence Laboratories, Dept. of Computer Science, Universitat Kaiserslautern, W. Germany, December 1988.

[Gramlich 1989] B. Gramlich, Inductive theorem proving using refined unfailing completion techniques, Tech. Rep. SR-89-14, Universitat Kaiserslautern, Germany, 1989.

*[Gramlich 1990a] B. Gramlich, UNICOM: A refined completion based inductive theorem prover (abstract), Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 655-656.

[Gramlich 1990b] B. Gramlich, Inductive theorem proving using refined unfailing completion techniques, SEKI Report SR-89-14, FB Informatik, Universitat Kaiserslautern, 1989.

*[Gramlich 1990c] B. Gramlich, Completion based inductive theorem proving: An abstract framework and its applications, Proc. 9th ECAI (Stockholm, Sweden, 6-10 August 1990), ed. L.C. Aiello, Pitman Publishing, London, 1990, pp. 314-319.

[Gramlich 1991] B. Gramlich, Completion based inductive theorem proving -- a case study in verifying sorting algorithms, SEKI Report, FB Informatik, Universitat Kaiserslautern, forthcoming.

[Green 1969a] C.C. Green, Application of theorem proving to problem solving, Proc. 1st IJCAI (Washington, DC, 7-9 May 1969), Morgan Kaufmann Publishers, Los Altos, CA, 1969, pp. 219-239; also in Readings in Artificial Intelligence, ed. B.L. Webber and N.J. Nilsson, Morgan Kaufmann Publishers, Los Altos, CA, 1981.

[Green 1969b] C.C. Green, Theorem-proving by resolution as a basis for question-answering systems, Machine Intelligence 4, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, Edinburgh, 1969, pp. 183-205.

[Green 1985] C. Green, What is program synthesis? J. of Automated Reasoning 1(1):37-40, D. Reidel Publ. Co., Dordrecht, Holland, 1985.

[Greenbaum 1982] S. Greenbaum, A. Nagasaka, P. O'Rorke, D. Plaisted, Comparison of natural deduction and locking resolution implementations, Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982, pp. 159-171.

[Greenbaum 1983] S. Greenbaum, P. O'Rorke, D.A. Plaisted, Comparison of abstraction and a robust resolution strategy, Rept., Univ. of Illinois, Urbana, IL, 1983.

[Greenbaum 1986a] S. Greenbaum, D.A. Plaisted, The Illinois Prover: A general purpose resolution theorem prover, 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. 685-686.

[Greenbaum 1986b] S. Greenbaum, Input transformations and resolution implementation techniques for theorem proving in first-order logic, PhD thesis, Dept. of Computer Science File 1298, Univ. of Illinois at Urbana-Champaign, September 1986.

*[Greif 1985] J.M. Greif, The SMP pattern matcher, 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. 303-314.

[Greiner 1985] R. Greiner, Learning by understanding analogies, PhD Thesis, Tech. Report STAN-CS-1071, Stanford Univ., September 1985.

[Griffin 1987] T.G. Griffin, An environment for formal systems, Tech. Report 87-846, Dept. of Computer Science, Cornell Univ., 1987; also LFCS report ECS-LFCS-87-34, Dept. of Computer Science, Univ. of Edinburgh.

*[Griffin 1988] T.G. Griffin, EFS - An interactive environment for formal systems, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 740-741.

[Griffin 1989] T.G. Griffin, Notational definition and top-down refinement for interactive proof development systems, DAI V50(03), PhD thesis, Cornell Univ., 1989.

[Grigor'ev 1988] D.Y. Grigor'ev, N.N. Vorobjov, Solving systems of polynomial inequalities in subexponential time, J. Symbolic Computation 5(1988):37-64.

*[Groeneboer 1988] C. Groeneboer, J.P. Delgrande, Tableau-based theorem proving in normal conditional logics, Proc. AAAI-88, 7th National Conf. on Artificial Intelligence, Vol. 1, St. Paul, Minnesota, 21-26 August 1988, pp. 171-176.

[Groote 1987] P. de Groote, How I spent my time in Cambridge with Isabelle, Tech. Report RR 87-1, Unite d'Informatique, Universite Catholique de Louvain, Belgium, January 1987.

[Guard 1964] J.R. Guard, Automated logic for semi-automated mathematics, Sci. Rep. 1, AFCRL 64-411, Air Force Cambridge Research Lab., Cambridge, MA, March 1964.

[Guard 1967] J.R. Guard, et al., CRT-aided semi-automated mathematics, AFRCL-67-0167, Princeton, NJ, Applied Logic Corporation, 1967.

[Guard 1969] J.R. Guard, F.C. Oglesby, J.H. Bennett, L.G. Settle, Semi-automated mathematics, JACM 16(1):49-62, January 1969; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 203-216.

[Guard 1970] J.R. Guard, The arbitrarily-large entities in man-machine mathematics, Formal Systems and Nonnumerical Problem Solving by Computer, ed. Mesarovic, Mihajlo and Banerji, 1970.

[Guckenbiehl 1985] Th. Guckenbiehl, A. Herold, Solving Linear Diophantine Equations, Memo-SEKI 85-IV-KL, Universitat Kaiserslautern, 1985.

*[Guckenbiehl 1991] T. Guckenbiehl, Formalizing and using persistency, 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. 105-110.

*[Guessarian 1988] I. Guessarian, Equational axiomatization of if-then-else, 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. 98-110.

*[Guessarian 1989] I. Guessarian, Some fixpoint techniques in algebraic structures and applications to computer science, In: Resolution of Equations in Algebraic Structures: Vol 1, Algebraic Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 263-292.

[Gurevich 1985] Y. Gurevick, S. Shelah, The decision problem for branching time logic, J. Symbolic Logic 50(3), 1985.

[Guttag 1981a] J.V. Guttag, D. Kapur, D.R. Musser, Derived pairs, overlap closures, and rewrite rules: New tools for analyzing term rewriting systems, Technical Report TR-286, MIT Lab. for Computer Science, December 1981; also Proc. 9th Intl. Colloquium on Automata, Languages and Programming '82, LNCS 140, Springer-Verlag, Berlin, Heidelberg, 1982, pp. 300-312.

[Guttag 1981b] J.V. Guttag, D. Kapur, D.R. Musser, On proving uniform termination and restricted termination of rewriting systems, Report 81, CRD 272, GE Corp. Research and Development Center, 1981; also in SIAM J. on Computing 12(1):189-214, February 1983; also in Proc. 9th Intl Colloquium on Automata, Languages and Programming, Aarhus, Denmark, 1983.

[Guttag 1984] J.V. Guttag, D. Kapur, D.R. Musser, eds., Proc. of an NSF Workshop on the Rewrite Rule Laboratory (September 1983), General Electric, Information Systems Laboratory, Schenectady, NY, No. 84GEN008, April 1984.

[Gypsy 1980] Gypsy 2.0 Verification Environment 6.0 User's Manual, Certifiable Minicomputer Project, Univ. of Texas at Austin, February 1980.


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