iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)

DOI10.1007/978-3-540-71070-7_24zbMath1165.68462OpenAlexW26338302WikidataQ56020735 ScholiaQ56020735MaRDI QIDQ3541709

Konstantin Korovin

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

Mathematics Subject Classification ID

Related Items (46)

Heterogeneous heuristic optimisation and scheduling for first-order theorem proving ⋮ Adding decision procedures to SMT solvers using axioms with triggers ⋮ A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Teaching Automated Theorem Proving by Example: PyRes 1.2 ⋮ Implementing Superposition in iProver (System Description) ⋮ A First Class Boolean Sort in First-Order Theorem Proving and TPTP ⋮ Satisfiability Modulo Theories ⋮ AC simplifications and closure redundancies in the superposition calculus ⋮ CTL Model Checking in Deduction Modulo ⋮ Efficient Low-Level Connection Tableaux ⋮ Solving dependency quantified Boolean formulas using quantifier localization ⋮ The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Constraint solving for finite model finding in SMT solvers ⋮ The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ On structures of regular standard contradictions in propositional logic ⋮ Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic ⋮ NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment ⋮ Model evolution with equality -- revised and implemented ⋮ A combined superposition and model evolution calculus ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Efficient CNF Simplification Based on Binary Implication Graphs ⋮ Complexity of fixed-size bit-vector logics ⋮ Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning ⋮ Simple and Efficient Clause Subsumption with Feature Vector Indexing ⋮ Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning ⋮ A Slice-Based Decision Procedure for Type-Based Partial Orders ⋮ iProver-Eq: An Instantiation-Based Theorem Prover with Equality ⋮ On the Saturation of YAGO ⋮ The Matita Interactive Theorem Prover ⋮ Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems ⋮ Experimenting with Deduction Modulo ⋮ SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment ⋮ Finding Finite Models in Multi-sorted First-Order Logic ⋮ Predicate Elimination for Preprocessing in First-Order Theorem Proving ⋮ GRUNGE: a grand unified ATP challenge ⋮ Old or heavy? Decaying gracefully with age/weight shapes ⋮ Complexity of translations from resolution to sequent calculus ⋮ Combining Instance Generation and Resolution ⋮ The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1 ⋮ Theorem proving as constraint solving with coherent logic ⋮ Ground joinability and connectedness in the superposition calculus ⋮ Reducing higher-order theorem proving to a sequence of SAT problems ⋮ SMELS: satisfiability modulo equality with lazy superposition ⋮ Certified DQBF solving by definition extraction ⋮ DQBDD: an efficient BDD-based DQBF solver

Uses Software

• VAMPIRE
• iProver

This page was built for publication: iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)