| 2008 |
| 15 | EE | Konstantin Korovin:
iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description).
IJCAR 2008: 292-298 |
| 2007 |
| 14 | EE | Konstantin Korovin,
Andrei Voronkov:
Integrating Linear Arithmetic into Superposition Calculus.
CSL 2007: 223-237 |
| 2006 |
| 13 | EE | Harald Ganzinger,
Konstantin Korovin:
Theory Instantiation.
LPAR 2006: 497-511 |
| 2005 |
| 12 | EE | Konstantin Korovin,
Andrei Voronkov:
Random Databases and Threshold for Monotone Non-recursive Datalog.
MFCS 2005: 591-602 |
| 11 | EE | Konstantin Korovin,
Andrei Voronkov:
Knuth-Bendix constraint solving is NP-complete.
ACM Trans. Comput. Log. 6(2): 361-388 (2005) |
| 2004 |
| 10 | EE | Harald Ganzinger,
Konstantin Korovin:
Integrating Equational Reasoning into Instantiation-Based Theorem Proving.
CSL 2004: 71-84 |
| 2003 |
| 9 | EE | Konstantin Korovin,
Andrei Voronkov:
An AC-Compatible Knuth-Bendix Order.
CADE 2003: 47-59 |
| 8 | EE | Harald Ganzinger,
Konstantin Korovin:
New Directions in Instantiation-Based Theorem Proving.
LICS 2003: 55-64 |
| 7 | EE | Konstantin Korovin,
Andrei Voronkov:
Orienting Equalities with the Knuth-Bendix Order.
LICS 2003: 75- |
| 6 | EE | Konstantin Korovin,
Andrei Voronkov:
Orienting rewrite rules with the Knuth-Bendix order.
Inf. Comput. 183(2): 165-186 (2003) |
| 2002 |
| 5 | EE | Konstantin Korovin,
Andrei Voronkov:
The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures.
FSTTCS 2002: 230-240 |
| 4 | EE | Konstantin Korovin,
Andrei Voronkov:
Knuth-Bendix constraint solving is NP-complete
CoRR cs.LO/0207068: (2002) |
| 2001 |
| 3 | EE | Konstantin Korovin,
Andrei Voronkov:
Knuth-Bendix Constraint Solving Is NP-Complete.
ICALP 2001: 979-992 |
| 2 | EE | Konstantin Korovin,
Andrei Voronkov:
Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order.
RTA 2001: 137-153 |
| 2000 |
| 1 | EE | Konstantin Korovin,
Andrei Voronkov:
A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering.
LICS 2000: 291-302 |