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 |