The search result changed since you submitted your search request. Documents might be displayed in a different sort order.
  • search hit 2 of 3
Back to Result List

Higher-Order Automated Theorem Proving for Natural Language Semantics

  • This paper describes a tableau-based higher-order theorem prover HOT and an application to natural language semantics. In this application, HOT is used to prove equivalences using world knowledge during higher-order unification (HOU). This extended form of HOU is used to compute the licensing conditions for corrections.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Author:Michael Kohlhase, Karsten Konrad
URN (permanent link):urn:nbn:de:hbz:386-kluedo-3912
Serie (Series number):SEKI Report (98,4)
Document Type:Preprint
Language of publication:English
Year of Completion:1998
Year of Publication:1998
Publishing Institute:Technische Universität Kaiserslautern
Date of the Publication (Server):2000/04/03
Tag:HOT; higher order tableau; natural language semantics; theorem prover
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011