| 2019 | CADE | The Aspect Calculus. | David A. Plaisted |
| 2015 | CADE | History and Prospects for First-Order Automated Deduction. | David A. Plaisted |
| 2014 | CADE | SGGS Theorem Proving: an Exposition. | Maria Paola Bonacina, David A. Plaisted |
| 2005 | TABLEAUX | The Space Efficiency of OSHL. | Swaha Miller, David A. Plaisted |
| 1997 | AAAI | Ordered Semantic Hyper Linking. | David A. Plaisted, Yunshan Zhu |
| 1997 | IJCAI | Equational Reasoning using AC Constraints. | David A. Plaisted, Yunshan Zhu |
| 1994 | CADE | Semantically Guided First-Order Theorem Proving using Hyper-Linking. | Heng Chu, David A. Plaisted |
| 1994 | CADE | The Search Efficiency of Theorem Proving Strategies. | David A. Plaisted |
| 1993 | AAAI | Rough Resolution: A Refinement of Resolution to Remove Large Literals. | Heng Chu, David A. Plaisted |
| 1993 | ISMIS | Finding Logical Consequences Using Unskolemization. | Ritu Chadha, David A. Plaisted |
| 1993 | ISMIS | Model Finding Strategies in Semantically Guided Instance-based Theorem Proving. | Heng Chu, David A. Plaisted |
| 1992 | CADE | Proving Equality Theorems with Hyper-Linking. | Geoffrey D. Alexander, David A. Plaisted |
| 1992 | ICCI | Use of Unit Clauses and Clause Splitting in Automatic Deduction. | Shie-Jue Lee, David A. Plaisted |
| 1990 | CADE | A Complete Semantic Back Chaining Proof System. | Xumin Nie, David A. Plaisted |
| 1989 | ICALP | Infinite Normal Forms (Preliminary Version). | Nachum Dershowitz, Stphane Kaplan, David A. Plaisted |
| 1988 | CADE | 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 |
| 1988 | CADE | A Goal Directed Theorem Prover. | David A. Plaisted |
| 1988 | CADE | Term Rewriting: Some Experimental Results. | Richard C. Potter, David A. Plaisted |
| 1988 | LICS | Rigid E-Unification is NP-Complete | Jean H. Gallier, Wayne Snyder, Paliath Narendran, David A. Plaisted |
| 1986 | CADE | The Illinois Prover: A General Purpose Resolution Theorem Prover. | Steven Greenbaum, David A. Plaisted |
| 1986 | CADE | A Simple Non-Termination Test for the Knuth-Bendix Method. | David A. Plaisted |
| 1986 | CADE | Abstraction Using Generalization Functions. | David A. Plaisted |
| 1986 | ICDCS | A Multiprocessor Architecture for Medium-Grain Parallelism. | J. Dean Brock, Amos R. Omondi, David A. Plaisted |
| 1986 | ISMIS | Extensions to functional programming in Scheme. | David A. Plaisted, J. W. Curry |
| 1986 | LICS | The Denotional Semantics of Nondeterministic Recursive Programs using Coherent Relations | David A. Plaisted |
| 1984 | CADE | Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving. | David A. Plaisted |
| 1984 | ICLP | An Efficient Bug Location Algorithm. | David A. Plaisted |
| 1983 | IJCAI | Associative-Commutative Rewriting. | Nachum Dershowitz, Jieh Hsiang, N. Alan Josephson, David A. Plaisted |
| 1982 | CADE | Comparison of Natural Deduction and Locking Resolution Implementations. | Steven Greenbaum, A. Nagasaka, Paul O'Rorke, David A. Plaisted |
| 1980 | AAAI | An Efficient Relevance Criterion for Mechanical Theorem Proving. | David A. Plaisted |
| 1980 | CADE | Abstraction Mappings in Mechanical Theorem Proving. | David A. Plaisted |
| 1980 | STOC | On the Distribution of Independent Formulae of Number Theory | David A. Plaisted |
| 1980 | STOC | Heuristics for Weighted Perfect Matching | Kenneth J. Supowit, David A. Plaisted, Edward M. Reingold |
| 1977 | FOCS | New NP-Hard and NP-Complete Polynomial and Integer Divisibility Problems | David A. Plaisted |
| 1976 | FOCS | Some Polynomial and Integer Divisibility Problems Are NP-Hard | David A. Plaisted |
| 1972 | STOC | Flowchart Schemata with Counters | David A. Plaisted |