Travelled to:1 × Australia
1 × Austria
1 × Greece
1 × Switzerland
1 × The Netherlands
2 × Canada
2 × Poland
2 × USA
2 × United Kingdom
Collaborated with:A.Voronkov ∅ H.Ganzinger C.Sticksel J.C.L.Hernandez M.Kosta T.Sturm M.Emmer Z.Khasidashvili
Talks about:base (6) instanti (5) bendix (5) order (5) knuth (5) theorem (4) theori (3) reason (3) prover (2) orient (2)
Person: Konstantin Korovin
DBLP: Korovin:Konstantin
Contributed to:
2014
2012
2011201020092008
200720042003
2003
2001
200120002018Wrote 15 papers:
- SMT-2014-KorovinKS #learning #towards
- Towards Conflict-Driven Learning for Virtual Substitution (KK, MK, TS), p. 71.
- IJCAR-2012-EmmerKKSV #bound #model checking #word
- EPR-Based Bounded Model Checking at Word Level (ME, ZK, KK, CS, AV), pp. 210–224.
- CADE-2011-KorovinV #bound #linear
- Solving Systems of Linear Inequalities by Bound Propagation (KK, AV), pp. 369–383.
- IJCAR-2010-KorovinS #named #proving #similarity #theorem proving
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality (KK, CS), pp. 196–202.
- CADE-2009-Korovin #automation #reasoning #theory and practice
- Instantiation-Based Automated Reasoning: From Theory to Practice (KK), pp. 163–166.
- IJCAR-2008-Korovin #first-order #logic #named #proving #theorem proving
- iProver — An Instantiation-Based Theorem Prover for First-Order Logic (KK), pp. 292–298.
- CSL-2007-KorovinV #calculus #linear
- Integrating Linear Arithmetic into Superposition Calculus (KK, AV), pp. 223–237.
- CSL-2004-GanzingerK #equation #proving #reasoning #theorem proving
- Integrating Equational Reasoning into Instantiation-Based Theorem Proving (HG, KK), pp. 71–84.
- CADE-2003-KorovinV #order
- An AC-Compatible Knuth-Bendix Order (KK, AV), pp. 47–59.
- LICS-2003-GanzingerK #proving #theorem proving
- New Directions in Instantiation-Based Theorem Proving (HG, KK), pp. 55–64.
- LICS-2003-KorovinV #order
- Orienting Equalities with the Knuth-Bendix Order (KK, AV), p. 75–?.
- ICALP-2001-KorovinV #constraints #theorem proving
- Knuth-Bendix Constraint Solving Is NP-Complete (KK, AV), pp. 979–992.
- RTA-2001-KorovinV #order #using #verification
- Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order (KK, AV), pp. 137–153.
- LICS-2000-KorovinV #algebra
- A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering (KK, AV), pp. 291–302.
- IJCAR-2018-HernandezK #abstraction #framework #reasoning #scalability
- An Abstraction-Refinement Framework for Reasoning with Large Theories (JCLH, KK), pp. 663–679.