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 |