| 2005 |
|---|
| 92 | EE | Swaha Miller,
David A. Plaisted:
The Space Efficiency of OSHL.
TABLEAUX 2005: 217-230 |
| 2003 |
|---|
| 91 | EE | David A. Plaisted,
Adnan H. Yahya:
A relevance restriction strategy for automated deduction.
Artif. Intell. 144(1-2): 59-93 (2003) |
| 90 | EE | David A. Plaisted:
A Hierarchical Situation Calculus
CoRR cs.AI/0309053: (2003) |
| 89 | EE | David A. Plaisted:
An Abstract Programming System
CoRR cs.SE/0306028: (2003) |
| 88 | EE | David A. Plaisted,
Armin Biere,
Yunshan Zhu:
A satisfiability procedure for quantified Boolean formulae.
Discrete Applied Mathematics 130(2): 291-328 (2003) |
| 2002 |
|---|
| 87 | | Adnan H. Yahya,
David A. Plaisted:
Ordered Semantic Hyper Tableaux.
J. Autom. Reasoning 29(1): 17-57 (2002) |
| 2001 |
|---|
| 86 | | Nachum Dershowitz,
David A. Plaisted:
Rewriting.
Handbook of Automated Reasoning 2001: 535-610 |
| 85 | | Jürgen Avenhaus,
David A. Plaisted:
General Algorithms for Permutations in Equational Inference.
J. Autom. Reasoning 26(3): 223-268 (2001) |
| 2000 |
|---|
| 84 | EE | David A. Plaisted:
Special Cases and Substitutes for Rigid E-Unification.
Appl. Algebra Eng. Commun. Comput. 10(2): 97-152 (2000) |
| 83 | | David A. Plaisted,
Yunshan Zhu:
Ordered Semantic Hyper-Linking.
J. Autom. Reasoning 25(3): 167-217 (2000) |
| 1999 |
|---|
| 82 | EE | David A. Plaisted,
Gregory Kucherov:
The Complexity of Some Complementation Problems.
Inf. Process. Lett. 71(3-4): 159-165 (1999) |
| 81 | | Mauricio Osorio,
Bharat Jayaraman,
David A. Plaisted:
Theory of Partial-Order Programming.
Sci. Comput. Program. 34(3): 207-238 (1999) |
| 1998 |
|---|
| 80 | EE | David A. Plaisted,
Yunshan Zhu:
Replacement Rules with Definition Detection.
FTP (LNCS Selection) 1998: 80-94 |
| 79 | | M. Paramasivam,
David A. Plaisted:
Automated Deduction Techniques for Classification in Description Logic Systems.
J. Autom. Reasoning 20(3): 337-364 (1998) |
| 1997 |
|---|
| 78 | | David A. Plaisted,
Yunshan Zhu:
Ordered Semantic Hyper Linking.
AAAI/IAAI 1997: 472-477 |
| 77 | | David A. Plaisted,
Yunshan Zhu:
Equational Reasoning using AC Constraints.
IJCAI (1) 1997: 108-113 |
| 76 | | Heng Chu,
David A. Plaisted:
CLIN-S - A Semantically Guided First-Order Theorem Prover.
J. Autom. Reasoning 18(2): 183-188 (1997) |
| 75 | | M. Paramasivam,
David A. Plaisted:
RRTP - A Replacement Rule Theorem Prover.
J. Autom. Reasoning 18(2): 221-226 (1997) |
| 1996 |
|---|
| 74 | | David A. Plaisted,
Andrea Sattler-Klein:
Proof Lengths for Equational Completion.
Inf. Comput. 125(2): 154-170 (1996) |
| 1995 |
|---|
| 73 | | Shie-Jue Lee,
David A. Plaisted:
Controlling the Consumption of Storage with Sliding Priority Search in a Hyper-Linking Based Theorem Prover.
Computers and Artificial Intelligence 14(6): (1995) |
| 1994 |
|---|
| 72 | | Heng Chu,
David A. Plaisted:
Semantically Guided First-Order Theorem Proving using Hyper-Linking.
CADE 1994: 192-206 |
| 71 | | David A. Plaisted:
The Search Efficiency of Theorem Proving Strategies.
CADE 1994: 57-71 |
| 70 | | Shie-Jue Lee,
David A. Plaisted:
Problem Solving by Searching for Models with a Theorem Prover.
Artif. Intell. 69(1-2): 205-233 (1994) |
| 69 | | Heng Chu,
David A. Plaisted:
Model Finding in Semantically Guided Instance-Based Theorem Proving.
Fundam. Inform. 21(3): 221-235 (1994) |
| 68 | | Ritu Chadha,
David A. Plaisted:
Correctness of Unification Without Occur Check in Prolog.
J. Log. Program. 18(2): 99-122 (1994) |
| 1993 |
|---|
| 67 | | Heng Chu,
David A. Plaisted:
Rough Resolution: A Refinement of Resolution to Remove Large Literals.
AAAI 1993: 15-20 |
| 66 | | Heng Chu,
David A. Plaisted:
Model Finding Strategies in Semantically Guided Instance-based Theorem Proving.
ISMIS 1993: 19-28 |
| 65 | | Ritu Chadha,
David A. Plaisted:
Finding Logical Consequences Using Unskolemization.
ISMIS 1993: 255-264 |
| 64 | | David A. Plaisted:
Polynomial Time Termination and Constraint Satisfaction Tests.
RTA 1993: 405-420 |
| 63 | EE | Jean H. Gallier,
Paliath Narendran,
David A. Plaisted,
Stan Raatz,
Wayne Snyder:
An Algorithm for Finding Canonical Sets of Ground Rewrite Rules in Polynomial Time.
J. ACM 40(1): 1-16 (1993) |
| 62 | | Ritu Chadha,
David A. Plaisted:
On the Mechanical Derivation of Loop Invariants.
J. Symb. Comput. 15(5/6): 705-744 (1993) |
| 1992 |
|---|
| 61 | | Geoffrey D. Alexander,
David A. Plaisted:
Proving Equality Theorems with Hyper-Linking.
CADE 1992: 706-710 |
| 60 | | David A. Plaisted,
Geoffrey D. Alexander,
Heng Chu,
Shie-Jue Lee:
Conditional Term Rewriting and First-Order Theorem Proving.
CTRS 1992: 257-271 |
| 59 | | Shie-Jue Lee,
David A. Plaisted:
Use of Unit Clauses and Clause Splitting in Automatic Deduction.
ICCI 1992: 228-232 |
| 58 | | Xumin Nie,
David A. Plaisted:
A Semantic Backward Chaining Proof System.
Artif. Intell. 55(1): 109-128 (1992) |
| 57 | | Shie-Jue Lee,
David A. Plaisted:
Eliminating Duplication with the Hyper-Linking Strategy.
J. Autom. Reasoning 9(1): 25-42 (1992) |
| 1991 |
|---|
| 56 | | David A. Plaisted,
Richard C. Potter:
Term Rewriting: Some Experimental Results.
J. Symb. Comput. 11(1/2): 149-180 (1991) |
| 55 | | Nachum Dershowitz,
Stéphane Kaplan,
David A. Plaisted:
Rewrite, Rewrite, Rewrite, Rewrite, Rewrite, . . .
Theor. Comput. Sci. 83(1): 71-96 (1991) |
| 1990 |
|---|
| 54 | | Xumin Nie,
David A. Plaisted:
A Complete Semantic Back Chaining Proof System.
CADE 1990: 16-27 |
| 53 | | Xumin Nie,
David A. Plaisted:
Experimental Results on Subgoal Reordering.
IEEE Trans. Computers 39(6): 845-848 (1990) |
| 52 | | Jean H. Gallier,
Paliath Narendran,
David A. Plaisted,
Wayne Snyder:
Rigid E-Unification: NP-Completeness and Applications to Equational Matings
Inf. Comput. 87(1/2): 129-195 (1990) |
| 51 | | David A. Plaisted:
A Sequent-Style Model Elimination Strategy and a Positive Refinement.
J. Autom. Reasoning 6(4): 389-402 (1990) |
| 50 | | David A. Plaisted:
A Heuristic Algorithm for Small Separators in Arbitrary Graphs.
SIAM J. Comput. 19(2): 267-280 (1990) |
| 1989 |
|---|
| 49 | | Nachum Dershowitz,
Stéphane Kaplan,
David A. Plaisted:
Infinite Normal Forms (Preliminary Version).
ICALP 1989: 249-262 |
| 48 | | Bharat Jayaraman,
David A. Plaisted:
Programming with Equations, Subsets, and Relations.
NACLP 1989: 1051-1068 |
| 47 | | Xumin Nie,
David A. Plaisted:
Refinements to Depth-First Iterative-Deepening Search in Automatic Theorem Proving.
Artif. Intell. 41(2): 223-235 (1989) |
| 1988 |
|---|
| 46 | | Jean H. Gallier,
Paliath Narendran,
David A. Plaisted,
Stan Raatz,
Wayne Snyder:
Finding Canonical Rewriting Systems Equivalent to a Finite Set of Ground Equations in Polynomial Time.
CADE 1988: 182-196 |
| 45 | | Richard C. Potter,
David A. Plaisted:
Term Rewriting: Some Experimental Results.
CADE 1988: 435-453 |
| 44 | | David A. Plaisted:
A Goal Directed Theorem Prover.
CADE 1988: 737 |
| 43 | | Jean H. Gallier,
Wayne Snyder,
Paliath Narendran,
David A. Plaisted:
Rigid E-Unification is NP-Complete
LICS 1988: 218-227 |
| 42 | | David A. Plaisted:
Non-Horn Clause Logic Programming Without Contrapositives.
J. Autom. Reasoning 4(3): 287-325 (1988) |
| 1987 |
|---|
| 41 | | David A. Plaisted:
A Logic for Conditional Term Rewriting Systems.
CTRS 1987: 212-227 |
| 40 | | Bharat Jayaraman,
David A. Plaisted:
Functional programming with sets.
FPCA 1987: 194-211 |
| 39 | | David A. Plaisted,
Jiarong Hong:
A Heuristic Triangulation Algorithm.
J. Algorithms 8(3): 405-437 (1987) |
| 1986 |
|---|
| 38 | | David A. Plaisted:
Abstraction Using Generalization Functions.
CADE 1986: 365-376 |
| 37 | | Steven Greenbaum,
David A. Plaisted:
The Illinois Prover: A General Purpose Resolution Theorem Prover.
CADE 1986: 685-687 |
| 36 | | David A. Plaisted:
A Simple Non-Termination Test for the Knuth-Bendix Method.
CADE 1986: 79-88 |
| 35 | | J. Dean Brock,
Amos Omondi,
David A. Plaisted:
A Multiprocessor Architecture for Medium-Grain Parallelism.
ICDCS 1986: 167-174 |
| 34 | | David A. Plaisted:
The Denotional Semantics of Nondeterministic Recursive Programs using Coherent Relations
LICS 1986: 163-174 |
| 33 | | David A. Plaisted:
A Decision Procedure for Combinations of Propositional Temporal Logic and Other Specialized Theories.
J. Autom. Reasoning 2(2): 171-190 (1986) |
| 32 | | David A. Plaisted,
Steven Greenbaum:
A Structure-Preserving Clause Form Translation.
J. Symb. Comput. 2(3): 293-304 (1986) |
| 1985 |
|---|
| 31 | | David A. Plaisted:
An Architecture for fast Data Movement in the FFP Machine.
FPCA 1985: 147-163 |
| 30 | | Leo Bachmair,
David A. Plaisted:
Associative Path Orderings.
RTA 1985: 241-254 |
| 29 | | Nachum Dershowitz,
David A. Plaisted:
Logic Programming cum Applicative Programming.
SLP 1985: 54-66 |
| 28 | | David A. Plaisted:
The Undecidability of Self-Embedding for Term Rewriting Systems.
Inf. Process. Lett. 20(2): 61-64 (1985) |
| 27 | | David A. Plaisted:
Semantic Confluence Tests and Completion Methods
Information and Control 65(2/3): 182-215 (1985) |
| 26 | | Leo Bachmair,
David A. Plaisted:
Termination Orderings for Associative-Commutative Rewriting Systems.
J. Symb. Comput. 1(4): 329-349 (1985) |
| 25 | | David A. Plaisted:
Complete Divisibility Problems for Slowly Utilized Oracles.
Theor. Comput. Sci. 35: 245-260 (1985) |
| 1984 |
|---|
| 24 | | David A. Plaisted:
Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving.
CADE 1984: 356-374 |
| 23 | | David A. Plaisted:
An Efficient Bug Location Algorithm.
ICLP 1984: 151-157 |
| 22 | | David A. Plaisted:
The Occur-Check Problem in Prolog.
SLP 1984: 272-280 |
| 21 | | David A. Plaisted:
Heuristic Matching for Graphs Satisfying the Triangle Inequality.
J. Algorithms 5(2): 163-179 (1984) |
| 20 | | David A. Plaisted:
Complete Problems in the First-Order Predicate Calculus.
J. Comput. Syst. Sci. 29(1): 8-35 (1984) |
| 19 | | David A. Plaisted:
The Occur-Check Problem in Prolog.
New Generation Comput. 2(4): 309-322 (1984) |
| 18 | | David A. Plaisted:
New NP-Hard and NP-Complete Polynomial and Integer Divisibility Problems.
Theor. Comput. Sci. 31: 125-138 (1984) |
| 1983 |
|---|
| 17 | | Nachum Dershowitz,
Jieh Hsiang,
N. Alan Josephson,
David A. Plaisted:
Associative-Commutative Rewriting.
IJCAI 1983: 940-944 |
| 16 | | David A. Plaisted:
A Low Level Language for Obtaining Decision Procedure for Classes of temporal Logics.
Logic of Programs 1983: 403-420 |
| 15 | | Kenneth J. Supowit,
Edward M. Reingold,
David A. Plaisted:
The Traveling Salesman Problem and Minimum Matching in the Unit Square.
SIAM J. Comput. 12(1): 144-156 (1983) |
| 1982 |
|---|
| 14 | | Steven Greenbaum,
A. Nagasaka,
Paul O'Rorke,
David A. Plaisted:
Comparison of Natural Deduction and Locking Resolution Implementations.
CADE 1982: 159-171 |
| 13 | | David A. Plaisted:
A Simplified Problem Reduction Format.
Artif. Intell. 18(2): 227-261 (1982) |
| 1981 |
|---|
| 12 | | David A. Plaisted:
Theorem Proving with Abstraction.
Artif. Intell. 16(1): 47-108 (1981) |
| 1980 |
|---|
| 11 | | David A. Plaisted:
An Efficient Relevance Criterion for Mechanical Theorem Proving.
AAAI 1980: 79-83 |
| 10 | | David A. Plaisted:
Abstraction Mappings in Mechanical Theorem Proving.
CADE 1980: 264-280 |
| 9 | | David A. Plaisted:
On the Distribution of Independent Formulae of Number Theory
STOC 1980: 39-44 |
| 8 | | Kenneth J. Supowit,
David A. Plaisted,
Edward M. Reingold:
Heuristics for Weighted Perfect Matching
STOC 1980: 398-419 |
| 7 | | David A. Plaisted:
The Application of Multivariate Polynomials to Inference Rules and Partial Tests for Unsatisfiability.
SIAM J. Comput. 9(4): 698-705 (1980) |
| 1979 |
|---|
| 6 | | David A. Plaisted:
Fast Verification, Testing, and Generation of Large Primes.
Theor. Comput. Sci. 9: 1-16 (1979) |
| 1978 |
|---|
| 5 | | David A. Plaisted:
Some Polynomial and Integer Divisibility problems are NP-Hard.
SIAM J. Comput. 7(4): 458-464 (1978) |
| 1977 |
|---|
| 4 | | David A. Plaisted:
New NP-Hard and NP-Complete Polynomial and Integer Divisibility Problems
FOCS 1977: 241-253 |
| 3 | | David A. Plaisted:
Sparse Complex Polynomials and Polynomial Reducibility.
J. Comput. Syst. Sci. 14(2): 210-221 (1977) |
| 1976 |
|---|
| 2 | | David A. Plaisted:
Some Polynomial and Integer Divisibility Problems Are NP-Hard
FOCS 1976: 264-267 |
| 1972 |
|---|
| 1 | | David A. Plaisted:
Flowchart Schemata with Counters
STOC 1972: 44-51 |
