1

Theorem proving with abstraction

David A. Plaisted
Journal:
Artificial Intelligence
Year:
1981
Language:
english
File:
PDF, 2.84 MB
english, 1981
2

A Bernoulli's Law Lab in a Bottle

Guerra, David, Plaisted, Aaron, Smith, Michael
Journal:
The Physcis Teacher
Year:
2005
Language:
english
File:
PDF, 470 KB
english, 2005
3

Refinements to depth-first iterative-deepening search in automatic theorem proving

Xumin Nie, David A. Plaisted
Journal:
Artificial Intelligence
Year:
1989
Language:
english
File:
PDF, 639 KB
english, 1989
4

On the mechanical derivation of loop invariants

Ritu Chadha, David A. Plaisted
Journal:
Journal of Symbolic Computation
Year:
1993
Language:
english
File:
PDF, 2.23 MB
english, 1993
7

A simplified problem reduction format

David A. Plaisted
Journal:
Artificial Intelligence
Year:
1982
Language:
english
File:
PDF, 1.64 MB
english, 1982
8

A semantic backward chaining proof system

Xumin Nie, David A. Plaisted
Journal:
Artificial Intelligence
Year:
1992
Language:
english
File:
PDF, 967 KB
english, 1992
9

Problem solving by searching for models with a theorem prover

Shie-Jue Lee, David A. Plaisted
Journal:
Artificial Intelligence
Year:
1994
Language:
english
File:
PDF, 1.39 MB
english, 1994
10

A heuristic triangulation algorithm

David A Plaisted, Jiarong Hong
Journal:
Journal of Algorithms
Year:
1987
Language:
english
File:
PDF, 1.61 MB
english, 1987
11

A relevance restriction strategy for automated deduction

David A Plaisted, Adnan Yahya
Journal:
Artificial Intelligence
Year:
2003
Language:
english
File:
PDF, 295 KB
english, 2003
13

Automated theorem proving

Plaisted, David A.
Journal:
Wiley Interdisciplinary Reviews: Cognitive Science
Year:
2014
Language:
english
File:
PDF, 629 KB
english, 2014
15

Complete problems in the first-order predicate calculus

David A. Plaisted
Journal:
Journal of Computer and System Sciences
Year:
1984
Language:
english
File:
PDF, 2.02 MB
english, 1984
16

An NP-complete matching problem

David A. Plaisted, Samuel Zaks
Journal:
Discrete Applied Mathematics
Year:
1980
Language:
english
File:
PDF, 847 KB
english, 1980
17

A model for the parallel execution of subset-equational languages

Amos R. Omondi, David A. Plaisted
Journal:
Future Generation Computer Systems
Year:
1995
Language:
english
File:
PDF, 2.68 MB
english, 1995
18

Heuristic matching for graphs satisfying the triangle inequality

David A Plaisted
Journal:
Journal of Algorithms
Year:
1984
Language:
english
File:
PDF, 1.07 MB
english, 1984
19

Fast verification, testing, and generation of large primes

David A. Plaisted
Journal:
Theoretical Computer Science
Year:
1979
Language:
english
File:
PDF, 1.80 MB
english, 1979
20

New NP-hard and NP-complete polynomial and integer divisibility problems

David A. Plaisted
Journal:
Theoretical Computer Science
Year:
1984
Language:
english
File:
PDF, 1.47 MB
english, 1984
21

Complete divisibility problems for slowly utilized oracles

David A. Plaisted
Journal:
Theoretical Computer Science
Year:
1985
Language:
english
File:
PDF, 1.10 MB
english, 1985
22

Correctness of unification without occur check in prolog

Ritu Chadha, David A. Plaisted
Journal:
The Journal of Logic Programming
Year:
1994
Language:
english
File:
PDF, 1.83 MB
english, 1994
23

The complexity of some complementation problems

David A. Plaisted, Gregory Kucherov
Journal:
Information Processing Letters
Year:
1999
Language:
english
File:
PDF, 89 KB
english, 1999
24

Sparse complex polynomials and polynomial reducibility

David Alan Plaisted
Journal:
Journal of Computer and System Sciences
Year:
1977
Language:
english
File:
PDF, 532 KB
english, 1977
25

A satisfiability procedure for quantified Boolean formulae

David A. Plaisted, Armin Biere, Yunshan Zhu
Journal:
Discrete Applied Mathematics
Year:
2003
Language:
english
File:
PDF, 301 KB
english, 2003
26

Theory of partial-order programming

Mauricio Osorio, Bharat Jayaraman, David A. Plaisted
Journal:
Science of Computer Programming
Year:
1999
Language:
english
File:
PDF, 2.18 MB
english, 1999
27

Term rewriting: Some experimental results

David A. Plaisted, Richard C. Potter
Journal:
Journal of Symbolic Computation
Year:
1991
Language:
english
File:
PDF, 1.57 MB
english, 1991
28

Termination orderings for associative-commutative rewriting systems

Leo Bachmair, David A. Plaisted
Journal:
Journal of Symbolic Computation
Year:
1985
Language:
english
File:
PDF, 1.31 MB
english, 1985
29

A Structure-preserving Clause Form Translation

David A. Plaisted, Steven Greenbaum
Journal:
Journal of Symbolic Computation
Year:
1986
Language:
english
File:
PDF, 724 KB
english, 1986
30

A sequent-style model elimination strategy and a positive refinement

David A. Plaisted
Journal:
Journal of Automated Reasoning
Year:
1990
Language:
english
File:
PDF, 689 KB
english, 1990
31

Non-Horn clause logic programming without contrapositives

David A. Plaisted
Journal:
Journal of Automated Reasoning
Year:
1988
Language:
english
File:
PDF, 1.72 MB
english, 1988
32

Eliminating duplication with the hyper-linking strategy

Shie-Jue Lee, David A. Plaisted
Journal:
Journal of Automated Reasoning
Year:
1992
Language:
english
File:
PDF, 1.01 MB
english, 1992
34

Special Cases and Substitutes for Rigid E-Unification

David A. Plaisted
Journal:
Applicable Algebra in Engineering, Communication and Computing
Year:
2000
Language:
english
File:
PDF, 286 KB
english, 2000
35

Rewrite, rewrite, rewrite, rewrite, rewrite, …

Nachum Dershowitz, Stéphane Kaplan, David A. Plaisted
Journal:
Theoretical Computer Science
Year:
1991
Language:
english
File:
PDF, 1.67 MB
english, 1991
36

RRTP - A Replacement Rule Theorem Prover

M. Paramasivam, David A. Plaisted
Journal:
Journal of Automated Reasoning
Year:
1997
Language:
english
File:
PDF, 98 KB
english, 1997
38

CLIN-S - A Semantically Guided First-Order Theorem Prover

Heng Chu, David A. Plaisted
Journal:
Journal of Automated Reasoning
Year:
1997
Language:
english
File:
PDF, 117 KB
english, 1997
39

Ordered Semantic Hyper-Linking

David A. Plaisted, Yunshan Zhu
Journal:
Journal of Automated Reasoning
Year:
2000
Language:
english
File:
PDF, 292 KB
english, 2000
40

General Algorithms for Permutations in Equational Inference

Jürgen Avenhaus, David A. Plaisted
Journal:
Journal of Automated Reasoning
Year:
2001
Language:
english
File:
PDF, 269 KB
english, 2001
41

Ordered Semantic Hyper Tableaux

Adnan Yahya, David A. Plaisted
Journal:
Journal of Automated Reasoning
Year:
2002
Language:
english
File:
PDF, 244 KB
english, 2002
42

Proof Lengths for Equational Completion

David A. Plaisted, Andrea Sattler-Klein
Journal:
Information and Computation
Year:
1996
Language:
english
File:
PDF, 595 KB
english, 1996
45

The occur-check problem in Prolog

David A. Plaisted
Journal:
New Generation Computing
Year:
1984
Language:
english
File:
PDF, 745 KB
english, 1984
46

The undecidability of self-embedding for term rewriting systems

David A. Plaisted
Journal:
Information Processing Letters
Year:
1985
Language:
english
File:
PDF, 306 KB
english, 1985
48

Semantic confluence tests and completion methods

David A. Plaisted
Journal:
Information and Control
Year:
1985
Language:
english
File:
PDF, 1.80 MB
english, 1985
49

Some Polynomial and Integer Divisibility Problems are $NP$-Hard

Plaisted, David
Journal:
SIAM Journal on Computing
Year:
1978
Language:
english
File:
PDF, 829 KB
english, 1978
50

A Heuristic Algorithm for Small Separators in Arbitrary Graphs

Plaisted, David A.
Journal:
SIAM Journal on Computing
Year:
1990
Language:
english
File:
PDF, 1.96 MB
english, 1990