The following pages link to iProver (Q21686):
Displaying 50 items.
- Semantically-guided goal-sensitive reasoning: model representation (Q287333) (← links)
- 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)
- Semantically-guided goal-sensitive reasoning: inference system and completeness (Q1707598) (← links)
- Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment (Q1742627) (← links)
- An abstraction-refinement framework for reasoning with large theories (Q1799131) (← links)
- SGGS decision procedures (Q2096457) (← links)
- Larry Wos: visions of automated reasoning (Q2102922) (← links)
- Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
- A posthumous contribution by Larry Wos: excerpts from an unpublished column (Q2102925) (← links)
- Theorem proving as constraint solving with coherent logic (Q2102932) (← links)
- Ground joinability and connectedness in the superposition calculus (Q2104507) (← links)
- SCL(EQ): SCL for first-order logic with equality (Q2104511) (← links)
- Certified DQBF solving by definition extraction (Q2118343) (← links)
- DQBDD: an efficient BDD-based DQBF solver (Q2118347) (← links)
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving (Q2128804) (← links)
- AC simplifications and closure redundancies in the superposition calculus (Q2142076) (← links)
- Solving dependency quantified Boolean formulas using quantifier localization (Q2148900) (← links)
- A neurally-guided, parallel theorem prover (Q2180215) (← 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)
- Scavenger 0.1: a theorem prover based on conflict resolution (Q2405260) (← 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)
- Non-cyclic Sorts for First-Order Satisfiability (Q2849491) (← links)
- Detection of First Order Axiomatic Theories (Q2849492) (← 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)
- History and Prospects for First-Order Automated Deduction (Q3454079) (← links)
- CTL Model Checking in Deduction Modulo (Q3454102) (← links)
- Exploring Theories with a Model-Finding Assistant (Q3454114) (← links)
- Efficient Low-Level Connection Tableaux (Q3455764) (← links)
- Extensional Crisis and Proving Identity (Q3457789) (← links)
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description) (Q3541709) (← links)
- Combining Instance Generation and Resolution (Q3655208) (← links)
- Invariant and Type Inference for Matrices (Q3656882) (← links)
- Simple and Efficient Clause Subsumption with Feature Vector Indexing (Q4913860) (← links)
- Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning (Q4916080) (← links)
