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 49 articles )

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

1 2 3 next

  1. Burel, Guillaume; Bury, Guillaume; Cauderlier, Raphaël; Delahaye, David; Halmagrand, Pierre; Hermant, Olivier: First-order automated reasoning with theories: when deduction modulo theory meets practice (2020)
  2. Teucke, Andreas; Weidenbach, Christoph: SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment (2020)
  3. Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
  4. Rawson, Michael; Reger, Giles: A neurally-guided, parallel theorem prover (2019)
  5. Rawson, Michael; Reger, Giles: Old or heavy? Decaying gracefully with age/weight shapes (2019)
  6. Reis, Giselle; Woltzenlogel Paleo, Bruno: Complexity of translations from resolution to sequent calculus (2019)
  7. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  8. Charrier, Tristan; Pinchinat, Sophie; Schwarzentruber, François: Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment (2018)
  9. Lopez Hernandez, Julio Cesar; Korovin, Konstantin: An abstraction-refinement framework for reasoning with large theories (2018)
  10. Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
  11. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: inference system and completeness (2017)
  12. Itegulov, Daniyar; Slaney, John; Woltzenlogel Paleo, Bruno: Scavenger 0.1: a theorem prover based on conflict resolution (2017)
  13. Korhonen, Tuukka; Berg, Jeremias; Saikko, Paul; Järvisalo, Matti: Maxpre: an extended maxsat preprocessor (2017)
  14. Reynolds, Andrew; Iosif, Radu; Serban, Cristina: Reasoning in the Bernays-Schönfinkel-Ramsey fragment of separation logic (2017)
  15. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
  16. Dross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei: Adding decision procedures to SMT solvers using axioms with triggers (2016)
  17. Khasidashvili, Zurab; Korovin, Konstantin: Predicate elimination for preprocessing in first-order theorem proving (2016)
  18. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  19. Reger, Giles; Suda, Martin; Voronkov, Andrei: Finding finite models in multi-sorted first-order logic (2016)
  20. Alagi, Gábor; Weidenbach, Christoph: NRCL -- a model building approach to the Bernays-Schönfinkel fragment (2015)

1 2 3 next