Semantic hyper-linking has recently been proposed as a way to use semantics in an instance-based theorem prover. The basic procedure is to use semantics to help generate ground instances of the input clauses until the ground clause set is unsatisfiab

In this paper, it is shown that there is an algorithm that, given by finite set E of ground equations, produces a reduced canonical rewriting system R equivalent to E in polynomial time. This algorithm based on congruence closure performs simplification steps guided by a total simplification ordering on ground terms, and it runs in time O(n 3 ) .

Rigid E-unification is a restricted kind of unification modulo equational theories, or E-unification, that arises naturally in extending Andrew's theorem proving method of matings to first-order languages with equality. This extension was first presented by J. H. Gallier, S. Raatz, and W. Snyder, who conjectured that rigid E-unification is decidable. In this paper, it is shown that rigid E-unification is NP-complete and that finite complete sets of rigid E-unifiers always exist. As a consequence, deciding whether a family of mated sets is an equational mating is an NP-complete problem. Some implications of this result regarding the complexity of theorem proving in first-order logic with equality are also discussed.

Some heuristic random polynomial time algorithms for finding good cuts in arbitrary graphs are presented. A cut is good if there are a small number of edges across the cut and if the cut divides the set of vertices somewhat evenly. The algorithms obtain cuts from solutions to randomly chosen network flow problems based on the input graph. Probabilistic bounds for the goodness of the cut obtained in terms of the goodness of an optimal separator are derived. These bounds are valid for all input graphs. There is reason to think that the algorithm will perform better than the bounds indicate.

The effect on the performance of a goal-oriented theorem power is studied on subgoal re-ordering using some simple synthetic heuristics. It is shown that subgoal reordering using these simple heuristics has a considerable impact on the performance of the prover on a large set of test problems. Some heuristics even provide equally good, and often better, performance as to the hand ordering of the input clauses. The merit of the approach seems to be that the syntactic aspect of theorem proving is considered. This approach is simple in form and cheap in its evaluation, and often provides good heuristics.>

Rigid E-unification is a restricted kind of unification modulo equational theories, or E-unification, that arises naturally in extending P. Andrews' (1981) theorem-proving method of mating to first-order languages with equality. It is shown that rigid E-unification is NP-complete and that finite complete sets of rigid E-unifiers always exist. As a consequence, deciding whether a family of mated sets is an equational mating is an NP-complete problem. Some implications of this result regarding the complexity of theorem proving in first-order logic with equality are discussed.>

We present some extensions to Scheme which increase its expressiveness within a purely declarative framework. We give constructs for sets and universal and existential quantifiers, allowing backtracking to be expressed easily. These constructs combine the expressiveness of set notation with the efficiency of lists, and have a simple semantics that is based on lists. We also give a nonstandard definition of fixpoints and a notation for it. These extensions, together with a convenient form of memo function, have been implemented as reasonably efficient macros in Scheme. The dramatic increase in conciseness of programs is illustrated by examples. These features bring us closer to executable specifications of programs and are therefore relevant for automatic program generation. We discuss extensions to Prolog-style languages that might enable them to approximate the same expressive power.

We show that the cost (length) of the shortest traveling salesman tour through n points in the unit square is, in the worst case, $\alpha _{{\text{opt}}}^{{\text{tsp}}} \sqrt n + o(\sqrt n )$, where $1.075 \leqq \alpha _{{\text{opt}}}^{{\text{tsp}}}\leqq 1.414$. The cost of the minimum matching of n points in the unit square is shown to be, in the worst case, $\alpha _{{\text{opt}}}^{{\text{mat}}} \sqrt n + o(\sqrt n )$, where $0.537 \leqq \alpha _{{\text{opt}}}^{{\text{mat}}} \leqq 0.707$. Furthermore, for each of these two problems there is an almost linear time heuristic algorithm whose Worst case cost is, neglecting lower order terms, as low as b Bible.

