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.


References in zbMATH (referenced in 35 articles )

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

1 2 next

  1. Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
  2. Itegulov, Daniyar; Slaney, John; Woltzenlogel Paleo, Bruno: Scavenger 0.1: a theorem prover based on conflict resolution (2017)
  3. Korhonen, Tuukka; Berg, Jeremias; Saikko, Paul; Järvisalo, Matti: Maxpre: an extended maxsat preprocessor (2017)
  4. Reynolds, Andrew; Iosif, Radu; Serban, Cristina: Reasoning in the Bernays-Schönfinkel-Ramsey fragment of separation logic (2017)
  5. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
  6. Dross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei: Adding decision procedures to SMT solvers using axioms with triggers (2016)
  7. Khasidashvili, Zurab; Korovin, Konstantin: Predicate elimination for preprocessing in first-order theorem proving (2016)
  8. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  9. Reger, Giles; Suda, Martin; Voronkov, Andrei: Finding finite models in multi-sorted first-order logic (2016)
  10. Alagi, Gábor; Weidenbach, Christoph: NRCL -- a model building approach to the Bernays-Schönfinkel fragment (2015)
  11. Ji, Kailiang: CTL model checking in deduction modulo (2015)
  12. Kaliszyk, Cezary: Efficient low-level connection tableaux (2015)
  13. Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei: A first class Boolean sort in first-order theorem proving and TPTP (2015)
  14. Plaisted, David A.: History and prospects for first-order automated deduction (2015)
  15. Saghafi, Salman; Danas, Ryan; Dougherty, Daniel J.: Exploring theories with a model-finding assistant (2015)
  16. Gupta, Ashutosh; Kovács, Laura; Kragl, Bernhard; Voronkov, Andrei: Extensional crisis and proving identity (2014)
  17. Brown, Chad E.: Reducing higher-order theorem proving to a sequence of SAT problems (2013)
  18. Filli^atre, Jean-Christophe: One logic to use them all (2013)
  19. Korovin, Konstantin: Inst-Gen -- a modular approach to instantiation-based automated reasoning (2013)
  20. Korovin, Konstantin: Non-cyclic sorts for first-order satisfiability (2013)

1 2 next