*Towards an Abstraction-Refinement Framework for Reasoning with Large Theories*

J. C. L. Hernandez, K. Korovin

IWIL@LPAR 2017, [full paper; bibtex@dblp], Kalpa Publications in Computing, EasyChair*Computing exponentially faster: Implementing a nondeterministic universal Turing machine using DNA*

A. Currin, K. Korovin, M. Ababi, K. Roper, D. B. Kell, P. J. Day, R. D. King

Journal of The Royal Society Interface [full paper; bibtex]© Royal Society, 2017*Predicate elimination for preprocessing in first-order theorem proving*

Z. Khasidashvili, K. Korovin

SAT 2016 [pdf; bibtex@dblp]©Springer-Verlag*Computing exponentially faster: Implementing a nondeterministic universal Turing machine using DNA*

A. Currin, K. Korovin, M. Ababi, K. Roper, D. B. Kell, P. J. Day, R. D. King

arXiv.org 2016 [pdf; bibtex@dblp]*EPR-based k-induction with Counterexample Guided Abstraction Refinement*

Z. Khasidashvili, K. Korovin and D. Tsarkov

GCAI 2015 [pdf/bibtex@easychair]*Towards Conflict-Driven Learning for Virtual Substitution,*

K. Korovin, M. Kosta, T. Sturm

CASC 2014 [pdf ; bibtex@dblp]©Springer-Verlag*Skolemization Modulo Theories,*

K. Korovin and M. Veanes

ICMS 2014 [pdf; bibtex@dblp]*Instantiations, Zippers and EPR Interpolation,*

N. Bjorner, A. Gurfinkel, K. Korovin, O. Lahav

LPAR'2013 (short) [pdf; bibtex]*Non-cyclic sorts for first-order clausification,*

K. Korovin,

FroCoS'2013 [pdf; bibtex]©Springer-Verlag

*Bound Propagation for Arithmetic Reasoning in Vampire,*

I. Dragan, K. Korovin, L. Kovacs, A. Voronkov,

SYNASC'2013 [pdf; bibtex]*Inst-Gen -- A Modular Approach to Instantiation-Based Automated Reasoning,*

K. Korovin,

Programming Logics, Essays in Memory of Harald Ganzinger, 2013 [pdf, bibtex@dblp]©Springer-Verlag

*Preprocessing Techniques for First-Order Clausification,*

K. Hoder, Z. Khasidashvili, K. Korovin, A. Voronkov

FMCAD 2012 [pdf, bibtex@dblp],*EPR-Based Bounded Model Checking at Word Level,*

M. Emmer, Z. Khasidashvili, K. Korovin, C. Sticksel, A. Voronkov

IJCAR 2012 [pdf; bibtex@dblp]©Springer-Verlag,*A Note on Model Representation and Proof Extraction in the First-Order Instantiation-Based Calculus Inst-Gen,*

K. Korovin, C. Sticksel

ARW 2012 [pdf; bib]*Solving Systems of Linear Inequalities by Bound Propagation,*

K. Korovin and A. Voronkov

CADE 2011 [pdf; bibtex@dblp]©Springer-Verlag,*Implementing Conflict Resolution,*

K. Korovin, N. Tsiskaridze and A. Voronkov

PSI 2011 [pdf; bibtex@dblp]©Springer-Verlag,*GoRRiLA and Hard Reality,*

K. Korovin and A. Voronkov

PSI 2011 [pdf; bibtex@dblp]©Springer-Verlag,*Encoding Industrial Hardware Verification Problems into Effectively Propositional Logic,*

M. Emmer, Z. Khasidashvili, K. Korovin and A. Voronkov

FMCAD 2010 [pdf; bibtex@dblp]©Springer-Verlag,*Labelled Unit Superposition Calculi for Instantiation-based Reasoning,*

K. Korovin and C.Sticksel

LPAR 2010 [pdf; bibtex@dblp]©Springer-Verlag,*iProver-Eq: An Instantiation-based Theorem Prover with Equality,*

K. Korovin and C.Sticksel

IJCAR 2010 [pdf, bib ]©Springer-Verlag,*Conflict Resolution,*

K. Korovin, N. Tsiskaridze, A. Voronkov

