Hola,
¿eres nuevo aquí?

Registrate y conecta tu empresa con financiación pública, partners y proyectos.

MTM2009-13842-C02-02

Financiado

GESTION MECANIZADA DEL CONOCIMIENTO MATEMATICO. APLICACIONES EN LOGICA

LA GESTION DEL CONOCIMIENTO MATEMATICO (MKM, SUS SIGLAS EN INGLES) ES UN NUEVO CAMPO DE INVESTIGACION EN LA INTERSECCION DE LAS MATEMATICAS Y LAS CIENCIAS DE LA COMPUTACION, EN ESTE AREA SE PRETENDE INTEGRAR TODOS LOS ASPECTOS DE... ver más

01/01/2009

5K€

Presupuesto del proyecto: 5K€

Líder del proyecto

UNIVERSIDAD DE SEVILLA No se ha especificado una descripción o un objeto social para esta compañía.

Total investigadores 3670

Ver Participantes

Financiación concedida El organismo AGENCIA ESTATAL DE INVESTIGACIÓN notifico la concesión del proyecto el día 2009-01-01

0% 100%

Participantes

Lider

Proyectos interesantes

MTM2009-13842-C02-01 GESTION MECANIZADA DEL CONOCIMIENTO MATEMATICO. APLICACIONES... 52K€ Cerrado

MeReMath Mechanised Reverse Mathematics in the Calculus of Inductive... 196K€ Cerrado

MTM2008-01139 LOGICA ALGEBRAICA Y LOGICAS NO CLASICAS 41K€ Cerrado

PID2019-110843GA-I00 LA GEOMETRIA DE LAS LOGICAS NO-CLASICAS 25K€ Cerrado

MTM2014-54151-P FORMALIZACION DE LAS MATEMATICAS: APLICACIONES EN CALCULO SI... 22K€ Cerrado

FFI2017-82878-P SEMANTICA RELACIONAL TERNARIA TIPO ROUTLEY-MEYER PARA NEGACI... 15K€ Cerrado

Últimas noticias

27-11-2024: Videojuegos y creaci... Se abre la línea de ayuda pública: Ayudas para la promoción del sector del videojuego, del pódcast y otras formas de creación digital

27-11-2024: DGIPYME En las últimas 48 horas el Organismo DGIPYME ha otorgado 1 concesiones

27-11-2024: FUNDACION-EOI En las últimas 48 horas el Organismo FUNDACION EOI ha otorgado 2 concesiones

Líder del proyecto

UNIVERSIDAD DE SEVILLA

Total investigadores 3670

Presupuesto del proyecto 5K€

Descripción del proyecto LA GESTION DEL CONOCIMIENTO MATEMATICO (MKM, SUS SIGLAS EN INGLES) ES UN NUEVO CAMPO DE INVESTIGACION EN LA INTERSECCION DE LAS MATEMATICAS Y LAS CIENCIAS DE LA COMPUTACION, EN ESTE AREA SE PRETENDE INTEGRAR TODOS LOS ASPECTOS DE LA MECANIZACION DE LAS MATEMATICAS COMO LA COMPUTACION, LA ORGANIZACION Y COMUNICACION DEL CONOCIMIENTO MATEMATICO Y LA DEDUCCION FORMAL Y AUTOMATIZADA DE DICHO CONOCIMIENTO, EN PARTICULAR, CUANDO LA DEDUCCION FORMAL SE REALIZA PARA CONCLUIR LAS PROPIEDADES DE CORRECCION DE UN DETERMINADO MODELO MATEMATICO DE UN SISTEMA (HARDWARE, SOFTWARE,,,,) , HABLAMOS DE VERIFICACION FORMAL DE SISTEMAS, ESTE SUBPROYECTO ABORDA LOS SIGUIENTES ASPECTOS RELATIVOS A LA GESTION MECANIZADA DEL CONOCIMIENTO MATEMATICO (MKM): VERIFICACION FORMAL DE MODELOS DE SISTEMAS (SISTEMAS DE COMPUTACION BASADOS EN REGLAS Y SISTEMAS DE CALCULO SIMBOLICO, EN CONCRETO), COMPUTACION USANDO ESOS SISTEMAS FORMALIZADOS Y FINALMENTE LA PRESENTACION DE DEMOSTRACIONES FORMALES (Y MECANIZADAS) SOBRE SISTEMAS LOGICOS, EN UN ESTILO CERCANO A LAS QUE SE PRESENTAN EN LOS TEXTOS MATEMATICOSEN PRIMER LUGAR, PRETENDEMOS ABORDAR LA VERIFICACION FORMAL DEL ALGORITMO RETE, USADO PARA IMPLEMENTAR SISTEMAS BASADOS EN REGLAS DE PRODUCCION, A PESAR DE SER UN ALGORITMO AMPLIAMENTE USADO COMO NUCLEO DE LA MAYORIA DE LOS GENERADORES DE SISTEMAS EXPERTOS (COMO CLIPS), NO EXISTE UNA FORMALIZACION CONOCIDA DE SU CORRECCION, ASI, PRETENDEMOS OBTENER EN PRIMER LUGAR UN MODELO FORMAL DEL ALGORITMO Y EN SEGUNDO LUGAR UNA ESPECIFICACION DE SU CORRECCION VERIFICADA FORMALMENTE, PARA ELLO USAREMOS EL DEMOSTRADOR AUTOMATICO ACL2, QUE ADEMAS NOS PERMITIRA REALIZAR COMPUTACIONES CON EL MODELO VERIFICADO,EN SEGUNDO LUGAR, Y COMO PARTE DEL PROYECTO COORDINADO CON LA UNIVERSIDAD DE LA RIOJA, PRETENDEMOS VERIFICAR FORMALMENTE ALGORITMOS QUE APARECEN EN LOS SISTEMAS DE CALCULO SIMBOLICO EN TOPOLOGIA ALGEBRAICA DESARROLLADOS POR EL GRUPO DE LA RIOJA,FINALMENTE, HAY QUE SEÑALAR QUE USUALMENTE, LAS DEMOSTRACIONES FORMALES OBTENIDAS POR UN DEMOSTRADOR AUTOMATICO ESTAN MAS ORIENTADAS A LA MAQUINA QUE AL HUMANO, NUESTRO TERCER OBJETIVO ES USAR DEMOSTRADORES DE TEOREMAS CON LA IDEA PRIMORDIAL DE DESARROLLAR DEMOSTRACIONESFORMALES (Y MECANIZADAS) QUE FUESEN "NATURALES" EN EL SENTIDO DE QUE SE PAREZCAN LO MAS POSIBLE A LAS QUE APARECEN EN LOS TEXTOS MATEMATICOS, CUMPLIENDO ASI UNO DE LOS OBJETIVOS DE MKM, EN PARTICULAR, ABORDAREMOS ESTE OBJETIVO PARA LA DEMOSTRACION DE RESULTADOS DE LOGICA MATEMATICA, Y USAREMOS PARA ELLO DEMOSTRADORES COMO ISABELLE/ISAR O PVS, GESTION DEL CONOCIMIENTO MATEMATICO\RAZONAMIENTO MECANIZADOL\LOGICA COMPUTACIONAL

Conecta tu I+D

Entra hoy

Financiación

Empresas

CTIs/Universidades

Proyectos

Investigadores