Presentación
El Diccionario de Oxford define la Inteligencia Artificial (IA) como la teoría y el desarrollo de sistemas informáticos capaces de realizar tareas que normalmente requieren de la inteligencia humana, como la percepción visual, el reconocimiento del habla, la toma de decisiones y la traducción entre idiomas.
La IA ha despertado un amplio interés en los sectores público y privado, debido a los diversos desarrollos tecnológicos e impactos que ha tenido y tiene en la sociedad. Además, tiene gran auge desde el punto de vista científico por todas las disciplinas, áreas y técnicas que se aplican.
Objetivo
El Coloquio Nacional en Inteligencia Artificial busca conjuntar a especialistas en las áreas que componen a la IA para que brinden conferencias sobre temas de su especialidad. Los invitados son contactados por el comité organizador. Las pláticas están programadas por 50 minutos y están dirigidas principalmente a investigadores y estudiantes de posgrado.
Este Coloquio se transmite una vez por mes, generalmente los miércoles a las 12:00 hrs. por las ligas de YouTube de las instituciones organizadoras.
Siguiente sesión
27 de enero de 2021
Logica Clasica de Orden Superior: Automatizacion y APlicaciones Seleccionadas
Reseña:
Demostración automática de teoremas (ATP) y demostración interactiva de teoremas (ITP) en La lógica de orden superior (HOL) ha logrado un progreso significativo en las últimas décadas.
Hoy en día hay disponibles potentes sistemas HOL-ATP que pueden resolver problemas no triviales automáticamente. Además, los sistemas ATP para La lógica proposicional y de primer orden se han integrado con éxito con sistemas ITP modernos como Isabelle, HOL-light, Coq, Lean y otros, y Estas integraciones son clave para futuras aplicaciones más allá de lo académico. contexto. Junto con colegas y estudiantes a los que he estado contribuyendo esta área de desafío durante más de 25 años. El resultado de la investigación incluye, entre otros, la familia Leo de sistemas ATP para HOL, el desarrollo de un infraestructura HOL-ATP internacional asociada (TPTP THF), y trabajo fundamental sobre la semántica y la teoría de la prueba de HOL. En el primero parte de mi presentación describiré estas contribuciones a la automatización de HOL.
Participante:
Dr. Christoph Benzmüller,
Científico en Inteligencia Artificial, Ciencias de la Computación y Matemáticas en Freia Universität Berlin
Moderador:
Dr. Raúl Rojas - Universidad Libre de Berlín
Fecha:
Miércoles 27 de Enero - 12:00 horas (Centro de México)
programa
