1999 | ||
---|---|---|
76 | David A. Plaisted, Gregory Kucherov: The Complexity of Some Complementation Problems. Information Processing Letters 71(3-4): 159-165 (1999) | |
75 | Mauricio Osorio, Bharat Jayaraman, David A. Plaisted: Theory of Partial-Order Programming. Science of Computer Programming 34(3): 207-238 (1999) | |
1998 | ||
74 | M. Paramasivam, David A. Plaisted: Automated Deduction Techniques for Classification in Description Logic Systems. Journal of Automated Reasoning 20(3): 337-364 (1998) | |
1997 | ||
73 | David A. Plaisted, Yunshan Zhu: Ordered Semantic Hyper Linking. AAAI/IAAI 1997: 472-477 | |
72 | David A. Plaisted, Yunshan Zhu: Equational Reasoning using AC Constraints. IJCAI (1) 1997: 108-113 | |
71 | Heng Chu, David A. Plaisted: CLIN-S - A Semantically Guided First-Order Theorem Prover. Journal of Automated Reasoning 18(2): 183-188 (1997) | |
70 | M. Paramasivam, David A. Plaisted: RRTP - A Replacement Rule Theorem Prover. Journal of Automated Reasoning 18(2): 221-226 (1997) | |
1996 | ||
69 | David A. Plaisted, Andrea Sattler-Klein: Proof Lengths for Equational Completion. Information and Computation 125(2): 154-170 (1996) | |
1994 | ||
68 | Heng Chu, David A. Plaisted: Semantically Guided First-Order Theorem Proving using Hyper-Linking. CADE 1994: 192-206 | |
67 | David A. Plaisted: The Search Efficiency of Theorem Proving Strategies. CADE 1994: 57-71 | |
66 | Shie-Jue Lee, David A. Plaisted: Problem Solving by Searching for Models with a Theorem Prover. Artificial Intelligence 69(1-2): 205-233 (1994) | |
65 | Heng Chu, David A. Plaisted: Model Finding in Semantically Guided Instance-Based Theorem Proving. Fundamenta Informaticae 21(3): 221-235 (1994) | |
64 | Ritu Chandha, David A. Plaisted: Correctness of Unification Without Occur Check in Prolog. JLP 18(2): 99-122 (1994) | |
1993 | ||
63 | Heng Chu, David A. Plaisted: Rough Resolution: A Refinement of Resolution to Remove Large Literals. AAAI 1993: 15-20 | |
62 | Heng Chu, David A. Plaisted: Model Finding Strategies in Semantically Guided Instance-based Theorem Proving. ISMIS 1993: 19-28 | |
61 | Ritu Chadha, David A. Plaisted: Finding Logical Consequences Using Unskolemization. ISMIS 1993: 255-264 | |
60 | David A. Plaisted: Polynomial Time Termination and Constraint Satisfaction Tests. RTA 1993: 405-420 | |
59 | 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. JACM 40(1): 1-16 (1993) | |
58 | Ritu Chadha, David A. Plaisted: On the Mechanical Derivation of Loop Invariants. JSC 15(5/6): 705-744 (1993) | |
1992 | ||
57 | Geoffrey D. Alexander, David A. Plaisted: Proving Equality Theorems with Hyper-Linking. CADE 1992: 706-710 | |
56 | David A. Plaisted, Geoffrey D. Alexander, Heng Chu, Shie-Jue Lee: Conditional Term Rewriting and First-Order Theorem Proving. CTRS 1992: 257-271 | |
55 | Xumin Nie, David A. Plaisted: A Semantic Backward Chaining Proof System. Artificial Intelligence 55(1): 109-128 (1992) | |
54 | Shie-Jue Lee, David A. Plaisted: Eliminating Duplication with the Hyper-Linking Strategy. Journal of Automated Reasoning 9(1): 25-42 (1992) | |
1991 | ||
53 | David A. Plaisted, Richard C. Potter: Term Rewriting: Some Experimental Results. JSC 11(1/2): 149-180 (1991) | |
52 | Nachum Dershowitz, Stéphane Kaplan, David A. Plaisted: Rewrite, Rewrite, Rewrite, Rewrite, Rewrite, . . . TCS 83(1): 71-96 (1991) | |
1990 | ||
51 | Xumin Nie, David A. Plaisted: A Complete Semantic Back Chaining Proof System. CADE 1990: 16-27 | |
50 | Xumin Nie, David A. Plaisted: Experimental Results on Subgoal Reordering. IEEE Transactions on Computers 39(6): 845-848 (1990) | |
49 | Jean H. Gallier, Paliath Narendran, David A. Plaisted, Wayne Snyder: Rigid E-Unification: NP-Completeness and Applications to Equational Matings. Information and Computation 87(1/2): 129-195 (1990) | |
48 | David A. Plaisted: A Sequent-Style Model Elimination Strategy and a Positive Refinement. Journal of Automated Reasoning 6(4): 389-402 (1990) | |
47 | David A. Plaisted: A Heuristic Algorithm for Small Separators in Arbitrary Graphs. SIAM J. Comput. 19(2): 267-280 (1990) | |
1989 | ||
46 | Nachum Dershowitz, Stéphane Kaplan, David A. Plaisted: Infinite Normal Forms (Preliminary Version). ICALP 1989: 249-262 | |
45 | Bharat Jayaraman, David A. Plaisted: Programming with Equations, Subsets, and Relations. NACLP 1989: 1051-1068 | |
44 | Xumin Nie, David A. Plaisted: Refinements to Depth-First Iterative-Deepening Search in Automatic Theorem Proving. Artificial Intelligence 41(2): 223-235 (1989) | |
1988 | ||
43 | 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 | |
42 | Richard C. Potter, David A. Plaisted: Term Rewriting: Some Experimental Results. CADE 1988: 435-453 | |
41 | David A. Plaisted: A Goal Directed Theorem Prover. CADE 1988: 737 | |
40 | Jean H. Gallier, Wayne Snyder, Paliath Narendran, David A. Plaisted: Rigid E-Unification is NP-Complete. LICS 1988: 218-227 | |
39 | David A. Plaisted: Non-Horn Clause Logic Programming Without Contrapositives. Journal of Automated Reasoning 4(3): 287-325 (1988) | |
1987 | ||
38 | David A. Plaisted: A Logic for Conditional Term Rewriting Systems. CTRS 1987: 212-227 | |
37 | David A. Plaisted, Jiarong Hong: A Heuristic Triangulation Algorithm. J. Algorithms 8(3): 405-437 (1987) | |
1986 | ||
36 | David A. Plaisted: Abstraction Using Generalization Functions. CADE 1986: 365-376 | |
35 | David A. Plaisted: A Simple Non-Termination Test for the Knuth-Bendix Method. CADE 1986: 79-88 | |
34 | J. Dean Brock, Amos Omondi, David A. Plaisted: A Multiprocessor Architecture for Medium-Grain Parallelism. ICDCS 1986: 167-174 | |
33 | David A. Plaisted: The Denotional Semantics of Nondeterministic Recursive Programs using Coherent Relations. LICS 1986: 163-174 | |
32 | David A. Plaisted, Steven Greenbaum: A Structure-Preserving Clause Form Translation. JSC 2(3): 293-304 (1986) | |
31 | David A. Plaisted: A Decision Procedure for Combinations of Propositional Temporal Logic and Other Specialized Theories. Journal of Automated Reasoning 2(2): 171-190 (1986) | |
1985 | ||
30 | David A. Plaisted: An Architecture for fast Data Movement in the FFP Machine. FPCA 1985: 147-163 | |
29 | Leo Bachmair, David A. Plaisted: Associative Path Orderings. RTA 1985: 241-254 | |
28 | Nachum Dershowitz, David A. Plaisted: Logic Programming cum Applicative Programming. SLP 1985: 54-66 | |
27 | David A. Plaisted: The Undecidability of Self-Embedding for Term Rewriting Systems. Information Processing Letters 20(2): 61-64 (1985) | |
26 | David A. Plaisted: Semantic Confluence Tests and Completion Methods. Information and Control 65(2/3): 182-215 (1985) | |
25 | Leo Bachmair, David A. Plaisted: Termination Orderings for Associative-Commutative Rewriting Systems. JSC 1(4): 329-349 (1985) | |
24 | David A. Plaisted: Complete Divisibility Problems for Slowly Utilized Oracles. TCS 35: 245-260 (1985) | |
1984 | ||
23 | David A. Plaisted: Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving. CADE 1984: 356-374 | |
22 | David A. Plaisted: An Efficient Bug Location Algorithm. ICLP 1984: 151-157 | |
21 | David A. Plaisted: The Occur-Check Problem in Prolog. SLP 1984: 272-280 | |
20 | David A. Plaisted: Heuristic Matching for Graphs Satisfying the Triangle Inequality. J. Algorithms 5(2): 163-179 (1984) | |
19 | David A. Plaisted: Complete Problems in the First-Order Predicate Calculus. JCSS 29(1): 8-35 (1984) | |
18 | David A. Plaisted: The Occur-Check Problem in Prolog. New Generation Computing 2(4): 309-322 (1984) | |
17 | David A. Plaisted: New NP-Hard and NP-Complete Polynomial and Integer Divisibility Problems. TCS 31: 125-138 (1984) | |
1983 | ||
16 | Nachum Dershowitz, Jieh Hsiang, Alan Josephson, David A. Plaisted: Associative-Commutative Rewriting. IJCAI 1983: 940-944 | |
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. Artificial Intelligence 18(2): 227-261 (1982) | |
1981 | ||
12 | David A. Plaisted: Theorem Proving with Abstraction. Artificial Intelligence 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. TCS 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. JCSS 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 |