Cristóbal Walther

Científico informático alemán (nacido en 1950)

Christoph Walther (nacido el 9 de agosto de 1950) ^[1] es un informático alemán, conocido por sus contribuciones a la demostración automatizada de teoremas . Es profesor emérito de la Universidad Tecnológica de Darmstadt . ^[2]

Publicaciones Seleccionadas

Sobre la demostración automatizada de teoremas

• Tomás Kolbe; Christoph Walther (1994). "Reutilización de pruebas". En Anthony Cohn (ed.). Proc. de la 11ª Conferencia Europea. sobre Inteligencia Artificial (ECAI-11) . John Wiley e hijos. págs. 80–84.
• Tomás Kolbe; Christoph Walther (1995). "Adaptación de Pruebas para su Reutilización". Proc. Simposio de otoño de AAAI de 1995 sobre adaptación del conocimiento para su reutilización . Prensa AAAI. págs. 61–67.
• Tomás Kolbe; Christoph Walther (1995). "Gestión y recuperación de pruebas". Proc. IJCAI-14 Taller sobre Enfoques Formales para la Reutilización de Planes, Pruebas y Programas . Morgan Kaufman. págs. 1 a 5.
• Tomás Kolbe; Christoph Walther (1995). "Evaluación del módulo de coincidencia de segundo orden: una técnica para reutilizar pruebas". Proc. 14º Interno. Conferencia conjunta. sobre Inteligencia Artificial (IJCAI-14) . Morgan Kaufman. págs. 190-195.
• Tomás Kolbe; Christoph Walther (1995). "Parchear pruebas para su reutilización". Proc. de la 8ª Conferencia Europea. sobre aprendizaje automático (ECML-8) . LNAI. vol. 912. Saltador. págs. 303–306.
• Tomás Kolbe; Christoph Walther (1996). "Terminación de la demostración de teoremas por reutilización". En MA McRobbie; JK Slaney (eds.). Proc. 13º Inter. Conf. sobre Deducción Automatizada (CADE-13) . LNAI. vol. 1104. Saltador. págs. 106-120.
• Tomás Kolbe; Christoph Walther (1996). "Demostración de teoremas imitando la habilidad de un ser humano". Simposio de primavera de AAAI 1996 sobre adquisición, aprendizaje y demostración . Prensa AAAI. págs. 50–56.
• Tomás Kolbe; Christoph Walther (1998). "Análisis de prueba, generalización y reutilización". En Wolfgang Bibel ; Peter Schmitt (eds.). Deducción automatizada: base para las solicitudes. vol. 9. Dordrecht: Editores académicos de Kluwer. págs. 189-219. doi :10.1007/978-94-017-0435-9_8.
• Christoph Walther; Tomás Kolbe (2000). "Sobre la terminación de las especulaciones sobre el lema". Información y Computación . 162 (1–2): 96–116. doi : 10.1006/inco.1999.2859 .
• Christoph Walther; Tomás Kolbe (2000). "Demostración de teoremas mediante reutilización". Inteligencia artificial . 116 (1–2): 17–66. doi :10.1016/S0004-3702(99)00096-X.
• Christoph Walther (2003). "Automatisches Beweisen". En Günther Görz (ed.). Einführung in die Künstliche Intelligenz . Addison-Wesley. págs. 223–263.

Sobre el análisis de terminación automatizado

