David Plaisted

Last updated

David Alan Plaisted is a computer science professor at the University of North Carolina at Chapel Hill.

Contents

Research interests

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, [1] the associative path ordering, [2] abstraction, [3] the simplified and modified problem reduction formats, [4] [5] ground reducibility, [6] nonstandard clause form translations, [7] rigid E-unification, [8] Knuth–Bendix completion, [9] [10] replacement rules in theorem proving, [11] instance-based theorem proving strategies, [12] and semantics in theorem proving. [13]

Education and career

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 ] Plaisted operates a Young Earth creation website called A Creation Perspective. [14] [15]

Related Research Articles

Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.

In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions. For example, using x,y,z as variables, the singleton equation set { cons(x,cons(x,nil)) = cons(2,y) } is a syntactic first-order unification problem that has the substitution { x ↦ 2, y ↦ cons(2,nil) } as its only solution.

In computer science, denotational semantics is an approach of formalizing the meanings of programming languages by constructing mathematical objects that describe the meanings of expressions from the languages. Other approaches providing formal semantics of programming languages include axiomatic semantics and operational semantics.

<span class="mw-page-title-main">Douglas Lenat</span> American entrepreneur and researcher in artificial intelligence

Douglas Bruce Lenat is the CEO of Cycorp, Inc. of Austin, Texas, and has been a prominent researcher in artificial intelligence. Lenat was awarded the biannual IJCAI Computers and Thought Award in 1976 for creating the machine-learning program AM. He has worked on machine learning, knowledge representation, "cognitive economy", blackboard systems, and what he dubbed in 1984 "ontological engineering". He has also worked in military simulations, and numerous projects for US government, military, intelligence, and scientific organizations. In 1980, he published a critique of conventional random-mutation Darwinism. He authored a series of articles in the Journal of Artificial Intelligence exploring the nature of heuristic rules.

In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems. In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.

The Knuth–Bendix completion algorithm is a semi-decision algorithm for transforming a set of equations into a confluent term rewriting system. When the algorithm succeeds, it effectively solves the word problem for the specified algebra.

<span class="mw-page-title-main">Logic in computer science</span> Academic discipline

Logic in computer science covers the overlap between the field of logic and that of computer science. The topic can essentially be divided into three main areas:

<span class="mw-page-title-main">Woody Bledsoe</span> American mathematician and computer scientist

Woodrow Wilson "Woody" Bledsoe was an American mathematician, computer scientist, and prominent educator. He is one of the founders of artificial intelligence (AI), making early contributions in pattern recognition and automated theorem proving. He continued to make significant contributions to AI throughout his long career.

Language equations are mathematical statements that resemble numerical equations, but the variables assume values of formal languages rather than numbers. Instead of arithmetic operations in numerical equations, the variables are joined by language operations. Among the most common operations on two languages A and B are the set union A ∪ B, the set intersection A ∩ B, and the concatenation A⋅B. Finally, as an operation taking a single operand, the set A* denotes the Kleene star of the language A. Therefore language equations can be used to represent formal grammars, since the languages generated by the grammar must be the solution of a system of language equations.

In computer science, more particularly in automated theorem proving, rippling refers to a group of meta-level heuristics, developed primarily in the Mathematical Reasoning Group in the School of Informatics at the University of Edinburgh, and most commonly used to guide inductive proofs in automated theorem proving systems. Rippling may be viewed as a restricted form of rewrite system, where special object level annotations are used to ensure fertilization upon the completion of rewriting, with a measure decreasing requirement ensuring termination for any set of rewrite rules and expression.

In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. The halting problem is undecidable, meaning that no general algorithm exists that solves the halting problem for all possible program–input pairs.

Inductive programming (IP) is a special area of automatic programming, covering research from artificial intelligence and programming, which addresses learning of typically declarative and often recursive programs from incomplete specifications, such as input/output examples or constraints.

<span class="mw-page-title-main">Encompassment ordering</span>

In theoretical computer science, in particular in automated theorem proving and term rewriting, the containment, or encompassment, preorder (≤) on the set of terms, is defined by

<span class="mw-page-title-main">Rewrite order</span>

