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.

References in zbMATH (referenced in 20 articles )

Showing results 1 to 20 of 20.
Sorted by year (citations)

  1. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
  2. Dross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei: Adding decision procedures to SMT solvers using axioms with triggers (2016)
  3. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  4. Ji, Kailiang: CTL model checking in deduction modulo (2015)
  5. Kaliszyk, Cezary: Efficient low-level connection tableaux (2015)
  6. Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei: A first class Boolean sort in first-order theorem proving and TPTP (2015)
  7. Plaisted, David A.: History and prospects for first-order automated deduction (2015)
  8. Saghafi, Salman; Danas, Ryan; Dougherty, Daniel J.: Exploring theories with a model-finding assistant (2015)
  9. Gupta, Ashutosh; Kovács, Laura; Kragl, Bernhard; Voronkov, Andrei: Extensional crisis and proving identity (2014)
  10. Brown, Chad E.: Reducing higher-order theorem proving to a sequence of SAT problems (2013)
  11. Korovin, Konstantin: Non-cyclic sorts for first-order satisfiability (2013)
  12. Lynch, Christopher; Ta, Quang-Trung; Tran, Duc-Khanh: SMELS: satisfiability modulo equality with lazy superposition (2013)
  13. Reynolds, Andrew; Tinelli, Cesare; Goel, Amit; Krstić, Sava; Deters, Morgan; Barrett, Clark: Quantifier instantiation techniques for finite model finding in SMT (2013)
  14. Baumgartner, Peter; Pelzer, Björn; Tinelli, Cesare: Model evolution with equality -- revised and implemented (2012)
  15. Baumgartner, Peter; Waldmann, Uwe: A combined superposition and model evolution calculus (2011)
  16. Burel, Guillaume: Experimenting with deduction modulo (2011)
  17. Baumgartner, Peter; Thorstensen, Evgenij: Instance based methods - A brief overview (2010) ioport
  18. Henzinger, Thomas A.; Hottelier, Thibaud; Kovács, Laura; Voronkov, Andrei: Invariant and type inference for matrices (2010)
  19. Korovin, Konstantin; Sticksel, Christoph: iProver-Eq: an instantiation-based theorem prover with equality (2010)
  20. Korovin, Konstantin: iProver -- an instantiation-based theorem prover for first-order logic. (System description) (2008)