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