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

Search Google Scholar
Metadaten
Author:Michael Kohlhase, Karsten Konrad
URN:urn:nbn:de:hbz:386-kluedo-3912
Series (Serial Number):SEKI Report (98,4)
Document Type:Preprint
Language of publication:English
Year of Completion:1998
Year of first Publication:1998
Publishing Institution: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:Kaiserslautern - Fachbereich Informatik
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011