• search hit 202 of 206
Back to Result List

HOT: A Concurrent Automated Theorem Prover based on Higher-Order Tableaux

  • HOT is an automated higher-order theorem prover based on HTE, an extensional higher-order tableaux calculus (Kohlhase 95). The first part of the paper introduces a variant of the calculus which closely corresponds to the proof procedure implemented in HOT. The second part discusses HOT's design that can be characterized as a concurrent Blackboard architecture. We show the usefulness of the implementation by including benchmark results for over one hundred solved problems from logic and set theory.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Author:Karsten Konrad
URN (permanent link):urn:nbn:de:hbz:386-kluedo-3893
Serie (Series number):SEKI Report (98,3)
Document Type:Preprint
Language of publication:English
Year of Completion:1999
Year of Publication:1999
Publishing Institute:Technische Universität Kaiserslautern
Date of the Publication (Server):2000/04/03
Tag:Blackboard architecture; HOT; HTE; higher-order tableaux calculus; higher-order 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