iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
From MaRDI portal
Publication:3541709
DOI10.1007/978-3-540-71070-7_24zbMath1165.68462WikidataQ56020735 ScholiaQ56020735MaRDI QIDQ3541709
Publication date: 27 November 2008
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-71070-7_24
Related Items
Constraint solving for finite model finding in SMT solvers, Simple and Efficient Clause Subsumption with Feature Vector Indexing, Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning, The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1, The CADE-28 Automated Theorem Proving System Competition – CASC-28, The Matita Interactive Theorem Prover, Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems, Experimenting with Deduction Modulo, Complexity of translations from resolution to sequent calculus, A Slice-Based Decision Procedure for Type-Based Partial Orders, iProver-Eq: An Instantiation-Based Theorem Prover with Equality, On the Saturation of YAGO, Adding decision procedures to SMT solvers using axioms with triggers, Model evolution with equality -- revised and implemented, A combined superposition and model evolution calculus, Complexity of fixed-size bit-vector logics, Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning, A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic, Certified DQBF solving by definition extraction, DQBDD: an efficient BDD-based DQBF solver, First-order automated reasoning with theories: when deduction modulo theory meets practice, SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment, GRUNGE: a grand unified ATP challenge, Old or heavy? Decaying gracefully with age/weight shapes, Reducing higher-order theorem proving to a sequence of SAT problems, SMELS: satisfiability modulo equality with lazy superposition, Extensional higher-order paramodulation in Leo-III, Finding Finite Models in Multi-sorted First-Order Logic, Predicate Elimination for Preprocessing in First-Order Theorem Proving, Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic, NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment, Efficient CNF Simplification Based on Binary Implication Graphs, Satisfiability Modulo Theories, A First Class Boolean Sort in First-Order Theorem Proving and TPTP, CTL Model Checking in Deduction Modulo, Efficient Low-Level Connection Tableaux, Combining Instance Generation and Resolution
Uses Software
