FORMALIZACION DE LAS MATEMATICAS: APLICACIONES EN CALCULO SIMBOLICO Y ALGEBRA CO...
FORMALIZACION DE LAS MATEMATICAS: APLICACIONES EN CALCULO SIMBOLICO Y ALGEBRA COMPUTACIONAL
LA FORMALIZACION DE LAS MATEMATICAS POR MEDIO DE ASISTENTES PARA EL RAZONAMIENTO MECANIZADO (COMO COQ, ISABELLE O ACL2) HA ALCANZADO UN GRADO DE MADUREZ QUE PERMITE ABORDAR PROBLEMAS REPUTADOS COMO DIFICILES, TANTO EN MATEMATICAS...
ver más
UNIVERSIDAD DE LA RIOJA
No se ha especificado una descripción o un objeto social para esta compañía.
Total investigadores311
Financiación
concedida
El organismo AGENCIA ESTATAL DE INVESTIGACIÓN notifico la concesión del proyecto
el día 2014-01-01
No tenemos la información de la convocatoria
0%
100%
Información adicional privada
No hay información privada compartida para este proyecto. Habla con el coordinador.
¿Tienes un proyecto y buscas un partner? Gracias a nuestro motor inteligente podemos recomendarte los mejores socios y ponerte en contacto con ellos. Te lo explicamos en este video
Proyectos interesantes
PID2020-116641GB-I00
METODOS HOMOLOGICOS EN ALGEBRA COMPUTACIONAL: GENERALIZACION...
33K€
Cerrado
MTM2017-88796-P
COMPUTACION SIMBOLICA: NUEVOS RETOS EN ALGEBRA Y GEOMETRIA Y...
74K€
Cerrado
PID2019-108991GB-I00
MATEMATICAS PARA EL DESARROLLO DE SISTEMAS INTELIGENTES
76K€
Cerrado
TIN2009-14562-C05-04
FEAST: FUNDAMENTOS Y EXTENSIONES DE LA TECNOLOGIA ANSWER SET...
141K€
Cerrado
LASD
Logic and Automata over Sequences with Data
2M€
Cerrado
Información proyecto MTM2014-54151-P
Líder del proyecto
UNIVERSIDAD DE LA RIOJA
No se ha especificado una descripción o un objeto social para esta compañía.
Total investigadores311
Presupuesto del proyecto
22K€
Descripción del proyecto
LA FORMALIZACION DE LAS MATEMATICAS POR MEDIO DE ASISTENTES PARA EL RAZONAMIENTO MECANIZADO (COMO COQ, ISABELLE O ACL2) HA ALCANZADO UN GRADO DE MADUREZ QUE PERMITE ABORDAR PROBLEMAS REPUTADOS COMO DIFICILES, TANTO EN MATEMATICAS COMO EN LA VERIFICACION DE SISTEMAS SOFTWARE, EN ESTE PROYECTO PROPONEMOS UTILIZAR ASISTENTES A LA DEMOSTRACION PARA FORMALIZAR TEOREMAS Y VERIFICAR LA CORRECCION DE PROGRAMAS PARA EL PROCESAMIENTO DE IMAGENES DIGITALES, LA RELEVANCIA DE ESTA CONTRIBUCION RESIDE EN NUESTRA COLABORACION CON ALGUNOS EQUIPOS DE BIOLOGOS QUE, EN PARTICULAR, INVESTIGAN EN FARMACOS CONTRA EL ALZHEIMER, NUESTROS PROGRAMAS EN USO PARA CIENTIFICOS EXPERIMENTALES REQUIEREN METODOS FORMALES DE LA INGENIERIA DEL SOFTWARE, PARA INCREMENTAR LA FIABILIDAD DE SUS RESULTADOS, LA ALGORITMICA SUBYACENTE A ESTOS PROGRAMAS PROVIENE DEL CALCULO SIMBOLICO (Y, MAS CONCRETAMENTE, DE LA TOPOLOGIA COMPUTACIONAL) Y DEL ALGEBRA COMPUTACIONAL (EN EL CAMPO DEL ALGEBRA HOMOLOGICA ALGORITMICA), FORMALIZACIÓN\VERIFICACIÓN DE SOFTWARE\DEMOSTRACIÓN MECANIZADA DE TEOREMAS\CÁLCULO SIMBÓLICO\TOPOLOGÍA COMPUTACIONAL