Pages that link to "Item:Q3541709"

The following pages link to iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description) (Q3541709):

Displayed 36 items.

• Adding decision procedures to SMT solvers using axioms with triggers (Q287384) ‎ (← links)
• Model evolution with equality -- revised and implemented (Q429586) ‎ (← links)
• A combined superposition and model evolution calculus (Q438531) ‎ (← links)
• Complexity of fixed-size bit-vector logics (Q504997) ‎ (← links)
• Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) ‎ (← links)
• A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (Q831915) ‎ (← links)
• Certified DQBF solving by definition extraction (Q2118343) ‎ (← links)
• DQBDD: an efficient BDD-based DQBF solver (Q2118347) ‎ (← links)
• First-order automated reasoning with theories: when deduction modulo theory meets practice (Q2209546) ‎ (← links)
• SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment (Q2303255) ‎ (← links)
• GRUNGE: a grand unified ATP challenge (Q2305410) ‎ (← links)
• Old or heavy? Decaying gracefully with age/weight shapes (Q2305433) ‎ (← links)
• Reducing higher-order theorem proving to a sequence of SAT problems (Q2351156) ‎ (← links)
• SMELS: satisfiability modulo equality with lazy superposition (Q2351265) ‎ (← links)
• Extensional higher-order paramodulation in Leo-III (Q2666959) ‎ (← links)
• Finding Finite Models in Multi-sorted First-Order Logic (Q2818025) ‎ (← links)
• Predicate Elimination for Preprocessing in First-Order Theorem Proving (Q2818027) ‎ (← links)
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic (Q2961583) ‎ (← links)
• NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment (Q2964454) ‎ (← links)
• Efficient CNF Simplification Based on Binary Implication Graphs (Q3007684) ‎ (← links)
• Satisfiability Modulo Theories (Q3176369) ‎ (← links)
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP (Q3453107) ‎ (← links)
• CTL Model Checking in Deduction Modulo (Q3454102) ‎ (← links)
• Efficient Low-Level Connection Tableaux (Q3455764) ‎ (← links)
• Combining Instance Generation and Resolution (Q3655208) ‎ (← links)
• Constraint solving for finite model finding in SMT solvers (Q4593094) ‎ (← links)
• Simple and Efficient Clause Subsumption with Feature Vector Indexing (Q4913860) ‎ (← links)
• Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning (Q4916080) ‎ (← links)
• The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1 (Q5015602) ‎ (← links)
• The Matita Interactive Theorem Prover (Q5200015) ‎ (← links)
• Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems (Q5200021) ‎ (← links)
• Experimenting with Deduction Modulo (Q5200022) ‎ (← links)
• Complexity of translations from resolution to sequent calculus (Q5236549) ‎ (← links)
• A Slice-Based Decision Procedure for Type-Based Partial Orders (Q5747758) ‎ (← links)
• iProver-Eq: An Instantiation-Based Theorem Prover with Equality (Q5747761) ‎ (← links)
• On the Saturation of YAGO (Q5747783) ‎ (← links)