iProver
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.
Keywords for this software
References in zbMATH (referenced in 49 articles )
Showing results 1 to 20 of 49.
Sorted by year (- 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)
- Teucke, Andreas; Weidenbach, Christoph: SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment (2020)
- Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
- Rawson, Michael; Reger, Giles: A neurally-guided, parallel theorem prover (2019)
- Rawson, Michael; Reger, Giles: Old or heavy? Decaying gracefully with age/weight shapes (2019)
- Reis, Giselle; Woltzenlogel Paleo, Bruno: Complexity of translations from resolution to sequent calculus (2019)
- Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
- 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)
- Lopez Hernandez, Julio Cesar; Korovin, Konstantin: An abstraction-refinement framework for reasoning with large theories (2018)
- Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
- Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: inference system and completeness (2017)
- Itegulov, Daniyar; Slaney, John; Woltzenlogel Paleo, Bruno: Scavenger 0.1: a theorem prover based on conflict resolution (2017)
- Korhonen, Tuukka; Berg, Jeremias; Saikko, Paul; Järvisalo, Matti: Maxpre: an extended maxsat preprocessor (2017)
- Reynolds, Andrew; Iosif, Radu; Serban, Cristina: Reasoning in the Bernays-Schönfinkel-Ramsey fragment of separation logic (2017)
- Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
- Dross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei: Adding decision procedures to SMT solvers using axioms with triggers (2016)
- Khasidashvili, Zurab; Korovin, Konstantin: Predicate elimination for preprocessing in first-order theorem proving (2016)
- Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
- Reger, Giles; Suda, Martin; Voronkov, Andrei: Finding finite models in multi-sorted first-order logic (2016)
- Alagi, Gábor; Weidenbach, Christoph: NRCL -- a model building approach to the Bernays-Schönfinkel fragment (2015)