Flowchart Schemata with Counters - David A. Plaisted (STOC, 1972)

Theorem proving and semantic trees. - David A. Plaisted (1976)

Sparse Complex Polynomials and Polynomial Reducibility. - David A. Plaisted (J. Comput. Syst. Sci., 1977)

Some Polynomial and Integer Divisibility problems are NP-Hard. - David A. Plaisted (SIAM J. Comput., 1978)

Fast Verification, Testing, and Generation of Large Primes. - David A. Plaisted (Theor. Comput. Sci., 1979)

An Efficient Relevance Criterion for Mechanical Theorem Proving. - David A. Plaisted (AAAI, 1980)

Abstraction Mappings in Mechanical Theorem Proving. - David A. Plaisted (CADE, 1980)

On the Distribution of Independent Formulae of Number Theory - David A. Plaisted (STOC, 1980)

Heuristics for Weighted Perfect Matching - Kenneth J. Supowit; David A. Plaisted; Edward M. Reingold (STOC, 1980)

An NP-complete matching problem. - David A. Plaisted; Samuel Zaks (Discret. Appl. Math., 1980)

The Application of Multivariate Polynomials to Inference Rules and Partial Tests for Unsatisfiability. - David A. Plaisted (SIAM J. Comput., 1980)

Theorem Proving with Abstraction. - David A. Plaisted (Artif. Intell., 1981)

Comparison of Natural Deduction and Locking Resolution Implementations. - Steven Greenbaum; A. Nagasaka; Paul O'Rorke; David A. Plaisted (CADE, 1982)

A Simplified Problem Reduction Format. - David A. Plaisted (Artif. Intell., 1982)

Associative-Commutative Rewriting. - Nachum Dershowitz; Jieh Hsiang; N. Alan Josephson; David A. Plaisted (IJCAI, 1983)

A Low Level Language for Obtaining Decision Procedure for Classes of temporal Logics. - David A. Plaisted (Logic of Programs, 1983)

The Travelling Salesman Problem and Minimum Matching in the Unit Square. - Kenneth J. Supowit; Edward M. Reingold; David A. Plaisted (SIAM J. Comput., 1983)

Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving. - David A. Plaisted (CADE, 1984)

An Efficient Bug Location Algorithm. - David A. Plaisted (ICLP, 1984)

Heuristic Matching for Graphs Satisfying the Triangle Inequality. - David A. Plaisted (J. Algorithms, 1984)

Complete Problems in the First-Order Predicate Calculus. - David A. Plaisted (J. Comput. Syst. Sci., 1984)

The Occur-Check Problem in Prolog. - David A. Plaisted (New Gener. Comput., 1984)

New NP-Hard and NP-Complete Polynomial and Integer Divisibility Problems. - David A. Plaisted (Theor. Comput. Sci., 1984)

An Architecture for fast Data Movement in the FFP Machine. - David A. Plaisted (FPCA, 1985)

Associative Path Orderings. - Leo Bachmair; David A. Plaisted (RTA, 1985)

Logic Programming cum Applicative Programming. - Nachum Dershowitz; David A. Plaisted (SLP, 1985)

Semantic Confluence Tests and Completion Methods - David A. Plaisted (Inf. Control., 1985)

The Undecidability of Self-Embedding for Term Rewriting Systems. - David A. Plaisted (Inf. Process. Lett., 1985)

Termination Orderings for Associative-Commutative Rewriting Systems. - Leo Bachmair; David A. Plaisted (J. Symb. Comput., 1985)

Conditional rewriting. - Nachum Dershowitz; David A. Plaisted (ACM SIGSOFT Softw. Eng. Notes, 1985)

Complete Divisibility Problems for Slowly Utilized Oracles. - David A. Plaisted (Theor. Comput. Sci., 1985)

The Illinois Prover: A General Purpose Resolution Theorem Prover. - Steven Greenbaum; David A. Plaisted (CADE, 1986)

A Simple Non-Termination Test for the Knuth-Bendix Method. - David A. Plaisted (CADE, 1986)

Abstraction Using Generalization Functions. - David A. Plaisted (CADE, 1986)

A Multiprocessor Architecture for Medium-Grain Parallelism. - J. Dean Brock; Amos R. Omondi; David A. Plaisted (ICDCS, 1986)

Extensions to functional programming in Scheme. - David A. Plaisted; J. W. Curry (ISMIS, 1986)

The Denotional Semantics of Nondeterministic Recursive Programs using Coherent Relations - David A. Plaisted (LICS, 1986)

A Decision Procedure for Combinations of Propositional Temporal Logic and Other Specialized Theories. - David A. Plaisted (J. Autom. Reason., 1986)

A Structure-Preserving Clause Form Translation. - David A. Plaisted; Steven Greenbaum (J. Symb. Comput., 1986)

A Logic for Conditional Term Rewriting Systems. - David A. Plaisted (CTRS, 1987)

