The inverse lambda calculus algorithm for typed first order logic lambda calculus and its application to translating english to FOL

Chitta Baral, Marcos Alvarez Gonzalez, Aaron Gottesman

Research output: Chapter in Book/Report/Conference proceedingChapter

1 Citation (Scopus)

Abstract

In order to answer questions and solve problems that require deeper reasoning with respect to a given text, it is necessary to automatically translate English sentences to formulas in an appropriate knowledge representation language. This paper focuses on a method to translate sentences to First-Order Logic (FOL). Our approach is inspired by Montague's use of lambda calculus formulas to represent the meanings of words and phrases. Since our target language is FOL, the meanings of words and phrases are represented as FOL-lambda formulas. In this paper we present algorithms that allow one to construct FOL-lambda formulas in an inverse manner. Given a sentence and its meaning and knowing the meaning of several words in the sentence our algorithm can be used to obtain the meaning of the other words in that sentence. In particular the two algorithms take as input two FOL-lambda formulas G and H and compute a FOL-lambda formula F such that F with input G, denoted by F@G, is H; respectively, G@F = H. We then illustrate our algorithm and present soundness, completeness and complexity results, and briefly mention the use of our algorithm in a NL Semantics system that translates sentences from English to formulas in formal languages.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages40-56
Number of pages17
Volume7265
DOIs
StatePublished - 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7265
ISSN (Print)03029743
ISSN (Electronic)16113349

Fingerprint

Lambda Calculus
First-order Logic
Formal languages
Knowledge representation
Formal Languages
Semantics
Knowledge Representation
Soundness
Completeness
Reasoning
Meaning
Target
Necessary

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Baral, C., Gonzalez, M. A., & Gottesman, A. (2012). The inverse lambda calculus algorithm for typed first order logic lambda calculus and its application to translating english to FOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7265, pp. 40-56). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7265). https://doi.org/10.1007/978-3-642-30743-0_4

The inverse lambda calculus algorithm for typed first order logic lambda calculus and its application to translating english to FOL. / Baral, Chitta; Gonzalez, Marcos Alvarez; Gottesman, Aaron.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 7265 2012. p. 40-56 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7265).

Research output: Chapter in Book/Report/Conference proceedingChapter

Baral, C, Gonzalez, MA & Gottesman, A 2012, The inverse lambda calculus algorithm for typed first order logic lambda calculus and its application to translating english to FOL. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 7265, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7265, pp. 40-56. https://doi.org/10.1007/978-3-642-30743-0_4
Baral C, Gonzalez MA, Gottesman A. The inverse lambda calculus algorithm for typed first order logic lambda calculus and its application to translating english to FOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 7265. 2012. p. 40-56. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-30743-0_4
Baral, Chitta ; Gonzalez, Marcos Alvarez ; Gottesman, Aaron. / The inverse lambda calculus algorithm for typed first order logic lambda calculus and its application to translating english to FOL. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 7265 2012. pp. 40-56 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inbook{56e0fbea0fa540709434cb24feadde9b,
title = "The inverse lambda calculus algorithm for typed first order logic lambda calculus and its application to translating english to FOL",
abstract = "In order to answer questions and solve problems that require deeper reasoning with respect to a given text, it is necessary to automatically translate English sentences to formulas in an appropriate knowledge representation language. This paper focuses on a method to translate sentences to First-Order Logic (FOL). Our approach is inspired by Montague's use of lambda calculus formulas to represent the meanings of words and phrases. Since our target language is FOL, the meanings of words and phrases are represented as FOL-lambda formulas. In this paper we present algorithms that allow one to construct FOL-lambda formulas in an inverse manner. Given a sentence and its meaning and knowing the meaning of several words in the sentence our algorithm can be used to obtain the meaning of the other words in that sentence. In particular the two algorithms take as input two FOL-lambda formulas G and H and compute a FOL-lambda formula F such that F with input G, denoted by F@G, is H; respectively, G@F = H. We then illustrate our algorithm and present soundness, completeness and complexity results, and briefly mention the use of our algorithm in a NL Semantics system that translates sentences from English to formulas in formal languages.",
author = "Chitta Baral and Gonzalez, {Marcos Alvarez} and Aaron Gottesman",
year = "2012",
doi = "10.1007/978-3-642-30743-0_4",
language = "English (US)",
isbn = "9783642307423",
volume = "7265",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "40--56",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - CHAP

T1 - The inverse lambda calculus algorithm for typed first order logic lambda calculus and its application to translating english to FOL

AU - Baral, Chitta

AU - Gonzalez, Marcos Alvarez

AU - Gottesman, Aaron

PY - 2012

Y1 - 2012

N2 - In order to answer questions and solve problems that require deeper reasoning with respect to a given text, it is necessary to automatically translate English sentences to formulas in an appropriate knowledge representation language. This paper focuses on a method to translate sentences to First-Order Logic (FOL). Our approach is inspired by Montague's use of lambda calculus formulas to represent the meanings of words and phrases. Since our target language is FOL, the meanings of words and phrases are represented as FOL-lambda formulas. In this paper we present algorithms that allow one to construct FOL-lambda formulas in an inverse manner. Given a sentence and its meaning and knowing the meaning of several words in the sentence our algorithm can be used to obtain the meaning of the other words in that sentence. In particular the two algorithms take as input two FOL-lambda formulas G and H and compute a FOL-lambda formula F such that F with input G, denoted by F@G, is H; respectively, G@F = H. We then illustrate our algorithm and present soundness, completeness and complexity results, and briefly mention the use of our algorithm in a NL Semantics system that translates sentences from English to formulas in formal languages.

AB - In order to answer questions and solve problems that require deeper reasoning with respect to a given text, it is necessary to automatically translate English sentences to formulas in an appropriate knowledge representation language. This paper focuses on a method to translate sentences to First-Order Logic (FOL). Our approach is inspired by Montague's use of lambda calculus formulas to represent the meanings of words and phrases. Since our target language is FOL, the meanings of words and phrases are represented as FOL-lambda formulas. In this paper we present algorithms that allow one to construct FOL-lambda formulas in an inverse manner. Given a sentence and its meaning and knowing the meaning of several words in the sentence our algorithm can be used to obtain the meaning of the other words in that sentence. In particular the two algorithms take as input two FOL-lambda formulas G and H and compute a FOL-lambda formula F such that F with input G, denoted by F@G, is H; respectively, G@F = H. We then illustrate our algorithm and present soundness, completeness and complexity results, and briefly mention the use of our algorithm in a NL Semantics system that translates sentences from English to formulas in formal languages.

UR - http://www.scopus.com/inward/record.url?scp=84864203898&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84864203898&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-30743-0_4

DO - 10.1007/978-3-642-30743-0_4

M3 - Chapter

AN - SCOPUS:84864203898

SN - 9783642307423

VL - 7265

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 40

EP - 56

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -