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 20 articles )
Showing results 1 to 20 of 20.
Sorted by year (- 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)
- Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
- Ji, Kailiang: CTL model checking in deduction modulo (2015)
- Kaliszyk, Cezary: Efficient low-level connection tableaux (2015)
- Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei: A first class Boolean sort in first-order theorem proving and TPTP (2015)
- Plaisted, David A.: History and prospects for first-order automated deduction (2015)
- Saghafi, Salman; Danas, Ryan; Dougherty, Daniel J.: Exploring theories with a model-finding assistant (2015)
- Gupta, Ashutosh; Kovács, Laura; Kragl, Bernhard; Voronkov, Andrei: Extensional crisis and proving identity (2014)
- Brown, Chad E.: Reducing higher-order theorem proving to a sequence of SAT problems (2013)
- Korovin, Konstantin: Non-cyclic sorts for first-order satisfiability (2013)
- Lynch, Christopher; Ta, Quang-Trung; Tran, Duc-Khanh: SMELS: satisfiability modulo equality with lazy superposition (2013)
- Reynolds, Andrew; Tinelli, Cesare; Goel, Amit; Krstić, Sava; Deters, Morgan; Barrett, Clark: Quantifier instantiation techniques for finite model finding in SMT (2013)
- Baumgartner, Peter; Pelzer, Björn; Tinelli, Cesare: Model evolution with equality -- revised and implemented (2012)
- Baumgartner, Peter; Waldmann, Uwe: A combined superposition and model evolution calculus (2011)
- Burel, Guillaume: Experimenting with deduction modulo (2011)
- Baumgartner, Peter; Thorstensen, Evgenij: Instance based methods - A brief overview (2010)
- Henzinger, Thomas A.; Hottelier, Thibaud; Kovács, Laura; Voronkov, Andrei: Invariant and type inference for matrices (2010)
- Korovin, Konstantin; Sticksel, Christoph: iProver-Eq: an instantiation-based theorem prover with equality (2010)
- Korovin, Konstantin: iProver -- an instantiation-based theorem prover for first-order logic. (System description) (2008)