Functional programming with sets. - Bharat Jayaraman; David A. Plaisted (FPCA, 1987)

A Heuristic Triangulation Algorithm. - David A. Plaisted; Jiarong Hong (J. Algorithms, 1987)

Finding Canonical Rewriting Systems Equivalent to a Finite Set of Ground Equations in Polynomial Time. - Jean H. Gallier; Paliath Narendran; David A. Plaisted; Stan Raatz; Wayne Snyder (CADE, 1988)

A Goal Directed Theorem Prover. - David A. Plaisted (CADE, 1988)

Rigid E-Unification is NP-Complete - Jean H. Gallier; Wayne Snyder; Paliath Narendran; David A. Plaisted (LICS, 1988)

Non-Horn Clause Logic Programming Without Contrapositives. - David A. Plaisted (J. Autom. Reason., 1988)

Infinite Normal Forms (Preliminary Version). - Nachum Dershowitz; Stéphane Kaplan; David A. Plaisted (ICALP, 1989)

Programming with Equations, Subsets, and Relations. - Bharat Jayaraman; David A. Plaisted (NACLP, 1989)

Refinements to Depth-First Iterative-Deepening Search in Automatic Theorem Proving. - Xumin Nie; David A. Plaisted (Artif. Intell., 1989)

A Complete Semantic Back Chaining Proof System. - Xumin Nie; David A. Plaisted (CADE, 1990)

Rigid E-Unification: NP-Completeness and Applications to Equational Matings - Jean H. Gallier; Paliath Narendran; David A. Plaisted; Wayne Snyder (Inf. Comput., 1990)

A Sequent-Style Model Elimination Strategy and a Positive Refinement. - David A. Plaisted (J. Autom. Reason., 1990)

A Heuristic Algorithm for Small Separators in Arbitrary Graphs. - David A. Plaisted (SIAM J. Comput., 1990)

Experimental Results on Subgoal Reordering. - Xumin Nie; David A. Plaisted (IEEE Trans. Computers, 1990)

Term Rewriting: Some Experimental Results. - David A. Plaisted; Richard C. Potter (J. Symb. Comput., 1991)

Rewrite, Rewrite, Rewrite, Rewrite, Rewrite, . . . - Nachum Dershowitz; Stéphane Kaplan; David A. Plaisted (Theor. Comput. Sci., 1991)

Proving Equality Theorems with Hyper-Linking. - Geoffrey D. Alexander; David A. Plaisted (CADE, 1992)

Conditional Term Rewriting and First-Order Theorem Proving. - David A. Plaisted; Geoffrey D. Alexander; Heng Chu; Shie-Jue Lee (CTRS, 1992)

Use of Unit Clauses and Clause Splitting in Automatic Deduction. - Shie-Jue Lee; David A. Plaisted (ICCI, 1992)

A Semantic Backward Chaining Proof System. - Xumin Nie; David A. Plaisted (Artif. Intell., 1992)

Eliminating Duplication with the Hyper-Linking Strategy. - Shie-Jue Lee; David A. Plaisted (J. Autom. Reason., 1992)

Rough Resolution: A Refinement of Resolution to Remove Large Literals. - Heng Chu; David A. Plaisted (AAAI, 1993)

Finding Logical Consequences Using Unskolemization. - Ritu Chadha; David A. Plaisted (ISMIS, 1993)

Model Finding Strategies in Semantically Guided Instance-based Theorem Proving. - Heng Chu; David A. Plaisted (ISMIS, 1993)

Polynomial Time Termination and Constraint Satisfaction Tests. - David A. Plaisted (RTA, 1993)

An Algorithm for Finding Canonical Sets of Ground Rewrite Rules in Polynomial Time. - Jean H. Gallier; Paliath Narendran; David A. Plaisted; Stan Raatz; Wayne Snyder (J. ACM, 1993)

On the Mechanical Derivation of Loop Invariants. - Ritu Chadha; David A. Plaisted (J. Symb. Comput., 1993)

Semantically Guided First-Order Theorem Proving using Hyper-Linking. - Heng Chu; David A. Plaisted (CADE, 1994)

The Search Efficiency of Theorem Proving Strategies. - David A. Plaisted (CADE, 1994)

Problem Solving by Searching for Models with a Theorem Prover. - Shie-Jue Lee; David A. Plaisted (Artif. Intell., 1994)

Model Finding in Semantically Guided Instance-Based Theorem Proving. - Heng Chu; David A. Plaisted (Fundam. Informaticae, 1994)

Correctness of Unification Without Occur Check in Prolog. - Ritu Chadha; David A. Plaisted (J. Log. Program., 1994)

Use of replace rules in theorem proving. - Shie-Jue Lee; David A. Plaisted (Methods Log. Comput. Sci., 1994)

Controlling the Consumption of Storage with Sliding Priority Search in a Hyper-Linking Based Theorem Prover. - Shie-Jue Lee; David A. Plaisted (Comput. Artif. Intell., 1995)

