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.

Export metadata

  • Export Bibtex
  • Export RIS

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
Tag:HOT ; higher order tableau ; natural language semantics; theorem prover
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:004 Datenverarbeitung; Informatik

$Rev: 12793 $