CP'09 [pdf, bib ]©Springer-Verlag,We introduce a new method for solving systems of linear inequalities over the rationals, called conflict resolution. The method successively refines an initial assignment with the help of newly derived constraints until either the assignment becomes a solution of the system or a trivially unsatisfiable constraint is derived. We show that this method is correct and terminating. Our experimental results show that conflict resolution outperforms the Fourier-Motzkin method and the Chernikov algorithm, in some cases by orders of magnitude.

*An Invitation to Instantiation-Based Reasoning: From Theory to Practice,*Invited paper CADE 2009 [pdf, bib]

K. Korovin*iProver - An Instantiation-Based Theorem Prover for First-Order Logic,*

K. Korovin

IJCAR'08 [pdf, bib]©Springer-Verlag,

In this paper we discuss design and implementation of iProver.

*Integrating Linear Arithmetic into Superposition Calculus,*

K. Korovin, A. Voronkov

CSL'07 [pdf, bib]©Springer-Verlag,

We present a method of integrating linear rational arithmetic into superposition calculus for first-order logic. As we show, the validity problem for first-order formulas of linear arithmetic extended with non-theory function symbols is $\Pi^{1}_{1}$-complete even in the case when there are no variables over the theory sort. Therefore, there is no sound and complete calculus for this logic. Nevertheless, one of the main results of this paper is that under some finiteness assumptions it is possible to show completeness of our calculus.

*Inst-Gen -- A Modular Approach to Instantiation-Based Automated Reasoning,*

K. Korovin

Volume in memoriam of Harald Ganzinger, to appear, [pdf]

In this paper we survey results on an instantiation-based method Inst-Gen, we start by overviewing theoretical developments, describe its refinements, abstract redundancy elimination and conclude with concrete redundancy criteria and implementation issues. We also describe novel simplifications utilising propositional reasoning, which can be also applicable to calculi such as resolution.

*Theory Instantiation,*

H. Ganzinger, K. Korovin

LPAR'06 [bib (full version) ps]©Springer-Verlag,

In this paper we present a method of integrating theory reasoning into the instantiation framework. One of the distinctive features of our approach is that it allows us to employ off-the-shelf satisfiability solvers for ground clauses modulo theories, as a part of general first-order reasoning. As an application of this approach, we show how it is possible to combine the instantiation calculus with other calculi, such as ordered resolution and paramodulation.

*Random Databases and Threshold for Monotone Non-Recursive Datalog,*

K. Korovin, A. Voronkov

MFCS'05, [bib ps]©Springer-Verlag,

In this paper we define a model of randomly generated databases and show how one can compute the threshold functions for queries expressible in monotone non-recursive datalog. We also show that monotone non-recursive datalog cannot express any property with a sharp threshold. Finally, we show that non-recursive datalog has a 0-1 law for a large class of probability functions, defined in the paper.

*Integrating equational reasoning into instantiation-based theorem proving,*

H. Ganzinger, K. Korovin

CSL'04, [bib ps]©Springer-Verlag,

We continue our previous work on the instantiation-based theorem proving and present a method for integrating equational reasoning into this framework. In this approach nice properties of the instantiation-based theorem proving are preserved in particular: (i) no recombination of clauses, (ii) the length of clauses does not grow, (iii) optimal efficiency in the ground case, (iv) semantic selection, (v) redundancy criteria. The method employs a satisfiability solver for ground equational clauses together with an instance generation process based on an ordered paramodulation type calculus for literals.

*New Directions in Instantiation-Based Theorem Proving,*

H. Ganzinger, K. Korovin

LICS'03, [bib ps]©IEEE,

We consider instantiation-based theorem proving whereby instances of clauses are generated by certain inferences, and where inconsistency is detected by propositional tests (so we can employ efficient SAT checkers to guide our inference). We give a model construction proof of completeness by which restrictive inference systems as well as admissible simplification techniques can be justified. Another contribution of the paper are novel inference systems that allow one to also employ decision procedures for first-order fragments more complex than propositional logic. The decision procedure provides for an approximative consistency test, and the instance generation inference system is a means of successively refining the approximation.

*PhD thesis: Knuth-Bendix orders in automated deduction and term rewriting,*K. Korovin, The University of Manchester, 2003 [bib ps]*Orienting Equalities with the Knuth-Bendix Order,*

K. Korovin, A. Voronkov

LICS'03, [bib ps]©IEEE,