• Christoph Walther (1988). "Algoritmos vinculados a argumentos como base para pruebas de terminación automatizadas". Proc. IX Jornadas de Deducción Automatizada . LNAI . vol. 310. Saltador. págs. 602–621.
• Christoph Walther (1991). "Automatización de Terminierungsbeweisen". En Wolfgang Bibel (ed.). Kunstliche Intelligenz . Vereg. págs. 1–254.
• Christoph Walther (1991). "Sobre la demostración de la terminación de algoritmos por máquina". Inteligencia artificial . 70 (1).
• Jürgen Giesl; Christoph Walther; Jürgen Brauburger (1998). "Análisis de terminaciones de programas funcionales". En Wolfgang Bibel ; Peter Schmitt (eds.). Deducción automatizada: base para las solicitudes. vol. 10. Dordrecht: Editores académicos de Kluwer. págs. 135-164. doi :10.1007/978-94-017-0437-3_6.
• Christoph Walther (2000). "Criterios de rescisión". En S. Hölldobler (ed.). Intelectética y Lógica Computacional. Dordrecht: Editores académicos de Kluwer. págs. 361–386.
• Christoph Walther; Stephan Schweitzer (2005). "Análisis de terminación automatizado para programas definidos de forma incompleta". En Franz Baader ; Andréi Voronkov (eds.). Proc. 11° Int. Conf. sobre Lógica para la Programación, Inteligencia Artificial y Razonamiento (LPAR) . LNAI. vol. 3452. Saltador. págs. 332–346.

Sobre el sistema de verificación VeriFun para programas funcionales

• Christoph Walther y Stephan Schweitzer (2003). "Acerca de VeriFun". En Franz Baader (ed.). Proc. XIX Jornadas de Deducción Automatizada . LNAI. vol. 2741. Saltador. págs. 322–327.
• Christoph Walther; Stephan Schweitzer (2004). "Verificación en el Aula". Revista de razonamiento automatizado . 31 (1): 35–73. doi :10.1016/0004-3702(85)90029-3.
• Christoph Walther; Stephan Schweitzer (2005). "Un generador de códigos verificado por máquina". En Moshe Y. Vardi ; Andréi Voronkov (eds.). Proc. 10° Int. Conf. de Lógica para la Programación, Inteligencia Artificial y Razonamiento (LPAR-10) . LNAI. vol. 2850. Saltador. págs. 91-106.
• Christoph Walther; Stephan Schweitzer (2005). "Razonamiento sobre programas incompletamente definidos". En Geoff Sutcliffe ; Andréi Voronkov (eds.). Proc. 12° Int. Conf. sobre Lógica para la Programación, Inteligencia Artificial y Razonamiento (LPAR-12) . LNAI. vol. 3835. Saltador. págs. 427–442.
• Markus Aderhold; Christoph Walther; Daniel Szallies; Andreas Schlosser (2006). "Una rápida refutación de VeriFun". En Wolfgang Ahrendt; Peter Baumgartner; Hans de Nivelle (eds.). Proc. Taller sobre No Teoremas, No Validez, No Demostrabilidad (DESPROVADOR-06) . págs. 59–69.
• Andrés Schlosser; Christoph Walther; Markus Aderhold (2006). "Especificaciones axiomáticas en VeriFun". En Serge Autexier; Heiko Mantel (eds.). Proc. 6to Taller de Verificación (VERIFY-06) . págs. 146-163.
• Andrés Schlosser; Christoph Walther; Michael Gonder; Markus Aderhold (2007). "Procedimientos dependientes del contexto y tipos calculados en VeriFun". Apuntes Electrónicos en Informática Teórica . 174 (7): 61–78. doi :10.1016/j.entcs.2006.10.038.
• Christoph Walther; Nathan Wasser (2017). "Fermat, Euler, Wilson: tres estudios de caso en teoría de números". Revista de razonamiento automatizado . 59 (2): 267–286. doi :10.1007/s10817-016-9387-z.
• Christoph Walther (2018). "Multiplicación de Montgomery formalmente verificada". En Hana Chockler; Georg Weissenbacher (eds.). Proc. del 30º Interno. Conf. sobre Verificación Asistida por Computadora (CAV 2018) . LNAI. vol. 10982. Saltador. págs. 505–522. doi :10.1007/978-3-319-96142-2_30.
• Christoph Walther (2019). "Iteración verificada de Newton-Raphson para potencias de módulo inversas multiplicativas de cualquier base". Transacciones ACM en software matemático (TOMS) . 45 (1): 9:1–9:7. doi :10.1145/3301317.

Sobre unificación, resolución y paramodulación variadas

