Henkin semantics for reasoning with natural language

• Autorzy: Hahn M. , Richter F.

Identyfikatory

DOI

10.15398/jlm.v3i2.113

• Języki publikacji: EN

Abstrakty

EN

The frequency of intensional and non-first-order definable operators in natural languages constitutes a challenge for automated reasoning with the kind of logical translations that are deemed adequate by formal semanticists. Whereas linguists employ expressive higher-order logics in their theories of meaning, the most successful logical reasoning strategies with natural language to date rely on sophisticated first-order theorem provers and model builders. In order to bridge the fundamental mathematical gap between linguistic theory and computational practice, we present a general translation from a higher-order logic frequently employed in the linguistics literature, two-sorted Type Theory, to first-order logic under Henkin semantics. We investigate alternative formulations of the translation, discuss their properties, and evaluate the availability of linguistically relevant inferences with standard theorem provers in a test suite of inference problems stated in English. The results of the experiment indicate that translation from higher-order logic to first-order logic under Henkin semantics is a promising strategy for automated reasoning with natural languages.

Słowa kluczowe

EN

Henkin semantics; reasoning; reducing higher-order reasoning; first-order reasoning

• Wydawca: Instytut Podstaw Informatyki PAN
• Czasopismo: Journal of Language Modelling
• Rocznik: 2015
• Tom: Vol. 3, No. 2
• Strony: 513--568
• Opis fizyczny: Bibliogr. 47 poz., rys., tab.

Twórcy

autor

Hahn M.

• Eberhard Karls Universität Tübingen, Tübingen, Germany

autor

Richter F.

• Goethe Universität Frankfurt, Frankfurt a.M., Germany

Bibliografia

