V. Lifschitz, L. Morgenstern, D. Plaisted 79
[87] M. Fitting. First-Order Logic and Automated Theorem Proving. Springer-
Verlag, New York, 1990.
[88] E. Franconi, A.L. Palma,N. Leone, S. Perri, and F. Scarcello. Census data repair:
a challenging application of disjunctive logic programming. In R. Nieuwenhuis
and A. Voronkov, editors. LPAR, Lecture Notes in Computer Science, vol. 2250,
pages 561–578. Springer, 2001.
[89] G. Frege. Begriffsschrift, eine der arithmetischen nachgebildete Formelsch-
prache des reinen Denkens. Halle, 1879. English translation: [261, pp. 1–82].
[90] T.W. Frühwirth and S. Abdennadher. The Munich rent advisor: A success for
logic programming on the Internet. TPLP, 1(3):303–319, 2001.
[91] U. Furbach and N. Shankar, editors. Automated Reasoning, Third International
Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17–20, 2006, Pro-
ceedings. Lecture Notes in Computer Science, vol. 4130. Springer, 2006.
[92] J.-M. Gaillourdet, T. Hillenbrand, B. Löchner, and H. Spies. The new Wald-
meister loop at work. In Baader [10], pages 317–321.
[93] H. Ganzinger and K. Korovin. New directions in instantiation-based theo-
rem proving. In Proc. 18th IEEE Symposium on Logic in Computer Science,
(LICS’03), pages 55–64. IEEE Computer Society Press, 2003.
[94] H. Gelernter, J.R. Hansen, and D.W. Loveland. Empirical explorations of the
geometry theorem proving machine. In E. Feigenbaum and J. Feldman, editors.
Computers and Thought, pages 153–167. McGraw-Hill, New York, 1963.
[95] M. Genesereth and N.J. Nilsson. Logical Foundations of Artificial Intelligence.
Morgan Kaufmann, San Mateo, CA, 1987.
[96] G. Gentzen. Untersuchungen über das logische Schließen. Mathematische
Zeitschrift, 39:176–210, 1935.
[97] J. Giesl and D. Kapur. Deciding inductive validity of equations. In Baader [10],
pages 17–31.
[98] J. Giesl, P. Schneider-Kamp, and R. Thiemann. Automatic termination proofs in
the dependency pair framework. In Furbach and Shankar [91], pages 281–286.
[99] P.C. Gilmore. A proof method for quantification theory. IBM Journal of Re-
search and Development, 4:28–35, 1960.
[100] K. Gödel. Die Vollständigkeit fer Axiome des logischen Funktionenkalküls.
Monatshefte für Mathematik und Physik, 37:349–360, 1930. English transla-
tion: [261, pp. 582–591].
[101] M.J. Gordon and T.F. Melham, editors. Introduction to HOL: A Theorem-
Proving Environment for Higher-Order Logic. Cambridge University Press,
1993.
[102] B.C. Grau, B. Parsia, E. Sirin, and A. Kalyanpur. Automatic partitioning of owl
ontologies using-connections. In I. Horrocks, U. Sattler, and F. Wolter, editors.
Description Logics, volume 147 of CEUR Workshop Proceedings, 2005.
[103] C.C. Green. The Applications of Theorem Proving to Question-Answering Sys-
tems. Garland, New York, 1969.
[104] C.C. Green. Application of theorem proving to problem solving. In IJCAI, pages
219–240, 1969.
[105] J.V. Guttag, D. Kapur, and D. Musser. On proving uniform termination and re-
stricted termination of rewriting systems. SIAM J. Comput., 12:189–214, 1983.