The following pages link to Konstantin Korovin (Q1401931):
Displaying 31 items.
- Orienting rewrite rules with the Knuth-Bendix order. (Q1401932) (← links)
- An abstraction-refinement framework for reasoning with large theories (Q1799131) (← links)
- The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints (Q2055849) (← links)
- Ground joinability and connectedness in the superposition calculus (Q2104507) (← links)
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving (Q2128804) (← links)
- AC simplifications and closure redundancies in the superposition calculus (Q2142076) (← links)
- A CDCL-style calculus for solving non-linear constraints (Q2180222) (← links)
- (Q2778876) (← links)
- Predicate Elimination for Preprocessing in First-Order Theorem Proving (Q2818027) (← links)
- Non-cyclic Sorts for First-Order Satisfiability (Q2849491) (← links)
- Skolemization Modulo Theories (Q2879139) (← links)
- Towards Conflict-Driven Learning for Virtual Substitution (Q2879330) (← links)
- EPR-Based Bounded Model Checking at Word Level (Q2908493) (← links)
- Conflict Resolution (Q3182526) (← links)
- GoRRiLA and Hard Reality (Q3457982) (← links)
- Implementing Conflict Resolution (Q3457987) (← links)
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description) (Q3541709) (← links)
- Integrating Linear Arithmetic into Superposition Calculus (Q3608415) (← links)
- (Q4415258) (← links)
- (Q4535077) (← links)
- Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning (Q4916080) (← links)
- Labelled Unit Superposition Calculi for Instantiation-Based Reasoning (Q4933325) (← links)
- Implementing Superposition in iProver (System Description) (Q5049017) (← links)
- Solving Systems of Linear Inequalities by Bound Propagation (Q5200037) (← links)
- Knuth--bendix constraint solving is NP-complete (Q5277725) (← links)
- Computer Science Logic (Q5311286) (← links)
- Theory Instantiation (Q5387915) (← links)
- Mathematical Foundations of Computer Science 2005 (Q5492892) (← links)
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality (Q5747761) (← links)
- Automated Deduction – CADE-19 (Q5900709) (← links)
- The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints (Q6076350) (← links)
