The following pages link to Konstantin Korovin (Q1401931):
Displaying 15 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)
- The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints (Q6076350) (← links)