• [1] Jon Barwise and Robin Cooper (1981), Generalized quantifiers and natural language, Linguistics and Philosophy, 4 (2): 159-219.
• [2] Michael Bennett (1974), Some Extensions of a Montague Fragment, Ph.D. thesis, UCLA.
• [3] Christoph Benzmüller, Larry Paulson, Frank Theiss, and Arnaud Fietzke (2007), Progress Report on Leo-II, an Automatic Theorem Prover for Higher-Order Logic, in Klaus Schneider and Jens Brandt, editors, Theorem Proving in Higher Order Logics 2007 – Emerging Trends, pp. 33-48.
• [4] Patrick Blackburn and Johan Bos (2005), Representation and Inference for Natural Language, CSLI Publications, Stanford.
• [5] Johan Bos (2004), Computational semantics in discourse: underspecification, resolution, and inference, Journal of Logic, Language and Information, 13: 139-157.
• [6] Johan Bos (2006), Three stories on automated reasoning for natural language understanding, in Proceedings of ESCoR (IJCAR Workshop): Empirically Successful Computerized Reasoning, pp. 81-91.
• [7] Johan Bos (2008), Wide-coverage semantic analysis with Boxer, in Johan Bos and Rodolfo Delmonte, editors, Semantics in Text Processing. STEP 2008 Conference Proceedings, Research in Computational Semantics, pp. 277-286, College Publications.
• [8] Johan Bos and Katja Markert (2006), When logical inference helps determining textual entailment (and when it doesn’t), in Bernardo Magnini and Ido Dagan, editors, The Second PASCAL Recognising Textual Entailment Challenge. Proceedings of the Challenges Workshop, pp. 98-103, Venice, Italy.
• [9] Chad E. Brown (2013), Reducing higher-order theorem proving to a sequence of SAT problems, Journal of Automated Reasoning, 51 (1): 57-77.
• [10] Ricardo Caferra, Alexander Leitsch, and Nicolas Peltier (2004), Automated Model Building, Kluwer.
• [11] Alonzo Church (1940), A formulation of the simple theory of types, The Journal of Symbolic Logic, 5 (2): 56-68.
• [12] Robin Cooper, Dick Crouch, Jan van Eijck, Chris Fox, Josef van Genabith, Jan Jaspars, Hans Kamp, David Milward, Manfred Pinkal, Massimo Poesio, Steve Pulman, Ted Briscoe, Holger Maier, and Karsten Konrad (1996), Using the Framework, Technical report, FraCaS Consortium, University of Edinburgh, Deliverable D16 — Final Draft.
• [13] Ido Dagan, Bill Dolan, Bernardo Magnini, and Dan Roth (2009), Recognizing textual entailment: Rational, evaluation and approaches, Natural Language Engineering, 15 (4): i-xvii.
• [14] Mary Dalrymple, Stuart M. Shieber, and Fernando C. N. Pereira (1991), Ellipsis and higher-order unification, Linguistics and Philosophy, 14 (4): 399-452.
• [15] David R. Dowty, Robert E. Wall, and Stanley Peters (1981), Introduction to Montague Semantics, Reidel, Dordrecht.
• [16] Joyce Friedman and David S. Warren (1980), λ-normal forms in an intensional model for English, Studia Logica, 39: 311-324.
• [17] Daniel Gallin (1975), Intensional and Higher-Order Modal Logic, North-Holland, Amsterdam.
• [18] L.T.F. Gamut (1991), Logic, Language and Meaning, Volume II: Intensional Logic and Logical Grammar, University of Chicago Press.
• [19] Jeroen Groenendijk and Martin Stokhof (1982), Semantic analysis of wh-complements, Linguistics and Philosophy, 5 (2): 175-233.
• [20] Leon Henkin (1950), Completeness in the theory of types, The Journal of Symbolic Logic, 15 (2): 81-91.
• [21] Klaus von Heusinger (1997), Definite descriptions and choice functions, in Seiki Akama, editor, Logic, Language and Computation, volume 5 of Applied Logic Series, pp. 61-91, Springer.
• [22] J. Roger Hindley and Jonathan P. Seldin (2008), Lambda-Calculus and Combinators, an Introduction, Cambridge University Press.
• [23] Jaako Hintikka (1962), Knowledge and Belief. An Introduction to the Logic of the Two Notions, Cornell University Press.
• [24] Kryštof Hoder and Andrei Voronkov (2011), Sine qua non for large theory reasoning, in Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, Automated Deduction – CADE-23, volume 6803 of Lecture Notes in Computer Science, pp. 299-314, Springer.
• [25] Joe Hurd (2002), An LCF-style interface between HOL and first-order logic, in Andrei Voronkov, editor, Automated Deduction – CADE-18, volume 2392 of Lecture Notes in Computer Science, pp. 134-138, Springer.
• [26] Bjørn Jespersen and Giuseppe Primiero (2013), Alleged assassins: realist and constructivist semantics for modal modification, in Guram Bezhanishvili, Sebastian Löbner, Vincenzo Marra, and Frank Richter, editors, Logic, Language, and Computation. 9th International Tbilisi Symposium, number 7758 in Lecture Notes in Computer Science, pp. 94-114, Springer.
• [27] Hans Kamp and Barbara Partee (1995), Prototype theory and compositionality, Cognition, 57 (2): 129-91.
• [28] Hans Kamp and Uwe Reyle (1993), From Discourse to Logic, Kluwer, Dordrecht.
• [29] Manfred Kerber (1992), On the Representation of Mathematical Concepts and their Translation into First Order Logic, Ph.D. thesis, Universität Kaiserslautern.
• [30] Michael Kohlhase and Karsten Konrad (1998), Higher-Order Automated Theorem Proving for Natural Language Semantics, unpublished manuscript. Web. Sept. 17, 2015. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.4186.
• [31] Karsten Konrad (2004), Model Generation for Natural Language Interpretation and Analysis, number 2953 in Lecture Notes in Artificial Intelligence, Springer.
• [32] Daniel Leivant (1994), Higher order logic, in Handbook of Logic in Artificial Intelligence and Logic Programming (2), pp. 229-322.
• [33] David K. Lewis (1968), Counterpart theory and quantifed modal logic, Journal of Philosophy, 65 (5): 113-126.
• [34] Bill MacCartney (2009), Natural Language Inference, Ph.D. thesis, Stanford University.
• [35] William McCune (2005-2010), Prover9 and Mace4, Web. Sept. 17, 2015. http://www.cs.unm.edu/~mccune/prover9/.
• [36] Jia Meng and Lawrence C. Paulson (2008), Translating higher-order clauses to first-order clauses, Journal of Automated Reasoning, 40 (1): 35-60.
• [37] Richard Montague (1970), English as a formal language, in Bruno Visenti, editor, Linguaggi nella Società e nella Tecnica, pp. 189-224, Edizioni di Comunità, Milan.
• [38] Richard Montague (1973), The proper treatment of quantification in ordinary English, in K. J. J. Hintikka, J. M. E. Moravcsik, and P. Suppes, editors, Approaches to Natural Language, pp. 221-242, Reidel, Dordrecht.
• [39] Ekaterina Ovchinnikova (2012), Integration of World Knowledge for Natural Language Understanding, volume 3 of Atlantis Thinking Machines, Atlantis Press.
• [40] Barbara H. Partee (1995), Lexical semantics and compositionality, in Lila R. Gleitman and Mark Liberman, editors, An Invitation to Cognitive Science. Language, volume 1, pp. 311-360, MIT Press.
• [41] Allan Ramsay (1995), Theorem proving for intensional logic, Journal of Automated Reasoning, 14: 237-255.
• [42] Nicholas Rescher (2005), Epistemic Logic: A Survey of the Logic of Knowledge, University of Pittsburgh Press.
• [43] Stephan Schulz (2004), System Description: E 0.81, in David Basin and Michaël Rusinowitch, editors, Automated Reasoning. Second International Joint Conference, IJCAR 2004, volume 3097 of Lecture Notes in Computer Science, pp. 223-228, Springer.
• [44] Ray Turner (1987), A theory of properties, Journal of Symbolic Logic, 52 (2): 455-472.
• [45] Johan van Benthem and Kees Doets (1983), Higher-order logic, in Handbook of philosophical logic, pp. 275-329, Springer.
• [46] Christoph Weidenbach (2001), Combining superposition, sorts and splitting, in Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 27, pp. 1965-2013, Elsevier Science.
• [47] Dag Westerståhl (2011), Generalized quantifiers, in Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy, summer 2011 edition.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).