A model for the parallel execution of subset-equational languages. - Amos R. Omondi; David A. Plaisted (Future Gener. Comput. Syst., 1995)

Propositional search efficiency and first-order theorem proving. - David A. Plaisted; Geoffrey D. Alexander (Satisfiability Problem: Theory and Applications, 1996)

Proof Lengths for Equational Completion. - David A. Plaisted; Andrea Sattler-Klein (Inf. Comput., 1996)

The efficiency of theorem proving strategies - a comparative and asymptotic analysis. - David A. Plaisted; Yunshan Zhu (Vieweg, 1997)

Equational Reasoning using AC Constraints. - David A. Plaisted; Yunshan Zhu (IJCAI (1), 1997)

CLIN-S - A Semantically Guided First-Order Theorem Prover. - Heng Chu; David A. Plaisted (J. Autom. Reason., 1997)

RRTP - A Replacement Rule Theorem Prover. - M. Paramasivam; David A. Plaisted (J. Autom. Reason., 1997)

Replacement Rules with Definition Detection. - David A. Plaisted; Yunshan Zhu (FTP (LNCS Selection), 1998)

Automated Deduction Techniques for Classification in Description Logic Systems. - M. Paramasivam; David A. Plaisted (J. Autom. Reason., 1998)

The Complexity of Some Complementation Problems. - David A. Plaisted; Gregory Kucherov (Inf. Process. Lett., 1999)

Theory of Partial-Order Programming. - Mauricio Osorio 001; Bharat Jayaraman; David A. Plaisted (Sci. Comput. Program., 1999)

Special Cases and Substitutes for Rigid E-Unification. - David A. Plaisted (Appl. Algebra Eng. Commun. Comput., 2000)

Ordered Semantic Hyper-Linking. - David A. Plaisted; Yunshan Zhu (J. Autom. Reason., 2000)

Rewriting. - Nachum Dershowitz; David A. Plaisted (Handbook of Automated Reasoning, 2001)

General Algorithms for Permutations in Equational Inference. - Jürgen Avenhaus; David A. Plaisted (J. Autom. Reason., 2001)

Ordered Semantic Hyper Tableaux. - Adnan H. Yahya; David A. Plaisted (J. Autom. Reason., 2002)

A relevance restriction strategy for automated deduction. - David A. Plaisted; Adnan H. Yahya (Artif. Intell., 2003)

A Hierarchical Situation Calculus - David A. Plaisted (CoRR, 2003)

An Abstract Programming System - David A. Plaisted (CoRR, 2003)

A satisfiability procedure for quantified Boolean formulae. - David A. Plaisted; Armin Biere; Yunshan Zhu (Discret. Appl. Math., 2003)

The Space Efficiency of OSHL. - Swaha Miller; David A. Plaisted (TABLEAUX, 2005)

Knowledge Representation and Classical Logic. - Vladimir Lifschitz; Leora Morgenstern; David A. Plaisted (Handbook of Knowledge Representation, 2008)

The Relative Power of Semantics and Unification. - David A. Plaisted; Swaha Miller (Programming Logics, 2013)

SGGS Theorem Proving: an Exposition. - Maria Paola Bonacina; David A. Plaisted (PAAR@IJCAR, 2014)

Constraint Manipulation in SGGS. - Maria Paola Bonacina; David A. Plaisted (UNIF, 2014)

History and Prospects for First-Order Automated Deduction. - David A. Plaisted (CADE, 2015)

Semantically-Guided Goal-Sensitive Reasoning: Model Representation. - Maria Paola Bonacina; David A. Plaisted (J. Autom. Reason., 2016)

Semantically-Guided Goal-Sensitive Reasoning: Inference System and Completeness. - Maria Paola Bonacina; David A. Plaisted (J. Autom. Reason., 2017)

The Aspect Calculus. - David A. Plaisted (CADE, 2019)

Properties and Extensions of Alternating Path Relevance - I. - David A. Plaisted (CoRR, 2019)

Situation Calculus by Term Rewriting. - David A. Plaisted (CoRR, 2020)

A Term-Rewriting Semantics for Imperative Style Programming. - David A. Plaisted; Lee Barnett (CoRR, 2020)

Search Spaces for Theorem Proving Strategies. - David A. Plaisted (ARCADE@CADE, 2021)

Relevance and Abstraction. - David A. Plaisted (ARCADE@CADE, 2021)

Management of the TPTP Problem Set. - Geoff Sutcliffe; David A. Plaisted (ARCADE@CADE, 2021)

Interactive Online Configurator via Boolean Satisfiability Modeling. - Tao Tao; David A. Plaisted (IAIT, 2021)

Automatic Parallelization of Programs via Software Stream Rewriting. - Tao Tao; David A. Plaisted (IPDPS Workshops, 2022)