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.

In this paper we discuss design and implementation of iProver.

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.

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.

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.

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.

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.

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.

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

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.

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.

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).

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.

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.

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.

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.