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

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