David Alan Plaisted es profesor de informática en la Universidad de Carolina del Norte en Chapel Hill .
Los intereses de investigación de Plaisted incluyen sistemas de reescritura de términos , demostración automatizada de teoremas , programación lógica y algoritmos . Sus logros de investigación en la demostración de teoremas incluyen trabajo en el ordenamiento de caminos recursivos, [1] el ordenamiento de caminos asociativos, [2] abstracción, [3] los formatos de reducción de problemas simplificados y modificados, [4] [5] reducibilidad de terreno, [6] traducciones de formularios de cláusulas no estándar, [7] unificación E rígida , [8] finalización Knuth-Bendix , [9] [10]reglas de reemplazo en la demostración de teoremas, [11] estrategias de demostración de teoremas basadas en instancias, [12] y semántica en la demostración de teoremas. [13]
Recibió su BS de la Universidad de Chicago en 1970 y su Ph.D. de la Universidad de Stanford en 1976. Se desempeñó en la facultad del departamento de informática de la Universidad de Illinois en Urbana-Champaign hasta 1984, y desde entonces ha sido profesor titular en el Departamento de Ciencias de la Computación de la Universidad de Carolina del Norte en Chapel. Cerro. Ha sido autor o coautor de publicaciones en informática, las cuales son citadas por académicos en este campo. Se ha desempeñado en varios comités de programas y en los consejos editoriales de varias revistas, incluido el Journal of Symbolic Computation , Information Processing Letters, Mathematical Systems Theory y Fundamenta Informaticae. Plaisted pasó un año sabático en SRI International en Menlo Park, California en 1982 y 1983 y otro en el Instituto Max Planck de Sistemas de Software y la Universidad de Kaiserslautern en Alemania en 1993 y 1994. [ cita requerida ] Plaisted opera un sitio web de creacionismo de la Tierra Joven llamado Una perspectiva de creación. [14] [15]
Referencias
- ^ David A. Plaisted (1978). Un pedido definido de forma recursiva para probar la terminación de los sistemas de reescritura de plazos (informe técnico). Univ. de Illinois, Departamento de Comp. Carolina del Sur. pag. 52. R-78-943.
- ^ Bachmair, L .; Plaisted, DA (1985). Jean-Pierre Jouannaud (ed.). Ordenaciones asociativas de caminos . LNCS. 202 . Springer-Verlag. págs. 241–54.
- ^ David A. Plaisted (1981). "Prueba de teorema con abstracción". Artif. Intell . 16 (1): 47–108. doi : 10.1016 / 0004-3702 (81) 90015-1 .
- ^ David A. Plaisted (1982). "Un formato simplificado de reducción de problemas". Artif. Intell . 18 (2): 227–61. doi : 10.1016 / 0004-3702 (82) 90041-8 .
- ^ Xumin Nie; David A. Plaisted (enero de 1989). Una variante semántica del formato de reducción de problemas modificado (PDF) (informe técnico). Univ. de Carolina del Norte en Chapel Hill. pag. 11. TR89-101.
- ^ Jean H. Gallier , Paliath Narendran, David A. Plaisted, Stan Raatz, Wayne Snyder (1993). "Un algoritmo para encontrar conjuntos canónicos de reglas de reescritura de tierra en tiempo polinomial" (PDF) . J. ACM . 40 (1): 1–16. doi : 10.1145 / 138027.138032 . S2CID 820591 .CS1 maint: varios nombres: lista de autores ( enlace )
- ^ David A. Plaisted; Steven Greenbaum (1986). "Una traducción del formulario de cláusula que preserva la estructura" . J. Computación simbólica . 2 (3): 293-304. doi : 10.1016 / s0747-7171 (86) 80028-1 .
- ^ Jean H. Gallier; Paliath Narendran; David A. Plaisted; Wayne Snyder (1990). "E-unificación rígida: NP-completitud y aplicaciones a los emparejamientos de ecuaciones" . Inf. Computación . 87 (1/2): 129–95. doi : 10.1016 / 0890-5401 (90) 90061-l .
- ^ David A. Plaisted (1985). "Pruebas de confluencia semántica y métodos de finalización" . Información y control . 65 (2/3): 182–215. doi : 10.1016 / s0019-9958 (85) 80005-x .
- ^ David A. Plaisted; Andrea Sattler-Klein (1996). "Longitudes de prueba para la realización de ecuaciones" (PDF) . Inf. Computación . 125 (2): 154–70. doi : 10.1006 / inco.1996.0028 .
- ^ Shie-Jue Lee; David A. Plaisted (1994). "Uso de reglas de reemplazo en la demostración de teoremas". Métodos de lógica en informática . 1 (2): 217–40.
- ^ Heng Chu; David A. Plaisted (1994). "Modelo de hallazgo en la demostración del teorema basado en instancia semánticamente guiada". Fundam. Informar . 21 (3): 221–235. doi : 10.3233 / FI-1994-2134 .
- ^ Xumin Nie; David A. Plaisted (julio de 1990). "Un completo sistema de prueba de encadenamiento posterior semántico". En ME Stickel (ed.). Proc. 10º CADE . LNAI. 449 . Saltador. págs. 16-27.
- ^ "Más malas noticias para las citas radiométricas" . www.cs.unc.edu . Consultado el 28 de noviembre de 2018 .
- ^ "Una perspectiva de la creación" . tasc-creationscience.org . Consultado el 28 de noviembre de 2018 .
enlaces externos
- Página de Plaisted en UNC
- David A. Plaisted en el servidor de bibliografía DBLP