Arrow Research search

Author name cluster

David A. Plaisted

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

18 papers
2 author rows

Possible papers

18

IJCAI Conference 1997 Conference Paper

Equational Reasoning using AC Constraints

  • David A. Plaisted
  • Yunshan Zhu

Unfailing completion is a commonly used technique for equational reasoning. For equational problems with associative and commutative functions, unfailing completion often generates a large number of rewrite rules. By comparing it with a ground completion procedure, we show that many of the rewrite rules generated are redundant. A set of consistency constraints is formulated to detect redundant rewrite rules. We propose a new completion algorithm, consistent unfailing completion, in which only consistent rewrite rules are used for critical pair generation and rewriting. Our approach does not need to use flattened terms. Thus it avoids the double exponential worst case complexity of AC unification. It also allows the use of more flexible termination orderings. We present some sufficient conditions for detecting inconsistent rewrite rules. The proposed algorithm is implemented in PROLOG.

PDF

AAAI Conference 1997 Conference Paper

Ordered Semantic Hyper Linking

  • David A. Plaisted

In this paper, we present a novel first order theorem proving strategy - ordered semantic hyper linking. Ordered semantic hyper linking (OSHL) is an instance-based refutational theorem proving strategy. It is sound and complete. OSHL has an efficient propositional decision procedure. It solves first order problems by reducing them to propositional problems. It uses natural semantics of an input problem to guide its search. It also incorporates term rewriting to handle equality. The propositional efficiency, semantic guidance and equality support allow OSHL to solve problems that are difficult for many other strategies. The efficiency of OSHL is supported by experimental study as well as complexity analysis.

PDF Details

FOCS Conference 1976 Conference Paper

Some Polynomial and Integer Divisibility Problems Are NP-Hard

  • David A. Plaisted

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.

Details