David Plaisted

David Alan Plaisted es profesor de informática en la Universidad de Carolina del Norte en Chapel Hill .

Intereses de investigación

Los intereses de investigación de Plaisted incluyen sistemas de reescritura de términos , demostración automática de teoremas , programación lógica y algoritmos . Sus logros de investigación en demostración de teoremas incluyen trabajo sobre 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 fundamento, ^{[ 6 ]} traducciones de formas de cláusulas no estándar, ^{[ 7 ]} E-unificación rígida , ^{[ 8 ]} completitud de Knuth-Bendix , ^{[ 9 ]}^{[ 10 ]} reglas de reemplazo en demostración de teoremas, ^{[ 11 ]} estrategias de demostración de teoremas basadas en instancias, ^{[ 12 ]} y semántica en demostración de teoremas. ^{[ 13 ]}

Educación y carrera

Obtuvo su licenciatura en la Universidad de Chicago en 1970 y su doctorado en la Universidad de Stanford en 1976. Fue profesor en el departamento de informática de la Universidad de Illinois en Urbana-Champaign hasta 1984, y desde entonces es catedrático en el Departamento de Informática de la Universidad de Carolina del Norte en Chapel Hill. Es autor o coautor de publicaciones en informática, citadas por académicos del sector. Ha formado parte de varios comités de programas y de los consejos editoriales de diversas revistas, como Journal of Symbolic Computation , Information Processing Letters, Mathematical Systems Theory y Fundamenta Informaticae. Plaisted realizó estancias sabáticas en SRI International en Menlo Park, California, en 1982 y 1983, y otras en el Instituto Max Planck de Sistemas de Software y la Universidad de Kaiserslautern en Alemania en 1993 y 1994.

Referencias

↑ David A. Plaisted (1978). Un ordenamiento definido recursivamente para probar la terminación de sistemas de reescritura de términos (Informe técnico). Univ. de Illinois, Dept. de Ciencias de la Computación, pág. 52. R-78-943.
^ Bachmair, L.; Plaisted, DA (1985). Jean-Pierre Jouannaud (ed.). Ordenamientos de rutas asociativas . LNCS. vol. 202. Springer-Verlag. págs. 241 a 54.
↑ David A. Plaisted (1981). "Probabilidad de teoremas con abstracción". Artif. Intell . 16 (1): 47– 108. doi : 10.1016/0004-3702(81)90015-1 .
↑ David A. Plaisted (1982). "Un formato simplificado para la 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). Universidad de Carolina del Norte en Chapel Hill. pág. 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 básicas en tiempo polinomial" (PDF) . J. ACM . 40 (1): 1– 16. doi : 10.1145/138027.138032 . S2CID 820591 . {{cite journal}}: CS1 maint: varios nombres: lista de autores ( enlace )
↑ David A. Plaisted; Steven Greenbaum (1986). "Una traducción de forma de cláusula que preserva la estructura" . J. Symbolic Comput . 2 (3): 293– 304. doi : 10.1016/s0747-7171(86)80028-1 .
↑ Jean H. Gallier; Paliath Narendran; David A. Plaisted; Wayne Snyder (1990). "Unificación E rígida: NP-completitud y aplicaciones a emparejamientos ecuacionales" . Inf. Comput . 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 completación" . Information and Control . 65 (2/3): 182–215 . doi : 10.1016/s0019-9958(85)80005-x .
↑ 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 .
↑ Shie-Jue Lee; David A. Plaisted (1994). "Uso de reglas de reemplazo en la demostración de teoremas". Métodos de lógica en ciencias de la computación . 1 (2): 217– 40.
↑ 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 .
↑ Xumin Nie; David A. Plaisted (julio de 1990). "Un sistema completo de prueba de encadenamiento semántico hacia atrás". En ME Stickel (ed.). Actas del 10.º CADE . LNAI. Vol. 449. Springer. págs. 16–27 .

Enlaces externos

Página de Plaisted en UNC
David A. Plaisted en el servidor de bibliografía DBLP

[1] David A. Plaisted (1978). Un ordenamiento definido recursivamente para probar la terminación de sistemas de reescritura de términos (Informe técnico). Univ. de Illinois, Dept. de Ciencias de la Computación, pág. 52. R-78-943.

[2] Bachmair, L.; Plaisted, DA (1985). Jean-Pierre Jouannaud (ed.). Ordenamientos de rutas asociativas . LNCS. vol. 202. Springer-Verlag. págs. 241 a 54.

[3] David A. Plaisted (1981). "Probabilidad de teoremas con abstracción". Artif. Intell . 16 (1): 47– 108. doi : 10.1016/0004-3702(81)90015-1 .

[4] David A. Plaisted (1982). "Un formato simplificado para la reducción de problemas". Artif. Intell . 18 (2): 227– 61. doi : 10.1016/0004-3702(82)90041-8 .

[5] Xumin Nie; David A. Plaisted (enero de 1989). Una variante semántica del formato de reducción de problemas modificado (PDF) (Informe técnico). Universidad de Carolina del Norte en Chapel Hill. pág. 11. TR89-101.

[6] Jean H. Gallier , Paliath Narendran, David A. Plaisted, Stan Raatz, Wayne Snyder (1993). "Un algoritmo para encontrar conjuntos canónicos de reglas de reescritura básicas en tiempo polinomial" (PDF) . J. ACM . 40 (1): 1– 16. doi : 10.1145/138027.138032 . S2CID 820591 . {{cite journal}}: CS1 maint: varios nombres: lista de autores ( enlace )

[7] David A. Plaisted; Steven Greenbaum (1986). "Una traducción de forma de cláusula que preserva la estructura" . 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). "Unificación E rígida: NP-completitud y aplicaciones a emparejamientos ecuacionales" . Inf. Comput . 87 (1/2): 129–95 . doi : 10.1016/0890-5401(90)90061-l .

[9] David A. Plaisted (1985). "Pruebas de confluencia semántica y métodos de completación" . 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). "Uso de reglas de reemplazo en la demostración de teoremas". Métodos de lógica en ciencias de la computación . 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 (julio de 1990). "Un sistema completo de prueba de encadenamiento semántico hacia atrás". En ME Stickel (ed.). Actas del 10.º CADE . LNAI. Vol. 449. Springer. págs. 16–27 .

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]

[ 13 ]