×

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

Referencing Publications by Year