In theoretical computer science, in particular in automated reasoning about formal equations, reduction orderings are used to prevent endless loops. Rewrite orders, and, in turn, rewrite relations, are generalizations of this concept that have turned out to be useful in theoretical investigations.

In theoretical computer science, in particular in term rewriting, a path ordering is a well-founded strict total order (>) on the set of all terms such that

Nachum Dershowitz is an Israeli computer scientist, known e.g. for the Dershowitz–Manna ordering and the multiset path ordering used to prove termination of term rewrite systems.

Wayne Snyder is an associate professor at Boston University known for his work in E-unification theory.

Christoph Walther is a German computer scientist, known for his contributions to automated theorem proving. He is Professor emeritus at Darmstadt University of Technology.

Jean Henri Gallier is a researcher in computational logic at the University of Pennsylvania, where he holds appointments in the Computer and Information Science Department and the Department of Mathematics.

Deepak Kapur is a Distinguished Professor in the Department of Computer Science at the University of New Mexico.

References

  1. ↑ David A. Plaisted (1978). A Recursively Defined Ordering for Proving Termination of Term Rewriting Systems (Technical report). Univ. of Illinois, Dept. of Comp. Sc. p. 52. R-78-943.
  2. ↑ Bachmair, L.; Plaisted, D.A. (1985). Jean-Pierre Jouannaud (ed.). Associative Path Orderings. LNCS. Vol. 202. Springer-Verlag. pp. 241–54.
  3. ↑ David A. Plaisted (1981). "Theorem Proving with Abstraction". Artif. Intell. 16 (1): 47–108. doi:10.1016/0004-3702(81)90015-1.
  4. ↑ David A. Plaisted (1982). "A Simplified Problem Reduction Format". Artif. Intell. 18 (2): 227–61. doi:10.1016/0004-3702(82)90041-8.
  5. ↑ Xumin Nie; David A. Plaisted (Jan 1989). A Semantic Variant of the Modified Problem Reduction Format (PDF) (Technical report). Univ. of North Carolina at Chapel Hill. p. 11. TR89-101.
  6. ↑ Jean H. Gallier, Paliath Narendran, David A. Plaisted, Stan Raatz, Wayne Snyder (1993). "An Algorithm for Finding Canonical Sets of Ground Rewrite Rules in Polynomial Time" (PDF). J. ACM. 40 (1): 1–16. doi:10.1145/138027.138032. S2CID   820591.{{cite journal}}: CS1 maint: multiple names: authors list (link)
  7. ↑ David A. Plaisted; Steven Greenbaum (1986). "A Structure-preserving Clause Form Translation". J. Symbolic Comput. 2 (3): 293–304. doi: 10.1016/s0747-7171(86)80028-1 .
  8. ↑ Jean H. Gallier; Paliath Narendran; David A. Plaisted; Wayne Snyder (1990). "Rigid E-Unification: NP-Completeness and Applications to Equational Matings". Inf. Comput. 87 (1/2): 129–95. doi: 10.1016/0890-5401(90)90061-l .
  9. ↑ David A. Plaisted (1985). "Semantic Confluence Tests and Completion Methods". Information and Control. 65 (2/3): 182–215. doi: 10.1016/s0019-9958(85)80005-x .
  10. ↑ David A. Plaisted; Andrea Sattler-Klein (1996). "Proof Lengths for Equational Completion" (PDF). Inf. Comput. 125 (2): 154–70. doi:10.1006/inco.1996.0028.
  11. ↑ Shie-Jue Lee; David A. Plaisted (1994). "Use of replace rules in theorem proving". Methods of Logic in Computer Science. 1 (2): 217–40.
  12. ↑ Heng Chu; David A. Plaisted (1994). "Model Finding in Semantically Guided Instance-Based Theorem Proving". Fundam. Inform. 21 (3): 221–235. doi:10.3233/FI-1994-2134.
  13. ↑ Xumin Nie; David A. Plaisted (July 1990). "A Complete Semantic Back Chaining Proof System". In M. E. Stickel (ed.). Proc. 10th CADE. LNAI. Vol. 449. Springer. pp. 16–27.
  14. ↑ "More Bad News for Radiometric Dating". www.cs.unc.edu. Retrieved 2018-11-28.
  15. ↑ "A Creation Perspective". tasc-creationscience.org. Retrieved 2018-11-28.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.