• Christoph Walther (1983). "Un cálculo variado basado en resolución y paramodulación". En Alan Bundy (ed.). Proc. del 8vo Interno. Conferencia conjunta. sobre Inteligencia Artificial (IJCAI-8) . Morgan Kaufman. págs. 882–891.
• Christoph Walther (1984). "Una solución mecánica de la apisonadora de Schubert mediante resoluciones variadas". Proc. de la IV Conf. Nacional. sobre Inteligencia Artificial (AAAI-4) . Morgan Kaufman. págs. 330–334.
• Christoph Walther (1984). "Unificación en muchas teorías variadas". En Tim O'Shea (ed.). Proc. de la VI Conf. Europea. sobre Inteligencia Artificial (ECAI-6) . Holanda del Norte. págs. 383–392.
• Walther, Christoph (1985). "Una solución mecánica de la apisonadora de Schubert mediante resoluciones variadas". Artif. Intel . 26 (2): 217–224. doi :10.1016/0004-3702(85)90029-3.
• Christoph Walther (1986). "Una clasificación de problemas de unificación de muchos tipos". En Jörg Siekmann (ed.). Proc. del 8º Inter. Conf. sobre Deducción Automatizada (CADE-8) . LNAI. vol. 230. Saltador. págs. 525–537.
• Christoph Walther (1987). Un cálculo variado basado en resolución y paramodulación. Pitman (Londres) y Morgan Kaufmann (Los Altos). págs. 1–170.
• Christoph Walther (1988). "Unificación variada". J. ACM . 35 (1): 1–17. doi :10.1145/42267.45071.
• Christoph Walther (1990). "Inferencias variadas en la demostración automatizada de teoremas". En K.-H. Blasius; U. Hedtstück; C.-R. Rodillo (eds.). Clases y tipos de inteligencia artificial . LNAI. vol. 418. Saltador. págs. 18–48.
• Christoph Walther (2016). Un algoritmo para la unificación múltiple (Erratas para la unificación múltiple, J. ACM vol 35 (1), 1988) (Informe técnico). Universidad Técnica de Darmstadt.

En la prueba de inducción

• Susanne Biundo , Birgit Hummel, Dieter Hutter y Christoph Walther (1986). "El sistema de demostración del teorema de inducción de Karlsruhe". En JH Siekmann (ed.). Proc. 8º CADE . LNAI. vol. 230. Saltador. págs. 672–674.
• Christoph Walther (1992). "Inducción matemática". En SC Shapiro (ed.). Enciclopedia de Inteligencia Artificial . John Wiley e hijos. págs. 668–672.
• Christoph Walther (1992). "Cálculo de axiomas de inducción" (PDF) . En Andrei Voronkov (ed.). Proc. LPAR . LNAI. vol. 624. Saltador. págs. 381–392.
• Christoph Walther (1993). "Combinación de axiomas de inducción por máquina" (PDF) . En Ruzena Bajcsy (ed.). Proc. XIII IJCAI . Morgan Kaufman. págs. 95-101.
• Christoph Walther (1994). «Inducción Matemática» (PDF) . En Dov M. Gabbay y CJ Hogger y JA Robinson (ed.). Manual de Lógica en Inteligencia Artificial y Programación Lógica . vol. 2. Prensa de la Universidad de Oxford. págs. 127-227.
• Christoph Walther (2001). "Semántica y verificación de programación". Teubner Textos para la informática . vol. 34. Teubner-Wiley. págs. 1–212.

Referencias

1. Simon Siegler y Nathan Wasser, ed. (2010). "Prefacio". Verificación, inducción, análisis de terminación —- Festschrift para Christoph Walther con motivo de su 60 cumpleaños . LNAI . vol. 6463. Saltador. ISBN 978-3-642-17171-0.
2. Professuren und Gruppenleitungen Archivado el 21 de febrero de 2015 en Wayback Machine (Sección Emeriti und Professoren im Ruhestand ) en el sitio web de la Universidad de Darmstadt

enlaces externos

• Página de inicio de Christoph Walther en la Universidad de Darmstadt
• Sistema VeriFun en la Universidad de Darmstadt