In previous work we have shown that orientability of term rewriting systems by the Knuth-Bendix order (KBO) can be done in polynomial time. In automated deduction we often need to orient equations or a union of equations and term rewriting systems. A straightforward algorithm for checking orientability of systems of equations can be based on orientability of TRS but would require to check an exponential number of possible orientations of the equations. We show how to avoid this problem, in particular we show that there exists a polynomial time algorithm which by the given system of equations and term rewriting rules can decide whether there exists a Knuth-Bendix order orienting this system, and if there exists such an order then outputs its parameters

*An AC-Compatible Knuth-Bendix Order,*

K. Korovin, A. Voronkov

CADE'03, [bib ps]©Springer-Verlag

We introduce a family of AC-compatible Knuth-Bendix simplification orders which are AC-total on ground terms. Our orders preserve attractive features of the original Knuth-Bendix orders such as existence of a polynomial-time algorithm for comparing terms; computationally efficient approximations, for instance comparing weights of terms; and preference of light terms over heavy ones. This makes these orders especially suited for automated deduction where efficient algorithms on orders are desirable.

There is a bug in the defenition of original non-ground AC-KBO in the case when the siganture contains zero-weight symbol f: in this case for each variable x, top(x) should be taken to be equal to f. Thanks to Akihisa Yamada for poiniting this out.

*The decidability of the first-order theory of the Knuth-Bendix order in the case of unary signatures,*

K. Korovin, A. Voronkov

FSTTCS'02, [bib, ps]©Springer-Verlag,

We show that the first-order theory of any Knuth-Bendix order in the case of the signatures consisting of unary function symbols and constants is decidable. Our decision procedure uses interpretation of unary terms as trees and uses decidability of the weak monadic second-order theory of binary trees. One area of applications of our result is automated deduction, since using the first-order theory of the Knuth-Bendix orders we can decide an important class of ordering constraints.

*Verifying orientability of rewrite rules using the Knuth-Bendix order,*

K. Korovin, A. Voronkov

RTA'01, [bib, (full version) ps]©Springer-Verlag, journal version has appeared in Information and Computation.

We show that the following problems can be solved in polynomial time: given a system of rewrite rules R, does there exist some KBO which orients every ground instance of every rewrite rule in R. We also show that this problem is P-complete. The second problem is deciding whether a given Knuth-Bendix ordering constraint consisting of a single inequality has a solution (we present an efficient polynomial-time algorithm).

*Knuth-Bendix constraint solving is NP-complete,*

K. Korovin, A. Voronkov

ICALP'01, [bib, (full version) ps]©Springer-Verlag journal version is to appear in ACM Transactions on Computational Logic.

We show that the problem of solving Knuth-Bendix ordering constraints is NP-complete, as a corollary we show that the existential first-order theory of term algebras with the Knuth-Bendix ordering is NP-complete.

*A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering,*

K. Korovin, A. Voronkov

LICS'00, [bib ps]©IEEE

Orderings on terms are popular in automated deduction and term rewriting. One of the important problems is to decide the existential theory (first-order theory) of term algebras with simplification orderings. In this paper we show that the existential theory of any absolutely free term algebra with the Knuth-Bendix ordering is decidable.

*Compositions of permutations and algorithmic reducibilities,*

K. Korovin

in Recursion Theory and Complexity, de Gruyter Series in Logic and Applications 2, pp89-95, 1999.

[bib ps]

In this paper we are studying the following question: for which algorithmic reducibilities the set of permutations reducible to a given set is closed under the composition. It is well-known that for the Turing reducibility the set of permutations reducible to a given set is closed under compositions and forms a group. Using this fact A. Morozov obtained a characterization of the Turing reducibility in terms of the corresponding group embeddings. In this paper we show that for the reducibilities tt,btt,wtt there exists a set (Turing reducible to 0') such that the set of permutations reducible to this set is not closed under the composition. Also we show that the following sets of permutations are not closed under the composition: {f | graph of f in } for any n>0; {f | graph of f tt-reducible to K}; {f | graph of f wtt-reducible to K}; {f | graph of f is -limit computable }, where is a creative set.

*Compositions of permutations and m-reducibility,*

K. Korovin

unpublished.

In this paper we show that for the m-reducibility for functions (which was introduced by M.Arslanov), there exists a r.e. set A such that the set of all permutations m-reducible to A is not closed under the composition.

2005-09-05