Please note: This is a beta version of the new dblp website.
You can find the classic dblp view of this page here.
You can find the classic dblp view of this page here.
David A. Plaisted
2000 – 2009
- 2005
[c43]- 2003
- [j47]David A. Plaisted, Adnan H. Yahya: A relevance restriction strategy for automated deduction. Artif. Intell. 144(1-2): 59-93 (2003)
- [j46]David A. Plaisted, Armin Biere, Yunshan Zhu: A satisfiability procedure for quantified Boolean formulae. Discrete Applied Mathematics 130(2): 291-328 (2003)
- [i2]
- [i1]
- 2002
- [j45]Adnan H. Yahya, David A. Plaisted: Ordered Semantic Hyper Tableaux. J. Autom. Reasoning 29(1): 17-57 (2002)
- 2001
- [j44]Jürgen Avenhaus, David A. Plaisted: General Algorithms for Permutations in Equational Inference. J. Autom. Reasoning 26(3): 223-268 (2001)
- [p1]
- 2000
- [j43]David A. Plaisted: Special Cases and Substitutes for Rigid E-Unification. Appl. Algebra Eng. Commun. Comput. 10(2): 97-152 (2000)
- [j42]David A. Plaisted, Yunshan Zhu: Ordered Semantic Hyper-Linking. J. Autom. Reasoning 25(3): 167-217 (2000)
1990 – 1999
- 1999
- [j41]David A. Plaisted, Gregory Kucherov: The Complexity of Some Complementation Problems. Inf. Process. Lett. 71(3-4): 159-165 (1999)
- [j40]Mauricio Osorio, Bharat Jayaraman, David A. Plaisted: Theory of Partial-Order Programming. Sci. Comput. Program. 34(3): 207-238 (1999)
- 1998
- [j39]M. Paramasivam, David A. Plaisted: Automated Deduction Techniques for Classification in Description Logic Systems. J. Autom. Reasoning 20(3): 337-364 (1998)
- [c42]David A. Plaisted, Yunshan Zhu: Replacement Rules with Definition Detection. FTP (LNCS Selection) 1998: 80-94
- 1997
- [j38]Heng Chu, David A. Plaisted: CLIN-S - A Semantically Guided First-Order Theorem Prover. J. Autom. Reasoning 18(2): 183-188 (1997)
- [j37]M. Paramasivam, David A. Plaisted: RRTP - A Replacement Rule Theorem Prover. J. Autom. Reasoning 18(2): 221-226 (1997)
- [c41]
- [c40]
- 1996
- [j36]David A. Plaisted, Andrea Sattler-Klein: Proof Lengths for Equational Completion. Inf. Comput. 125(2): 154-170 (1996)
- 1995
- [j35]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
- [j34]Shie-Jue Lee, David A. Plaisted: Problem Solving by Searching for Models with a Theorem Prover. Artif. Intell. 69(1-2): 205-233 (1994)
- [j33]Heng Chu, David A. Plaisted: Model Finding in Semantically Guided Instance-Based Theorem Proving. Fundam. Inform. 21(3): 221-235 (1994)
- [j32]Ritu Chadha, David A. Plaisted: Correctness of Unification Without Occur Check in Prolog. J. Log. Program. 18(2): 99-122 (1994)
- [j31]Shie-Jue Lee, David A. Plaisted: Use of replace rules in theorem proving. Meth. of Logic in CS 1(2): 217-240 (1994)
- [c39]
- [c38]
- 1993
- [j30]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)
- [j29]Ritu Chadha, David A. Plaisted: On the Mechanical Derivation of Loop Invariants. J. Symb. Comput. 15(5/6): 705-744 (1993)
- [c37]
- [c36]Heng Chu, David A. Plaisted: Model Finding Strategies in Semantically Guided Instance-based Theorem Proving. ISMIS 1993: 19-28
- [c35]Ritu Chadha, David A. Plaisted: Finding Logical Consequences Using Unskolemization. ISMIS 1993: 255-264
- [c34]
- 1992
- [j28]Xumin Nie, David A. Plaisted: A Semantic Backward Chaining Proof System. Artif. Intell. 55(1): 109-128 (1992)
- [j27]Shie-Jue Lee, David A. Plaisted: Eliminating Duplication with the Hyper-Linking Strategy. J. Autom. Reasoning 9(1): 25-42 (1992)
- [c33]Geoffrey D. Alexander, David A. Plaisted: Proving Equality Theorems with Hyper-Linking. CADE 1992: 706-710
- [c32]David A. Plaisted, Geoffrey D. Alexander, Heng Chu, Shie-Jue Lee: Conditional Term Rewriting and First-Order Theorem Proving. CTRS 1992: 257-271
- [c31]Shie-Jue Lee, David A. Plaisted: Use of Unit Clauses and Clause Splitting in Automatic Deduction. ICCI 1992: 228-232
- 1991
- [j26]David A. Plaisted, Richard C. Potter: Term Rewriting: Some Experimental Results. J. Symb. Comput. 11(1/2): 149-180 (1991)
- [j25]Nachum Dershowitz, Stéphane Kaplan, David A. Plaisted: Rewrite, Rewrite, Rewrite, Rewrite, Rewrite, . . . Theor. Comput. Sci. 83(1): 71-96 (1991)
- 1990
- [j24]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)
- [j23]David A. Plaisted: A Sequent-Style Model Elimination Strategy and a Positive Refinement. J. Autom. Reasoning 6(4): 389-402 (1990)
- [j22]David A. Plaisted: A Heuristic Algorithm for Small Separators in Arbitrary Graphs. SIAM J. Comput. 19(2): 267-280 (1990)
- [j21]Xumin Nie, David A. Plaisted: Experimental Results on Subgoal Reordering. IEEE Trans. Computers 39(6): 845-848 (1990)
- [c30]
1980 – 1989
- 1989
- [j20]Xumin Nie, David A. Plaisted: Refinements to Depth-First Iterative-Deepening Search in Automatic Theorem Proving. Artif. Intell. 41(2): 223-235 (1989)
- [c29]Nachum Dershowitz, Stéphane Kaplan, David A. Plaisted: Infinite Normal Forms (Preliminary Version). ICALP 1989: 249-262
- [c28]Bharat Jayaraman, David A. Plaisted: Programming with Equations, Subsets, and Relations. NACLP 1989: 1051-1068
- 1988
- [j19]David A. Plaisted: Non-Horn Clause Logic Programming Without Contrapositives. J. Autom. Reasoning 4(3): 287-325 (1988)
- [c27]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
- [c26]
- [c25]
- [c24]Jean H. Gallier, Wayne Snyder, Paliath Narendran, David A. Plaisted: Rigid E-Unification is NP-Complete. LICS 1988: 218-227
- 1987
- [j18]David A. Plaisted, Jiarong Hong: A Heuristic Triangulation Algorithm. J. Algorithms 8(3): 405-437 (1987)
- [c23]
- [c22]
- 1986
- [j17]David A. Plaisted: A Decision Procedure for Combinations of Propositional Temporal Logic and Other Specialized Theories. J. Autom. Reasoning 2(2): 171-190 (1986)
- [j16]David A. Plaisted, Steven Greenbaum: A Structure-Preserving Clause Form Translation. J. Symb. Comput. 2(3): 293-304 (1986)
- [c21]
- [c20]
- [c19]Steven Greenbaum, David A. Plaisted: The Illinois Prover: A General Purpose Resolution Theorem Prover. CADE 1986: 685-687
- [c18]J. Dean Brock, Amos Omondi, David A. Plaisted: A Multiprocessor Architecture for Medium-Grain Parallelism. ICDCS 1986: 167-174
- [c17]David A. Plaisted: The Denotional Semantics of Nondeterministic Recursive Programs using Coherent Relations. LICS 1986: 163-174
- 1985
- [j15]David A. Plaisted: Semantic Confluence Tests and Completion Methods. Information and Control 65(2/3): 182-215 (1985)
- [j14]David A. Plaisted: The Undecidability of Self-Embedding for Term Rewriting Systems. Inf. Process. Lett. 20(2): 61-64 (1985)
- [j13]Leo Bachmair, David A. Plaisted: Termination Orderings for Associative-Commutative Rewriting Systems. J. Symb. Comput. 1(4): 329-349 (1985)
- [j12]David A. Plaisted: Complete Divisibility Problems for Slowly Utilized Oracles. Theor. Comput. Sci. 35: 245-260 (1985)
- [c16]
- [c15]
- [c14]Nachum Dershowitz, David A. Plaisted: Logic Programming cum Applicative Programming. SLP 1985: 54-66
- 1984
- [j11]David A. Plaisted: Heuristic Matching for Graphs Satisfying the Triangle Inequality. J. Algorithms 5(2): 163-179 (1984)
- [j10]David A. Plaisted: Complete Problems in the First-Order Predicate Calculus. J. Comput. Syst. Sci. 29(1): 8-35 (1984)
- [j9]
- [j8]David A. Plaisted: New NP-Hard and NP-Complete Polynomial and Integer Divisibility Problems. Theor. Comput. Sci. 31: 125-138 (1984)
- [c13]David A. Plaisted: Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving. CADE 1984: 356-374
- [c12]
- [c11]
- 1983
- [j7]Kenneth J. Supowit, Edward M. Reingold, David A. Plaisted: The Travelling Salesman Problem and Minimum Matching in the Unit Square. SIAM J. Comput. 12(1): 144-156 (1983)
- [c10]Nachum Dershowitz, Jieh Hsiang, N. Alan Josephson, David A. Plaisted: Associative-Commutative Rewriting. IJCAI 1983: 940-944
- [c9]David A. Plaisted: A Low Level Language for Obtaining Decision Procedure for Classes of temporal Logics. Logic of Programs 1983: 403-420
- 1982
- [j6]
- [c8]Steven Greenbaum, A. Nagasaka, Paul O'Rorke, David A. Plaisted: Comparison of Natural Deduction and Locking Resolution Implementations. CADE 1982: 159-171
- 1981
- [j5]
- 1980
- [j4]David A. Plaisted: The Application of Multivariate Polynomials to Inference Rules and Partial Tests for Unsatisfiability. SIAM J. Comput. 9(4): 698-705 (1980)
- [c7]David A. Plaisted: An Efficient Relevance Criterion for Mechanical Theorem Proving. AAAI 1980: 79-83
- [c6]
- [c5]
- [c4]Kenneth J. Supowit, David A. Plaisted, Edward M. Reingold: Heuristics for Weighted Perfect Matching. STOC 1980: 398-419
1970 – 1979
- 1979
- [j3]David A. Plaisted: Fast Verification, Testing, and Generation of Large Primes. Theor. Comput. Sci. 9: 1-16 (1979)
- 1978
- [j2]David A. Plaisted: Some Polynomial and Integer Divisibility problems are NP-Hard. SIAM J. Comput. 7(4): 458-464 (1978)
- 1977
- [j1]David A. Plaisted: Sparse Complex Polynomials and Polynomial Reducibility. J. Comput. Syst. Sci. 14(2): 210-221 (1977)
- [c3]David A. Plaisted: New NP-Hard and NP-Complete Polynomial and Integer Divisibility Problems. FOCS 1977: 241-253
- 1976
- [c2]David A. Plaisted: Some Polynomial and Integer Divisibility Problems Are NP-Hard. FOCS 1976: 264-267
- 1972
- [c1]
Coauthor Index
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2012-12-12 17:05 CET by the dblp team