David Plaisted

Plaisted's research interests include term rewriting systems, automated theorem proving, logic programming, and algorithms. His research accomplishments in theorem proving include work on the recursive path ordering,{{cite tech report| author=David A. Plaisted| title=A Recursively Defined Ordering for Proving Termination of Term Rewriting Systems|year=1978|number=R-78-943|pages=52|institution=Univ. of Illinois, Dept. of Comp. Sc.|url=https://archive.org/details/recursivelydefin943plai}}

the associative path ordering,{{cite book|author1=Bachmair, L. |author2=Plaisted, D.A. |title=Associative Path Orderings|year=1985|volume=202|pages=241–54|publisher=Springer-Verlag| editor=Jean-Pierre Jouannaud|series=LNCS}} abstraction,{{cite journal| author=David A. Plaisted|title=Theorem Proving with Abstraction|journal=Artif. Intell.|year=1981|volume=16| number=1|pages=47–108|doi=10.1016/0004-3702(81)90015-1}} the simplified and modified problem reduction formats,{{cite journal|author=David A. Plaisted|title=A Simplified Problem Reduction Format|journal=Artif. Intell.|year=1982|volume=18|number=2|pages=227–61|doi=10.1016/0004-3702(82)90041-8}}{{cite tech report|author1=Xumin Nie |author2=David A. Plaisted |title=A Semantic Variant of the Modified Problem Reduction Format|date=Jan 1989|number=TR89-101|pages=11| institution=Univ. of North Carolina at Chapel Hill| url=http://www.cs.unc.edu/techreports/89-001.pdf}} ground reducibility,{{cite journal|author=Jean H. Gallier, Paliath Narendran, David A. Plaisted, Stan Raatz, Wayne Snyder|title=An Algorithm for Finding Canonical Sets of Ground Rewrite Rules in Polynomial Time|journal=J. ACM|year=1993|volume=40|number=1|pages=1–16|url=http://cs-pub.bu.edu/fac/snyder/publications/groundcompletionJACMr.pdf|doi=10.1145/138027.138032|s2cid=820591}}

nonstandard clause form translations,{{cite journal|author1=David A. Plaisted |author2=Steven Greenbaum |title=A Structure-preserving Clause Form Translation|journal=J. Symbolic Comput.|year=1986|volume=2|issue=3 |pages=293–304|doi=10.1016/s0747-7171(86)80028-1|doi-access=free}} rigid E-unification,{{cite journal|author1=Jean H. Gallier |author2=Paliath Narendran |author3=David A. Plaisted |author4=Wayne Snyder |title=Rigid E-Unification: NP-Completeness and Applications to Equational Matings| journal=Inf. Comput.|year=1990|volume=87|number=1/2| pages=129–95|doi=10.1016/0890-5401(90)90061-l|url=https://repository.upenn.edu/cis_reports/630 |doi-access=free}} Knuth–Bendix completion,{{cite journal|author=David A. Plaisted|title=Semantic Confluence Tests and Completion Methods|journal=Information and Control|year=1985|volume=65| number=2/3|pages=182–215|doi=10.1016/s0019-9958(85)80005-x|doi-access=free}}{{cite journal|author1=David A. Plaisted |author2=Andrea Sattler-Klein |title=Proof Lengths for Equational Completion|journal=Inf. Comput.|year=1996|volume=125|number=2|pages=154–70|url=https://kluedo.ub.uni-kl.de/files/376/seki_50.pdf|doi=10.1006/inco.1996.0028}} replacement rules in theorem proving,{{cite journal|author1=Shie-Jue Lee |author2=David A. Plaisted |title=Use of replace rules in theorem proving| journal=Methods of Logic in Computer Science|year=1994| volume=1|number=2|pages=217–40}} instance-based theorem proving strategies,{{cite journal|author1=Heng Chu |author2=David A. Plaisted |title=Model Finding in Semantically Guided Instance-Based Theorem Proving| journal=Fundam. Inform.|year=1994|volume=21|number=3|pages=221–235|doi=10.3233/FI-1994-2134 }} and semantics in theorem proving.{{cite book|author1=Xumin Nie |author2=David A. Plaisted |chapter=A Complete Semantic Back Chaining Proof System|title=Proc. 10th CADE|date=July 1990|volume=449|pages=16–27|publisher=Springer|editor=M. E. Stickel|series=LNAI}}

He received his B.S. from the University of Chicago in 1970 and his Ph.D. from Stanford University in 1976. He served on the faculty of the computer science department at the University of Illinois at Urbana-Champaign until 1984, and since then has been a full professor in the Department of Computer Science at the University of North Carolina at Chapel Hill. He has authored or co-authored publications in computer science, which are cited by academics in this field. He has served on a number of program committees and on the editorial boards of a number of journals, including the Journal of Symbolic Computation, Information Processing Letters, Mathematical Systems Theory, and Fundamenta Informaticae. Plaisted spent a sabbatical at SRI International in Menlo Park, California in 1982 and 1983 and another at the Max Planck Institute for Software Systems and the University of Kaiserslautern in Germany in 1993 and 1994.{{citation needed|date=November 2015}}

{{reflist}}

• [http://www.cs.unc.edu/~plaisted Plaisted's page at UNC]
• {{DBLP|name=David A. Plaisted}}

{{Authority control}}

{{DEFAULTSORT:Plaisted, David}}

Category:University of Chicago alumni

Category:Living people

Category:Year of birth missing (living people)

Category:American computer scientists

Category:University of North Carolina at Chapel Hill faculty

Category:Stanford University alumni

Category:University of Illinois Urbana-Champaign faculty