ileanCoP swMATH ID: 9757 Software Authors: Otten, Jens Description: Clausal connection-based theorem proving in intuitionistic first-order logic. We present a clausal connection calculus for first-order intuitionistic logic. It extends the classical connection calculus by adding prefixes that encode the characteristics of intuitionistic logic. Our calculus is based on a clausal matrix characterisation for intuitionistic logic, which we prove correct and complete. The calculus was implemented by extending the classical prover leanCoP. We present some details of the implementation, called Emphasis ileanCoP, and experimental results. Homepage: http://www.leancop.de/ileancop/index.html Related Software: leanCoP; TPTP; FEMaLeCoP; E Theorem Prover; VAMPIRE; ILTP; MaLeCoP; MleanCoP; MPTP 0.2; JProver; Coq; nanoCoP; Satallax; MaLARea; Mizar; Flyspeck; leanTAP; SETHEO; QMLTP; HOList Cited in: 31 Publications all top 5 Cited by 33 Authors 10 Otten, Jens 5 Urban, Josef 4 Raths, Thomas 3 Färber, Michael 3 Kaliszyk, Cezary 3 Kreitz, Christoph 2 Benzmüller, Christoph Ewald 2 Brown, Chad Edward 2 Rawson, Michael 2 Reger, Giles 2 Sutcliffe, Geoff 2 Waaler, Arild 2 Zombori, Zsolt 1 Alonderis, Romas 1 Antonsen, Roger 1 Bibel, Wolfgang 1 Brandt, Christoph 1 Czajka, Łukasz 1 Dyckhoff, Roy 1 Gauthier, Thibault 1 Holden, Sean B. 1 Holen, Bjarne 1 Johnsen, Einar Broch 1 Mangla, Chaitanya 1 McLaughlin, Sean 1 Olšák, Miroslav 1 Pak, V. G. 1 Paulson, Lawrence Charles 1 Pavlov, V. A. 1 Pease, Adam 1 Pfenning, Frank 1 Schulz, Stephan 1 Vyskočil, Jiří Cited in 5 Serials 3 Journal of Automated Reasoning 1 Programming and Computer Software 1 Journal of Symbolic Computation 1 AI Communications 1 Archive for Mathematical Logic Cited in 3 Fields 26 Computer science (68-XX) 13 Mathematical logic and foundations (03-XX) 1 Operations research, mathematical programming (90-XX) Citations by Year