HOT swMATH ID: 13308 Software Authors: Konrad, Karsten Description: HOT: A concurrent automated theorem prover based on higher-order tableaux. HOT is an automated higher-order theorem prover based on ℋ𝒯ℰ an extensional higher-order tableaux calculus. The first part of this paper introduces an improved 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. Homepage: http://link.springer.com/chapter/10.1007/BFb0055140 Keywords: automated higher-order theorem prover; extensional higher-order tableaux calculus Related Software: TPS; Nuprl; Zipperposition; CoqHammer; HOLyHammer; E Theorem Prover; Sledgehammer; Satallax; HOL; TPTP; VAMPIRE; ML; DISCOUNT; Leo-III; SPASS; Lambda-Clam; Leo; IMPS; Twelf; ETPS Cited in: 6 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year HOT: A concurrent automated theorem prover based on higher-order tableaux. Zbl 0927.03021Konrad, Karsten 1998 all top 5 Cited by 11 Authors 2 Bentkamp, Alexander 2 Blanchette, Jasmin Christian 2 Tourret, Sophie 2 Vukmirović, Petar 2 Waldmann, Uwe 1 Andrews, Peter B. 1 Bonacina, Maria Paola 1 Brown, Chad Edward 1 Grundy, Jim 1 Konrad, Karsten 1 Newey, Malcolm C. Cited in 4 Serials 1 Journal of Automated Reasoning 1 Annals of Mathematics and Artificial Intelligence 1 Journal of Applied Logic 1 Lecture Notes in Computer Science Cited in 3 Fields 6 Computer science (68-XX) 3 Mathematical logic and foundations (03-XX) 1 General and overarching topics; collections (00-XX) Citations by Year