OpenTheory swMATH ID: 32625 Software Authors: Hurd, J. Description: The goal of the OpenTheory project is to allow specifications and proofs to be shared between different theorem prover implementations of higher order logic, including HOL Light, HOL4 and ProofPower. It is hoped that OpenTheory packages are adopted by the higher order logic theorem proving community as a common format to build a standard library of formalized mathematics and verified software. Homepage: http://www.gilith.com/opentheory/ Related Software: HOL Light; HOL; Isabelle/HOL; Isabelle; Coq; Flyspeck; QMT; MMT; ProofPower; HOLyHammer; CakeML; Jitawa; Milawa; LCF; Mizar; MoMM; TPTP; ML; MPTP 0.2; Tactician Cited in: 16 Publications all top 5 Cited by 30 Authors 6 Kaliszyk, Cezary 4 Gauthier, Thibault 4 Kumar, Ramana 3 Arthan, Rob D. 3 Myreen, Magnus O. 2 Abrahamsson, Oskar 2 Norrish, Michael 2 Rabe, Florian 1 Carneiro, Mario M. 1 Chihani, Zakaria 1 Davis, Jared 1 Ebner, Gabriel 1 Grov, Gudmund 1 Hetzl, Stefan 1 Ho, Son Lam 1 Hurd, Joe 1 Kanabar, Hrutvik 1 Kohlhase, Michael 1 Lin, Yuhui 1 Miller, Dale Allen 1 Müller, Dennis 1 Owens, Scott 1 Reis, Giselle 1 Renaud, Fabien 1 Riener, Martin 1 Tan, Yong Kiam 1 Urban, Josef 1 Wang, Qingxiang 1 Wolfsteiner, Simon 1 Zivota, Sebastian Cited in 4 Serials 6 Journal of Automated Reasoning 2 Journal of Formalized Reasoning 1 Journal of Symbolic Computation 1 Journal of Logical and Algebraic Methods in Programming Cited in 2 Fields 16 Computer science (68-XX) 5 Mathematical logic and foundations (03-XX) Citations by Year