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,
SpringerVerlag, Berlin, pp. 205220; also Theoretical Computer
Science 43(1):189200, 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, SpringerVerlag,
Berlin, pp. 205220; also in Theoretical Computer Science
43(1986):189200.
[Fages 1984] F. Fages, Associativecommunative 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 (CADE7, Napa, CA, May 1984), ed. R.E.
Shostak, LNCS 170, SpringerVerlag, NY, 1984, pp. 194208; also
INRIA Report CNRSLITP4, 1983; also Technical report, INRIA, BP
105, 78153 le Chesnay, 1985; also J. of Symbolic Computation
3(3):257275, June 1987.
[Farinas 1982a] L. Farinas del Cerro, A simple deduction method
for modal logic, Information Processing Letters 14(2):4951, 20
April 1982.
*[Farinas 1982b] L. Farinas del Cerro, A deduction method for
modal logic, Proc. ECAI82, Univ. ParisSud, Orsay, France, 1214
July 1982, pp. 6061.
[Farinas 1983] L. Farinas del Cerro, Temporal reasoning and
termination of programs, Proc. 8th IJCAI, Karlsruhe, W. Germany,
August 1983, pp. 926929.
[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
CollesurLoup, France), October 1984, pp. 4678.
[Farinas 1985] L. Farinas del Cerro, M. Orlowska, eds.,
Automated reasoning in nonclassical logic, Special double issue
of Logique et Analyse 28(1985):115294.
[Farinas 1986] L. Farinas del Cerro, Molog, a system that
extends Prolog with modal logic, New Generation Computing
4(1986):3550.
[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 (CADE9,
Argonne, Illinois, 2326 May 1988), ed. E. Lusk and R. Overbeek,
LNCS 310, SpringerVerlag, Berlin, 1988, pp. 487499.
[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, 610 August 1990), ed. L.C. Aiello, Pitman Publishing,
London, 1990, pp. 262267.
[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
secondorder monadic terms, Annals of Pure and Applied Logic
39(1988):131174.
[Farmer 1988b] W.M. Farmer, A partial functions version of
Church's simple theory of types, Tech. Report M8852, 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 M9019, 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 (CADE10, Kaiserslautern, FRG, July
1990), Lecture Notes in Artificial Intelligence 449, ed. M.E.
Stickel, SpringerVerlag, Berlin, 1990, pp. 653654.
*[Farmer 1992a] W.M. Farmer, J.D. Guttman, F.J. Thayer, Little
theories, Proc. 11th Intl. Conf. on Automated Deduction (CADE11,
Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes
in Artificial Intelligence 607, SpringerVerlag, Berlin, 1992, pp.
567581.
*[Farmer 1992b] W.M. Farmer, J.D. Guttman, F.J. Thayer, IMPS:
System description, Proc. 11th Intl. Conf. on Automated Deduction
(CADE11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur,
Lecture Notes in Artificial Intelligence 607, SpringerVerlag,
Berlin, 1992, pp. 701705.
*[Farreny 1982] H. Farreny, H. Prade, About flexible matching
and its use in analogical reasoning, Proc. ECAI82, Univ.
ParisSud, Orsay, France, 1214 July 1982, pp. 4347.
*[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 userlevel semantic matching
capability in MACSYMA, Proc. 2nd Symp. on Symbolic and Algebraic
Manipulation (Los Angeles, CA, March 2325), ed. S.R. Petrick,
ACM, NY, 1971, pp. 311323.
[Fateman 1972] R.J. Fateman, Essays in algebraic simplification,
PhD thesis, 1972; also Tech. Rep. MACTR95, 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.
(MUC79, Washington, DC, 2022 June 1979), MIT Laboratory for
Computer Science, 545 Technology Square, Cambridge, MA, 1979, pp.
563582.
*[Fateman 1988] R. Fateman, A. Bundy, R. O'Keefe, I. Sterling,
Commentary on: Solving symbolic equations with PRESS, SIGSAM
Bulletin 22(2):2740, issue 84, April 1988.
[Fateman 1989] R.J. Fateman, C. Ponder, Speed and data
structures in computer algebra systems, ACM SIGSAM Bulletin
23(2):811, 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, 1517 July 1991), ACM Press, NY, NY, 1991, pp. 360369.
[Fay 1979] M. Fay, First order unification in an equational
theory, Proc. 4th Workshop on Automated Deduction (CADE4, Austin,
Texas, 13 February 1979), ed. W.H. Joyner, 1979, pp. 161167.
[FearnleySander 1985] D. FearnleySander, Using and computing
symmetry in geometry proofs, DAI Research Paper 257, Dept. of
Artificial Intelligence, Edinburgh, 1985; also Proc. AISB85, ed.
P. Ross, Warwick, 1985.
*[FearnleySander 1989] D. Fearnley, Sander, The idea of a
diagram, In: Resolution of Equations in Algebraic Structures: Vol
1, Algebraic Techniques, ed. H. AitKaci, M. Nivat, Academic
Press, Inc., San Diego, 1989, pp. 127150.
*[Fehrer 1990] D. Fehrer, A resolution calculus for a logic
based on vaguely defined predicates, Proc. 9th ECAI (Stockholm,
Sweden, 610 August 1990), ed. L.C. Aiello, Pitman Publishing,
London, 1990, pp. 268273.
*[Fegaras 1992] L. Fegaras, T. Sheard, D. Stemple, Uniform
traversal combinators: definition, use and properties, Proc. 11th
Intl. Conf. on Automated Deduction (CADE11, Saratoga Springs, NY,
USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial
Intelligence 607, SpringerVerlag, Berlin, 1992, pp. 148162.
[Feigenbaum 1963] E. Feigenbaum, J. Feldman, eds., Computers and
Thought, McGrawHill, 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, Patterndirected
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, Patterndirected
invocation with changing equations, J. Automated Reasoning
7(3):403433, September 1991.
*[Feldman 1993] Y.A. Feldman, H. Schneider, Simulating reactive
systems by deduction, ACM Trans. on Software Engineering and
Methodology 2(2):128175, April 1993.
[Felty 1986] A.P. Felty, Using extended tactics to do proof
transofrmations, Tech. Report MSCIS8689, Dept. of Computer and
Information Science, Univ. of Pennsylvania, 1986. *[Felty 1988a]
A. Felty, D. Miller, Specifying theorem provers in a higherorder
logic programming language, Proc. 9th Intl. Conf. on Automated
Deduction (CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk
and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
6180.
*[Felty 1988b] A. Felty, et al., Lambda Prolog: an extended
logic programming language, Proc. 9th Intl. Conf. on Automated
Deduction (CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk
and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
754755.
*[Felty 1990a] A. Felty, D. Miller, Encoding a dependenttype
lambdacalculus in a logic programming language, Proc. 10th Intl.
Conf. on Automated Deduction (CADE10, Kaiserslautern, FRG, July
1990), Lecture Notes in Artificial Intelligence 449, ed. M.E.
Stickel, SpringerVerlag, Berlin, 1990, pp. 221235.
*[Felty 1990b] A. Felty, E. Gunter, D. Miller, F. Pfenning,
Lambda Prolog (tutorial abstract), Proc. 10th Intl. Conf. on
Automated Deduction (CADE10, Kaiserslautern, FRG, July 1990),
Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel,
SpringerVerlag, Berlin, 1990, p. 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):6976, 1975.
[Ferro 1978] A. Ferro, E.G. Omodeo, An efficient validity test
for formulae in extensional twolevel syllogistic, Le Matematiche
(Catania, Italy) 33(1978):130137.
*[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, 811 July 1980), ed. W.
Bibel and R. Kowalski, LNCS 87, SpringerVerlag, Berlin, 1980, pp.
8896.
*[Ferro 1980b] A. Ferro, E.G. Omodeo, J.T. Schwartz, Decision
procedures for elementary sublanguages of set theory. I:
Multilevel syllogistic and some extensions, Commun. Pure and
Appl. Math. 33(5):599608, 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, 811 July 1980), ed. W.
Bibel and R. Kowalski, LNCS 87, SpringerVerlag, Berlin, 1980, pp.
8896.
[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): 367374.
[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):265280.
*[Ferro 1990] G.C. Ferro, G. Gallo, A procedure to prove
statements in differential geometry, J. Automated Reasoning
6(2):203209, 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):257270, June 1991.
*[Ferscha 1987] A. Ferscha, A matrixapproach for proving
inequalities, Proc. European Conf. on Computer Algebra (EUROCAL
'87, Leipzig, GDR, 25 June 1987), ed. J.H. Davenport, LNCS 378,
SpringerVerlag, Berlin, 1989, pp. 403411.
[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):151168, Hungary.
[Fikes 1970] R.E. Fikes, REFARF: A system for solving problems
stated as procedures, Artificial Intelligence 1(1970):27120.
[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. 608620; also
Artificial Intelligence 2(Winter):189208, 1971.
[Fikes 1977] R. Fikes, G. Hendrix, A networkbased knowledge
representation and its natural deduction system, Proc. 5th IJCAI,
MIT, Cambridge, MA, 1977, pp. 235246.
*[Fisher 1991] M. Fisher, A resolution method for temporal
logic, Proc. 12th Intl. Conf. on Artificial Intelligence, Vol 1
(IJCAI91, Darling Harbour, Sydney, Australia, 2430 August 1991),
Morgan Kaufmann Publ., Inc., 1991, pp. 99104.
*[Fisher 1992] M. Fisher, A normal form for firstorder temporal
formulae, Proc. 11th Intl. Conf. on Automated Deduction (CADE11,
Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes
in Artificial Intelligence 607, SpringerVerlag, Berlin, 1992, pp.
370384.
[Fishman 1976] D.H. Fishman, Problemoriented search procedure
for theorem proving, IEEE Trans. on Computers 25(8):807815,
August 1976.
[Fitting 1972] M.C. Fitting, Tableau methods of proof for modal
logics, Notre Dame J. of Formal Logic 13(1972):237247.
[Fitting 1977] M.C. Fitting, A tableau system for propositional
SS, Notre Dame J. of Formal Logic 18(1977):292294.
[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 (1417 October 1987, Charlotte, North Carolina), ed. Z.W.
Ras and M. Zemankova, NorthHolland, Amsterdam, 1987, pp. 400407.
*[Fitting 1988] M. Fitting, Firstorder modal tableux, J.
Automated Reasoning 4(2):191213, 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. 6370.
*[Fitting 1990] M. Fitting, FirstOrder Logic and Automated
Theorem Proving, SpringerVerlag 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):124139.
[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. 1419.
*[Forgaard 1984a] R. Forgaard, D. Detlefs, A program for
generating and analyzing term rewriting systems, Tech. Report
MIT/LCS/TR343, 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 KnuthBendix, 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 failureresistant KnuthBendix,
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. 531.
[Forgaard 1986] R. Forgaard, A program for generating and
analyzing term rewriting systems, MIT/LCS/TR343, 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,
CarnegieMellon Univ., Pittsburgh, PA 15213, 1980; also Artificial
Intelligence 19(1):1738, 1982.
[Forster 1980] D. Forster, GTP: A graphbased theorem prover,
Master's thesis, Univ. of Waterloo, Ontario, Canada, 1980.
[Forsythe 1984] K. Forsythe, S. Matwin, Implementation
strategies for planbased deduction, Proc. 7th Intl. Conf. on
Automated Deduction (CADE7, Napa, CA, May 1984), ed. R.E.
Shostak, LNCS 170, SpringerVerlag, NY, 1984, pp. 426444.
[Fortenbacher 1981] A. Fortenbacher, M. Schreck, G. Wrightson,
Implementation and results of a proof procedure for firstorder
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, 2022 May
1985), ed. J.P. Jouannaud, LNCS 202, SpringerVerlag, Berlin,
1985, pp. 381397; also J. of Symbolic Computation 3(3):217229,
June 1987.
[Franova 1984] M. Franova, CMStrategydriven deductions for
automatic programming, in ECAI84, Advances in Artificial
Intelligence, ed. T. O'Shea, Elsevier Science Publ. B.V.
(NorthHolland), 1984, pp. 573576.
[Franova 1985] M. Franova, CMStrategy: A methodology for
inductive theorem proving or constructive wellgeneralize proofs,
Proc. 9th IJCAI, Vol. 2, Los Angeles, CA, 1823 August 1985, pp.
12141220.
*[Franova 1988] M. Franova, Fundamentals for a new methodology
for inductive theorem proving: CMconstruction of atomic formulae,
Proc. 8th ECAI, Institut fur Informatik der Technischen
Universitat Munchen, 15 August 1988. pp. 136141.
[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. ParisSud,
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. ParisSud,
Bat. 490, 91405 Orsay Cedex, France, 1993.
*[Franova 1993c] M. Franova, Constructive matching methodology
and automatic planconstruction 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 ACunification,
Internal Report, Dept. of Comp. Sci., Northwestern Univ.,
Illinois, 1987; also Proc. 9th Intl. Conf. on Automated Deduction
(CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk and R.
Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp. 643657.
[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 rulebased nonmonotonic deduction system, Proc.
11th German Workshop on Artificial Intelligence (GWAI87, Geseke,
September 28October 2, 1987), ed. K. Morik, SpringerVerlag,
Berlin, 1987, pp. 170174.
[Fribourg 1983] L. Fribourg, A superposition oriented theorem
prover, Tech. Report 11, LITP, 1983; also Proc. 8th IJCAI,
Karlsruhe, W. Germany, August 1983, pp. 923925; also Theoretical
Computer Science 35(1985):129164.
[Fribourg 1984a] L. Fribourg, A narrowing procedure for theories
with constructors, Proc. 7th Intl. Conf. on Automated Deduction
(CADE7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170,
SpringerVerlag, NY, 1984, pp. 259281.
[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. 162172.
[Fribourg 1984c] L. Fribourg, Handling function definition
through innermost superposition and rewriting, Report 8469 LITP,
Universite Paris 7, 1984; also Proc. 1st Conf. Rewriting
Techniques and Applications (Dijon, France, 2022 May 1985), ed.
J.P. Jouannaud, LNCS 202, SpringerVerlag, Berlin, 1985, pp.
325344.
*[Fribourg 1985] L. Fribourg, SLOG: A logic programming language
interpreter based on clausal superposition and rewriting, Proc.
1985 Symp. Logic Programming, Boston, MA, 1518 July 1985, pp.
172184.
[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, SpringerVerlag, Berlin, 1986, pp. 105115;
revised appeared in J. Symbolic Computation 8(3):253276, 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, SpringerVerlag, 1986, pp. 105115.
*[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, 810 July
1987), ed. S. Kaplan and J.P. Jouannaud, LNCS 308,
SpringerVerlag, Berlin, 1988, pp. 5661.
[Fribourg 1989a] L. Fribourg, A strong restriction of the
inductive completion procedure, J. Symbolic Computation
8(3):253276, 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.
AitKaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp.
117140.
*[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. 103116.
[Friedland 1985] P.E. Friedland, Y. Iwasaki, The concept and
implementation of skeletal plans, J. of Automated Reasoning
1(2):161208, 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 semidecision procedure for
functional calculus, JACM 10(1):124, 1963; also Automation of
Reasoning  Classical Papers on Computational Logic, Vol. I,
19571966, ed. J. Siekmann and G. Wrightson, SpringerVerlag,
Berlin, 1983, pp. 331354.
[Friedman 1963b] J. Friedman, A computer program for a solvable
case of the decision problem, JACM 10(3):348356, 1963; also
Automation of Reasoning  Classical Papers on Computational Logic,
Vol. I, 19571966, ed. J. Siekmann and G. Wrightson,
SpringerVerlag, Berlin, 1983, pp. 355363.
[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. 327328.
[Frisch 1985] A.M. Frisch, An investigation into inference with
restricted quantification and a taxonomic representation, SIGART
Newsletter 91(1985):2831.
[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. 126136.
[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(13):161198, May 1991.
*[Frisch 1992] A.M. Frisch, An abstract view of sorted
unification, Proc. 11th Intl. Conf. on Automated Deduction
(CADE11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur,
Lecture Notes in Artificial Intelligence 607, SpringerVerlag,
Berlin, 1992, pp. 178192.
[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.,
NorthHolland, AmsterdamNew York, 1986, pp. 391401.
[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 August3 September 1993), Vol 1, ed. R.
Bajscy, IJCAI, Inc., 1993, pp. 5259.
[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
(GWAI87, Geseke, September 28October 2, 1987), ed. K. Morik,
SpringerVerlag, Berlin, 1987, pp. 195200.
*[Furbach 1989a] U. Furbach, S. Holldobler, J. Schreiber, Linear
paramodulation modulo equality, Proc. 13 German Workshop on
Artificial Intelligence (GWAI89, Eringerfeld, 1822 September
1989), ed. D. Metzing, SpringerVerlag, Berlin, 1989, pp. 107116.
*[Furbach 1989b] U. Furbach, S. Holldobler, J. Schreiber, Horn
equational theories and paramodulation, J. Automated Reasoning
5(3):309337, 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 ACMSIGSAM
Symp. on Symbolic and Algebraic Computation (SYMSAC '86, Univ. of
Waterloo, Waterloo, Ontario, 2123 July 1986), ed. B.W. Char, ACM,
New York, NY, 1986, pp. 222224.
[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. 5266.
[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):511536, December 1991.
[Gabow 1976] H. Gabow, An efficient implementation of Edmond's
algorithm for maximum matching on graphs, JACM 23(1976):221234.
*[Gabriel 1985] J. Gabriel, T. Lindholm, E.L. Lusk, R.A.
Overbeek, A tutorial on the Warren abstract machine for
computational logic, Tech. Report ANL8484, 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 75239, PhD
thesis, Dept. of Computer Science, Cornell Univ., 1975.
[Galil 1977a] Z. Galil, On the complexity of regular resolution
and the DavisPutnam procedure, Theoretical Computer Science
4(1977):2346.
[Galil 1977b] Z. Galil, On resolution with clauses of bounded
size, SIAM J. Computing 6(1977):44459.
*[Galil 1991] Z. Galil, G. Italiano, Data structures and
algorithms for disjoint set union problems, ACM Computing Surveys
23(3):319344, 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):123150, November 1985.
[Gallier 1985] J.H. Gallier, S. Raatz, Logic programming and
graph rewriting, Proc. 2nd Symp. on Logic Programming, Boston, MA,
1985, pp. 208219.
[Gallier 1986a] J.H. Gallier, A fast algorithm for testing
unsatisfiability of Ground Horn clauses, MSCIS8606, Univ. of
Pennsylvania, 1986.
[Gallier 1986b] J.H. Gallier, S. Raatz, Extending SLDResolution
to equational Horn clauses using EUnification, MSCIS8644,
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, MSCIS8610, Univ. of
Pennsylvania, 1986.
[Gallier 1986d] J.H. Gallier, S. Raatz, Refutation methods for
Horn clauses with equality based on unification, MSCIS8659,
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, SLDresolution methods
for Horn clauses with equality based on Eunification, Proc. Symp.
on Logic Programming, Salt Lake City, Utah, 2225 September 1986,
pp. 168179.
[Gallier 1987a] J.H. Gallier, S. Raatz, W. Snyder, Theorem
proving using rigid Eunification: Equational matings, Proc. IEEE
Symp. on Logic in Computer Science, Ithaca, NY, 2225 June 1987,
pp. 338346; also Internal Report, Dept. of Computer and
Information Science, Univ. of Pennsylvania, Philadelphia.
[Gallier 1987b] J.H. Gallier, W. Snyder, A general complete
Eunification procedure, Proc. 2nd Intl. Conf. on Rewriting
Techniques and Applications (Bordeaux, France, 2527 May 1987),
ed. P. Lescanne, LNCS 256, SpringerVerlag, Berlin, 1987, pp.
216227.
*[Gallier 1987c] J.H. Gallier, Fast algorithms for testing
unsatisfiability of Ground Horn clauses, J. of Symbolic
Computation 4(2):233254, October 1987.
*[Gallier 1988a] J. Gallier, W. Snyder, P. Narendran, D.
Plaisted, Rigid Eunification is NPcomplete, Proc. 3rd IEEE Symp.
on Logic in Computer Science, Edinburgh, Scotland, 58 July 1988,
pp. 218227.
*[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 (CADE9, Argonne, Illinois,
2326 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310,
SpringerVerlag, Berlin, 1988, pp. 182196.
*[Gallier 1989a] J. Gallier, W. Snyder, S. Raatz, Rigid
Eunification and its applications to equational matings, In:
Resolution of Equations in Algebraic Structures: Vol 1, Algebraic
Techniques, ed. H. AitKaci, M. Nivat, Academic Press, Inc., San
Diego, 1989, pp. 151216.
[Gallier 1989b] J. Gallier, W. Snyder, Completion sets of
transformations for general Eunification, Theor. Comput. Sci.
67(1989): 203260.
[Gallier 1990] J. Gallier, W. Snyder, Designing unification
procedures using transformations: A survey, EATCS Bulletin,
40(February 1990): 273326.
[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):116, 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, 1921 February 1987), ed. F.J. Brandenburg, G.
VidalNaquet and M. Wirsing, LNCS 247, 1987, pp. 286298.
[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, 810 July 1987), ed. S. Kaplan and J.P.
Jouannaud, LNCS 308, SpringerVerlag, Berlin, 1988, pp. 6283;
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):2228.
[Ganzinger 1988a] H. Ganzinger, Completion with
historydependent complexities for generated equations, In Recent
Trends in Data Type Specification, ed. Sannella and Tarlecki,
Springer LNCS 332, 1988, pp. 7391.
[Ganzinger 1988b] H. Ganzinger, Ordersorted completion: The
manysorted 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 (CADE9, Argonne,
Illinois, 2326 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310,
SpringerVerlag, Berlin, 1988, pp. 748749.
[Garland 1988] S.J. Garland, J.V. Guttag, Inductive methods for
reasoning about abstract data types, Proc. POPL '88, 1988, pp.
219228.
*[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, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 137151.
[Garson 1980] J. Garson, P. Mellema, ComputerAssisted
Instruction on Logic: EMIL, Teaching Philosophy, 1980, pp.
453478.
[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):403417, 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 ACMSIGSAM Symp. on
Symbolic and Algebraic Computation (SYMSAC '86, Univ. of Waterloo,
Waterloo, Ontario, 2123 July 1986), ed. B.W. Char, ACM, New York,
NY, 1986, pp. 218221.
*[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,
1922 March 1986, pp. 309324.
[Gelder 1984] A. Van Gelder, A satisfiability tester for
nonclausal propositional calculus, Proc. 7th Intl. Conf. on
Automated Deduction (CADE7, Napa, CA, May 1984), ed. R.E.
Shostak, LNCS 170, SpringerVerlag, NY, 1984, pp. 101112; also
UCSCCRL8832, 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):336345.
[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
geometrytheorem proving machine, Proc. Intl. Conf. on Information
Processing, UNESCO House, 1959, pp. 273282; also in Computers and
Thought, ed. E.A. Feigenbaum and J. Feldman, McGrawHill, NY,
1963; also reprinted in Siekmann and Wrightson, 1983, pp. 99117.
[Gelernter 1963a] H. Gelernter, Machinegenerated
problemsolving graphs, Proc. Symp. Math. Theory Automata,
Polytechnic Press, NY, 1963, pp. 179203; also Automation of
Reasoning  Classical Papers on Computational Logic, Vol. I,
19571966, ed. J. Siekmann and G. Wrightson, SpringerVerlag,
Berlin, 1983, pp. 288312.
[Gelernter 1963b] H. Gelernter, Realization of a
geometrytheorem proving machine, Proc. Intl. Conf. Information
Proc., UNESCO House, Paris, 1959, pp. 273283; also in Computers
and Thought, ed. E.A. Feigenbaum and J. Feldman, McGrawHill, NY,
1963, pp. 134152; also Automation of Reasoning  Classical Papers
on Computational Logic, Vol. I, 19571966, ed. J. Siekmann and G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 99122.
[Gelernter 1963c] H. Gelernter, J. Hansen, D. Loveland,
Empirical explorations of the geometrytheorem proving machine,
Proc. West Joint Computer Conf., 1960, pp. 143147, in Computers
and Thought, ed. E.A. Feigenbaum and J. Feldman,, McGrawHill, NY,
1963, pp. 153167; also Automation of Reasoning  Classical Papers
on Computational Logic, Vol. I, 19571966, ed. J. Siekmann and G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 140150.
[Gelperin 1973] D. Gelperin, Deletion directed search in
resolutionbased proof procedures, Proc. 3rd IJCAI, Stanford
Univ., 1973, pp. 4750.
[Gelperin 1976] D. Gelperin, A resolutionbased proof procedure
using deletiondirected search, IEEE Trans. on Computers
C25(4):323327, April 1976.
[Genesereth 1983] M.R. Genesereth, R. Greiner, D.E. Smith, A
metalevel representation system, Stanford, Memo HPP8328, 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):155170, April 1983.
[Gentzen 1935] G. Gentzen, Investigations into logical
deduction, 1935, In The Collected Papers of Gerhard Gentzen, ed.
M.E. Szabo, NorthHolland, Amsterdam, 1969, pp. 68131.
[Gergely 1978] T. Gergely, K.P. Vershinin, Model theoretical
investigation of theorem proving methods, Notre Dame J. Formal
Logic 19(4):523542, October 1978.
[Gergely 1983] T. Gergely, K. Vershinin, Negative
Hyperresolution for proving statements containing transistive
relations, Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983,
pp. 877881.
[Gerhart 1980] S.L. Gerhart, et al., An overview of AFFIRM: a
specification and verification system, Information Processing
80(October 1980):343348, ed. S.H. Lavington, NorthHolland.
[Geser 1985] A. Geser, H. Hussmann, Rapid prototyping for
algebraic specifications  Examples for the use of the RAP system,
MIP8517, 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, 1719 March 1986), ed. B. Robinet and R.
Wilhelm, LNCS 213, SpringerVerlag, Berlin, 1986, pp. 339350.
*[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,
810 July 1987), ed. S. Kaplan and J.P. Jouannaud, LNCS 308,
SpringerVerlag, Berlin, 1988, pp. 8490.
*[Geupel 1989] Oliver Geupel, Overlap closures and termination
of term rewriting systems, Reprot MIP8922, Fakultat fur
Mathematik und Informatik, Universitat Passau, July 1989.
[Ghallab 1981] M. Ghallab, Decision trees for optimizing
patternmatching algorithms in production systems, Proc. IJCAI81,
Vancouver, BC, 1981, pp. 310312.
*[Ghelfo 1985] S. Ghelfo, E.G. Omodeo, Towards practical
implementations of syllogistic (Full paper), Proc. European Conf.
on Computer Algebra (EUROCAL '85, Linz, Austria, 13 April 1985),
Vol. 2: Research Contributions, ed. B.F. Caviness, LNCS 204,
SpringerVerlag, Berlin, pp. 4049.
[Gianni 1988] P. Gianni, B. Trager, G. Zacharias, Grobner bases
and primary decomposition of polynomial ideals, J. Symbolic
Computation 6(1988):149169.
*[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
(CADE8, Oxford, England, July 27August 1, 1986), ed. J.H.
Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp. 683684.
[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. 265273.
[Gilmore 1960] P.C. Gilmore, A proof method for quantification
theory: Its justification and realization, IBM J. Research and
Development 4(January 1960):2835; also Automation of Reasoning 
Classical Papers on Computational Logic, Vol. I, 19571966, ed. J.
Siekmann and G. Wrightson, SpringerVerlag, Berlin, 1983, pp.
151161.
[Gilmore 1970] P. Gilmore, An examination of the geometry
theorem machine, Artificial Intelligence 1(Fall 1970):171187.
[Ginsberg 1989] M.L. Ginsberg, A circumscriptive theorem prover,
Artif. Intell. 39(2):209230, June 1989.
*[Ginsberg 1990] M.L. Ginsberg, W.D. Harvey, Iterative
broadening, Proc. 8th National Conf. on Artificial Intelligence
(AAAI90, July 29August 3, 1990), AAAI Press/MIT Press, 1990, pp.
216220; also Artif. Intell. 55(23):367383, June 1992.
*[Giovannetti 1986] E. Giovannetti, C. Moiso, A completeness
result for Eunification algorithms based on conditional
narrowing, Proc. Foundations of Logic and Functional Programming
(Trento, Italy, 1519 December 1986), ed. M. Boscarol, L.C.
Aiello, and G. Levi, LNCS 306, SpringerVerlag, 1988, pp. 157167.
*[Giovannetti 1988] E. Giovannetti, C. Moiso, Notes on the
elimination of conditions, Proc. 1st Intl. Workshop on Conditional
Term Rewriting Systems (Orsay, France, 810 July 1987), ed. S.
Kaplan and J.P. Jouannaud, LNCS 308, SpringerVerlag, Berlin,
1988, pp. 9197.
[Girard 1987] J.Y. Girard, Linear logic, Theoret. Comput. Sci.
50(1987):1102.
*[Giunchiglia 1988] F. Giunchiglia, A. Giunchiglia, Building
complex derived inference rules: a decider for the class of Prenex
universalexistential formulas, Proc. 8th ECAI, Institut fur
Informatik der Technischen Universitat, Munchen, 15 August 1988,
pp. 607609; 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 (AISB89, Univ. of Sussex, 1821 April 1989),
ed. A.G. Cohn, Pitman Publ., London, 1989, pp. 175183.
*[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, 2025 August 1989), ed. N.S. Sridharan, IJCAI Inc.,
1989, pp. 372377.
[Giunchiglia 1989c] F. Giunchiglia, A. Smaill, Reflection in
constructive and nonconstructive automated reasoning, Proc.
Workshop on MetaProgramming in Logic Programming, ed. H. Abramson
and M.H. Rogers, MIT Press, 1989, pp. 123140; IRST Tech. Report
890204; 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 MetaProgramming in Logic, ed. M.
Bruynooghe, MIT Press, 1990; also IRST Tech. Report 900312.
[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 UKIT 90 Conference, 1990,
pp. 365370.
*[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 (IJCAI91, Darling Harbour, Sydney, Australia,
2430 August 1991), Morgan Kaufmann Publ., Inc., 1991, pp.
111117.
[Giunchiglia 1991b] F. Giunchiglia, R.W. Weyhrauch, FOL user
manual  FOL version 2, Tech. report 910705, 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 (AISB91, Leeds, UK),
1991; also IRSTTechnical Report no. 901008; 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, 37 August 1992), ed. B. Neumann, John Wiley & Sons,
Chichester, 1992, pp. 7781.
[Glickfeld 1986] B. Glickfeld, R. Overbeek, A foray into
combinatory logic, J. of Automated Reasoning 2(4):419431,
December 1986.
[Gloess 1980] P.Y. Gloess, An experiment with the BoyerMoore
theorem prover: A proof of the correctness of a simple parser of
expressions, Proc. 5th Conf. on Automated Deduction (Les Arcs,
France, 811 July 1980), ed. W. Bibel and R. Kowalski, LNCS 87,
SpringerVerlag, Berlin, 1980, pp. 154169.
[Glushkov 1972] V.M. Glushkov, Y.V. Kapitonova, Automatic search
for proofs of mathematical theorems and intelligent computers,
Kibernetika 8(5):26, 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 (CADE8, Oxford, England, July
27August 1, 1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag,
Berlin, 1986, pp. 5261.
[Gnaedig 1988] I. Gnaedig, KnuthBendix procedure and
nondeterministic behavior  An example, Bulletin of the European
Association for Theoretical Computer Science 32(1988):8692.
[Gnaedig 1990] I. Gnaedig, H. Kirchner, Equational completion in
ordersorted algebras, Theor. Comput. Sci. 72(2,3):169202, May
1990.
[Goad 1980a] C. Goad, Proofs as descriptions of computation.
Proc. 5th Conf. on Automated Deduction (Les Arcs, France), LNCS
87, SpringerVerlag, Berlin, 1980, pp. 3952.
[Goad 1980b] C. Goad, Computational uses of the manipulation of
formal proofs, Tech. report STANCS80819, 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.
155203.
*[Gobel 1985a] R. Gobel, Completion of globally finite term
rewriting systems for inductive proofs, Proc. GWAI85, 9th German
Workshop on Artificial Intelligence (Dassel/Solling, 2327
September 1985), InformatikFachberichte 118, ed. H. Stoyan,
SpringerVerlag, Berlin, 1985, pp. 101110; also SEKI Report
SR8606, Universitat Kaiserslautern, 1986.
[Gobel 1985b] R. Gobel, A specialized KnuthBendix 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
SR8618, Universitat Kaiserslautern, 1986; also Proc. 2nd Intl.
Conf. on Rewriting Techniques and Applications (Bordeaux, France,
2527 May 1987), ed. P. Lescanne, LNCS 256, SpringerVerlag,
Berlin, 1987, pp. 156167.
[Gobel 1986b] R. Gobel, Completion of globally finite term
rewriting systems for inductive proofs, Universitat Kaiserslautern
SEKI Report SR8606, 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. 170189; reprinted in
Software Specification Techniques, ed. N. Gehani and A.
McGettrick, AddisonWesley, 1985, pp. 391420.
[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, SpringerVerlag,
Berlin, 1980, pp. 356372.
[Goguen 1981] J.A. Goguen, J. Meseguer, Completeness of
manysorted equational logic, ACM Sigplan Notices 16(7):2432,
January 1981; also Houston J. of Mathematics 11(1985):307334.
[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, SpringerVerlag,
1987, pp. 5393.
*[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, 810 July 1987), ed. S. Kaplan and J.P. Jouannaud, LNCS
308, SpringerVerlag, Berlin, 1988, pp. 258263.
[Goguen 1988b] J.A. Goguen, What is unification? A categorical
view, SRICSL882, 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,
SpringerVerlag, NY, 1989, pp. 218267.
*[Goguen 1989b] J. Goguen, What is unifications?, In: Resolution
of Equations in Algebraic Structures: Vol 1, Algebraic Techniques,
ed. H. AitKaci, M. Nivat, Academic Press, Inc., San Diego, 1989,
pp. 217261.
[Goldberg 1979a] A. Goldberg, Average complexity of the
satisfiability problem, Proc. 4th Workshop on Automated Deduction
(CADE4, Austin, Texas, 13 February 1979), ed. W.H. Joyner, 1979,
pp. 16.
[Goldberg 1979b] A.T. Goldberg, On the complexity of the
satisfiability problem, NSO16, Courant Institute of Mathematical
Sciences, New York Univ., 1979.
[Goldfarb 1981] W.D. Goldfarb, The undecidability of the
secondorder unification problem, Theoretical Computer Science
13(2):225230, 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.
127131.
[Good 1975] D.I. Good, R.L. London, W.W. Bledsoe, An interactive
program verifier, IEEE Trans. on Software Eng. SEI(March
1975):5967; also Proc. 1975 Intl. Conf. on Reliable Software, Los
Angeles, CA, pp. 482492.
[Gordon 1977a] M. Gordon, R. Milner, C. Wadsworth, Edinburgh
LCF, Internal report CSR1177, 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 CSR1677, Dept. of Comput. Sci., Univ. of Edinburgh,
September 1977; also Proc. 5th ACM SIGACTSIGPLAN 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,
SpringerVerlag, 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. 163185.
[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
higherorder 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. 73128.
*[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, SpringerVerlag, NY, 1989, pp. 387439.
[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. 154158.
[Goto 1991] S. Goto, Proof normalization with nonstandard
objects, Theor. Comput. Sci. 85(2):333351, 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, 35
April 1989), ed. N. Dershowitz, SpringerVerlag, NY, 1989, pp.
152166.
[Gottlob 1985a] G. Gottlob, A. Leitsch, On the efficiency of
subsumption algorithms, JACM 32(2):280295, April 1985.
*[Gottlob 1985b] G. Gottlob, A. Leitsch, Fast subsumption
algorithms (full paper), Proc. European Conf. on Computer Algebra
(EUROCAL '85, Linz, Austria, 13 April 1985), Vol. 2: Research
Contributions, ed. B.F. Caviness, LNCS 204, SpringerVerlag,
Berlin, pp. 6477.
[Gottlob 1987] G. Gottlob, Subsumption and implication,
Information Processing Letters 24 (1987):109111.
[Gould 1966] W.E. Gould, A matching procedure for omegaorder
logic, AFCRL667814 (thesis), Air Force Cambridge Research
Laboratories, Princeton, NJ, 1966.
*[Gramlich 1988a] B. Gramlich, J. Denzinger, ACmatching using
constraint propagation, SEKI Report SR8815, Universitat
Kaiserslautern, 1988.
[Gramlich 1988b] B. Gramlich, Unification of term schemes 
theory and application, SEKI Report SR8818, 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. SR8914,
Universitat Kaiserslautern, Germany, 1989.
*[Gramlich 1990a] B. Gramlich, UNICOM: A refined completion
based inductive theorem prover (abstract), Proc. 10th Intl. Conf.
on Automated Deduction (CADE10, Kaiserslautern, FRG, July 1990),
Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel,
SpringerVerlag, Berlin, 1990, pp. 655656.
[Gramlich 1990b] B. Gramlich, Inductive theorem proving using
refined unfailing completion techniques, SEKI Report SR8914, 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, 610 August 1990), ed. L.C. Aiello,
Pitman Publishing, London, 1990, pp. 314319.
[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, 79 May 1969),
Morgan Kaufmann Publishers, Los Altos, CA, 1969, pp. 219239; 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, Theoremproving by resolution as a
basis for questionanswering systems, Machine Intelligence 4, ed.
B. Meltzer and D. Michie, Edinburgh Univ. Press, Edinburgh, 1969,
pp. 183205.
[Green 1985] C. Green, What is program synthesis? J. of
Automated Reasoning 1(1):3740, 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, SpringerVerlag, Berlin, 1982, pp. 159171.
[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 (CADE8, Oxford, England, July
27August 1, 1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag,
Berlin, 1986, pp. 685686.
[Greenbaum 1986b] S. Greenbaum, Input transformations and
resolution implementation techniques for theorem proving in
firstorder logic, PhD thesis, Dept. of Computer Science File
1298, Univ. of Illinois at UrbanaChampaign, September 1986.
*[Greif 1985] J.M. Greif, The SMP pattern matcher, Proc.
European Conf. on Computer Algebra (EUROCAL '85, Linz, Austria,
13 April 1985), Vol. 2: Research Contributions, ed. B.F.
Caviness, LNCS 204, SpringerVerlag, Berlin, pp. 303314.
[Greiner 1985] R. Greiner, Learning by understanding analogies,
PhD Thesis, Tech. Report STANCS1071, Stanford Univ., September
1985.
[Griffin 1987] T.G. Griffin, An environment for formal systems,
Tech. Report 87846, Dept. of Computer Science, Cornell Univ.,
1987; also LFCS report ECSLFCS8734, 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
(CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk and R.
Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp. 740741.
[Griffin 1989] T.G. Griffin, Notational definition and topdown
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):3764.
*[Groeneboer 1988] C. Groeneboer, J.P. Delgrande, Tableaubased
theorem proving in normal conditional logics, Proc. AAAI88, 7th
National Conf. on Artificial Intelligence, Vol. 1, St. Paul,
Minnesota, 2126 August 1988, pp. 171176.
[Groote 1987] P. de Groote, How I spent my time in Cambridge
with Isabelle, Tech. Report RR 871, Unite d'Informatique,
Universite Catholique de Louvain, Belgium, January 1987.
[Guard 1964] J.R. Guard, Automated logic for semiautomated
mathematics, Sci. Rep. 1, AFCRL 64411, Air Force Cambridge
Research Lab., Cambridge, MA, March 1964.
[Guard 1967] J.R. Guard, et al., CRTaided semiautomated
mathematics, AFRCL670167, Princeton, NJ, Applied Logic
Corporation, 1967.
[Guard 1969] J.R. Guard, F.C. Oglesby, J.H. Bennett, L.G.
Settle, Semiautomated mathematics, JACM 16(1):4962, January
1969; also Automation Of Reasoning  Classical Papers On
Computational Logic, Vol. II, 19671970, ed. J. Siekmann And G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 203216.
[Guard 1970] J.R. Guard, The arbitrarilylarge entities in
manmachine 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, MemoSEKI 85IVKL, Universitat
Kaiserslautern, 1985.
*[Guckenbiehl 1991] T. Guckenbiehl, Formalizing and using
persistency, Proc. 12th Intl. Conf. on Artificial Intelligence,
Vol 1 (IJCAI91, Darling Harbour, Sydney, Australia, 2430 August
1991), Morgan Kaufmann Publ., Inc., 1991, pp. 105110.
*[Guessarian 1988] I. Guessarian, Equational axiomatization of
ifthenelse, Proc. 1st Intl. Workshop on Conditional Term
Rewriting Systems (Orsay, France, 810 July 1987), ed. S. Kaplan
and J.P. Jouannaud, LNCS 308, SpringerVerlag, Berlin, 1988, pp.
98110.
*[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. AitKaci, M. Nivat, Academic Press, Inc., San
Diego, 1989, pp. 263292.
[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 TR286, MIT
Lab. for Computer Science, December 1981; also Proc. 9th Intl.
Colloquium on Automata, Languages and Programming '82, LNCS 140,
SpringerVerlag, Berlin, Heidelberg, 1982, pp. 300312.
[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):189214, 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.