It follows by Gödel's incompleteness Theorem [6] that any effective sound system of logic for elementary arithmetic must be incomplete. We show that in any effective sound system of logic for elementary arithmetic, there exist valid unprovable formulae that are quite small relative to the complexity of the logical system. Also, such formulae are quite dense. In fact, the situation is about as bad as it could possibly be. That is , no infinite axiom system for elementary arithmetic can be much more compact than a listing of all the valid formulae. The unprovable formulae we construct express predicates in the classes &Sgr2 and π 2 of the Kleene arithmetic hierarchy [12]. The construction yields a set of short formulae, at least one of which must be valid and unprovable, but the construction does not tell us which one is valid and unprovable. We also construct small valid unprovable formulae expressing a relation in the class π 1 of the Kleene arithmetic hierarchy. These latter formulae are not as small. We do not know how small the independent formulae corresponding to the class π 1 are. The constructions are based on the concept of a restricted oracle, first introduced in [10] and further developed in [11]. The proofs make use of the recent result of Matijasevic [9] concerning the relationship between recursively enumerable sets and Diophantine equations.

The problem of finding near optimal perfect matchings of an even number n of vertices is considered. When the distances between the vertices satisfy the triangle inequality it is possible to get within a constant multiplicative factor of the optimal matching in time O(n2 log K) where K is the ratio of the longest to the shortest distance between vertices. Other heuristics are analyzed as well, including one that gets within a logarithmic factor of the optimal matching in time O(n2 log n). Finding an optimal weighted matching requires t(n3) time by the fastest known algorithm, so these heuristics are quite useful. When the n vertices lie in the unit (Euclidean) square, no heuristic can be guaranteed to produce a matching of cost less than [equation] in the worst case. We analyze various heuristics for this case, including one that always produces a matching costing at most [equation]. In addition, this heuristic also finds a traveling salesman tour of the n vertices costing at most [equation]. A different one of the heuristics analyzed produces asymptotically optimal results. It is also shown that asymptotically optimal traveling salesman tours can be found in O(n log n) time in the unit square.

There are some relationships between unsatisfiability of sets of clauses, and properties of polynomials in several variables. These polynomials can be used to obtain a polynomial time solution to a certain problem involving sets of clauses. Using these polynomials, one can establish a correspondence between unsatisfiable sets of clauses and a convex region of Euclidean space. Also, some inference rules based on these polynomials may provide shorter proofs of inconsistency than are possible using other known inference rules.

Most known $NP$-complete problems are stated in terms of one of an exponential number of possibilities being true. In this paper we exhibit some $NP$-hard and $NP$-complete problems which are not of this form. In addition, we exhibit some new $NP$-complete problems of a more conventional nature. Many of these problems involve divisibility properties of integers or of sparse polynomials with coefficients of $ \pm 1$. This paper extends and refines earlier results of the author.

Abstract We show that some problems involving sparse polynomials are NP-hard. For example, it is NP-hard to determine if a sparse polynomial has a root of modulus 1, and it is NP-hard to decide if two sparse polynomials are not relatively prime. Also, we show that a divisibility problem involving an unbounded number of sparse polynomials is NP-complete using a theorem of Linnik concerning the distribution of primes in arithmetic sequences. From these results it follows that certain problems involving inequalities, recurrence relations, differential equations, and eigenvalues of sparse matrices are NP-hard. Problems involving divisibility properties of two sparse polynomials, divisibility of sparse binary numbers and ring homomorphisms are also NP-hard.

In an earlier paper [1], the author showed that certain problems involving sparse polynomials and integers are NP-hard. In this paper we show that many related problems are also NP-hard. In addition, we exhibit some new NP-complete problems. Most of the new results concern problems in which the nondeterminism is "hidden". That is, the problems are not explicitly stated in terms of one of a number of possibilities being true. Furthermore, most of these problems are in the areas of number theory or the theory of functions of a complex variable. Thus there is a rich mathematical theory that can be brought to bear. These results therefore introduce a class of NP-hard and NP-complete problems different from those known previously.

The translation of a specific flowchart schema with one counter into an equivalent flowchart schema without counters is described. This result leads easily to the general translation method from one-counter flowchart schemata to zero-counter flowchart schemata. Some generalizations are then presented.