iProver swMATH ID: 9707 Software Authors: Korovin, Konstantin Description: iProver – an instantiation-based theorem prover for first-order logic. iProver is an instantiation-based theorem prover which is based on Inst-Gen calculus, complete for first-order logic. One of the distinctive features of iProver is a modular combination of instantiation and propositional reasoning. In particular, any state-of-the art SAT solver can be integrated into our framework. iProver incorporates state-of-the-art implementation techniques such as indexing, redundancy elimination, semantic selection and saturation algorithms. Redundancy elimination implemented in iProver include: dismatching constraints, blocking non-proper instantiations and propositional-based simplifications. In addition to instantiation, iProver implements ordered resolution calculus and a combination of instantiation and ordered resolution. In this paper we discuss the design of iProver and related implementation issues. Homepage: http://link.springer.com/chapter/10.1007%2F978-3-540-71070-7_24 Related Software: TPTP; VAMPIRE; E Theorem Prover; SPASS; z3; Sledgehammer; MiniSat; CVC4; OTTER; iProver-Eq; Darwin; Isabelle/HOL; Satallax; SIMPLIFY; Mace4; SMT-LIB; E-Darvin; HOL Light; Coq; Waldmeister Referenced in: 53 Publications all top 5 Referenced by 89 Authors 8 Korovin, Konstantin 4 Plaisted, David Alan 4 Voronkov, Andrei 3 Brown, Chad Edward 3 Burel, Guillaume 3 Kovács, Laura Ildikó 3 Reger, Giles 3 Sutcliffe, Geoff 3 Tinelli, Cesare 3 Weidenbach, Christoph 3 Woltzenlogel Paleo, Bruno 2 Barrett, Clark W. 2 Baumgartner, Peter 2 Biere, Armin 2 Bonacina, Maria Paola 2 Kaliszyk, Cezary 2 Rawson, Michael 2 Reynolds, Andrew 2 Schulz, Stephan 2 Slaney, John K. 1 Alagi, Gábor 1 Asperti, Andrea 1 Benzmüller, Christoph Ewald 1 Bromberger, Martin 1 Bury, Guillaume 1 Cauderlier, Raphaël 1 Charrier, Tristan 1 Conchon, Sylvain 1 Cruanes, Simon 1 Danas, Ryan 1 Delahaye, David 1 Desharnais, Martin 1 Deters, Morgan 1 Dougherty, Daniel J. 1 Dowek, Gilles 1 Dragoste, Irina 1 Dross, Claire 1 Duarte, André 1 Faqeh, Rasha 1 Fetzer, Christof 1 Filliâtre, Jean-Christophe 1 Fröhlich, Andreas M. 1 Gauthier, Thibault 1 Goel, Amit 1 Gupta, Ashutosh 1 Halmagrand, Pierre 1 Henzinger, Thomas A. 1 Hermant, Olivier 1 Heule, Marijn J. H. 1 Holden, Edvard K. 1 Hottelier, Thibaud 1 Iosif, Radu 1 Itegulov, Daniyar 1 Järvisalo, Matti 1 Ji, Kailiang 1 Kanig, Johannes 1 Khasidashvili, Zurab O. 1 Kotel’nikov, Evgeny A. 1 Kovásznai, Gergely 1 Kragl, Bernhard 1 Krötzsch, Markus 1 Krstic, Sava A. 1 López-Hernández, Julio César 1 Lynch, Christopher A. 1 McGregor, Ralph Eric 1 Miller, Swaha 1 Paskevich, Andrei 1 Pelzer, Björn 1 Pinchinat, Sophie 1 Reichl, Franz-Xaver 1 Reis, Giselle 1 Ricciotti, Wilmer 1 Sacerdoti Coen, Claudio 1 Saghafi, Salman 1 Schwarzentruber, François 1 Serban, Cristina 1 Síč, Juraj 1 Slivovsky, Friedrich 1 Steen, Alexander 1 Sticksel, Christoph 1 Strejček, Jan 1 Suda, Martin 1 Szeider, Stefan 1 Ta, Quang-Trung 1 Tassi, Enrico 1 Teucke, Andreas 1 Tran, Duc-Khanh 1 Urban, Josef 1 Waldmann, Uwe Referenced in 5 Serials 10 Journal of Automated Reasoning 1 Journal of Symbolic Computation 1 AI Communications 1 MSCS. Mathematical Structures in Computer Science 1 Theory of Computing Systems Referenced in 2 Fields 50 Computer science (68-XX) 25 Mathematical logic and foundations (03-XX) Referencing Publications by Year