Diferencia entre revisiones de «Projects»
(→Proyectos futuros) |
(→Proyectos futuros) |
||
| Línea 1: | Línea 1: | ||
== Proyectos futuros == | == Proyectos futuros == | ||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
=== Solución declarativa de problemas === | === Solución declarativa de problemas === | ||
El objetivo es construir una colección de problemas y comparar sus soluciones usando distintos sistemas de programación declarativa: | El objetivo es construir una colección de problemas y comparar sus soluciones usando distintos sistemas de programación declarativa: | ||
| Línea 17: | Línea 11: | ||
* Programación basada en reglas de producción: [http://clipsrules.sourceforge.net/ CLIPS] y [http://herzberg.ca.sandia.gov/ Jess]. | * Programación basada en reglas de producción: [http://clipsrules.sourceforge.net/ CLIPS] y [http://herzberg.ca.sandia.gov/ Jess]. | ||
* Programación en sistemas de demostración: [http://www.cs.unm.edu/~mccune/otter/ Otter/Mace2], [http://www.cs.unm.edu/~mccune/prover9/ Prover9/Mace4], [http://www.cs.utexas.edu/users/moore/acl2/ ACL2], [http://pvs.csl.sri.com/ PVS] e [http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Isabelle]. | * Programación en sistemas de demostración: [http://www.cs.unm.edu/~mccune/otter/ Otter/Mace2], [http://www.cs.unm.edu/~mccune/prover9/ Prover9/Mace4], [http://www.cs.utexas.edu/users/moore/acl2/ ACL2], [http://pvs.csl.sri.com/ PVS] e [http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Isabelle]. | ||
| + | |||
| + | === Verificación de SAT === | ||
| + | El objetivo es construir en ACL2 un sistema SAT cuya eficiencia sea comparable a los más avanzados y formalmente verificado en ACL2. | ||
| + | |||
| + | === Verificación de traductores de problemas combinatorios en SAT === | ||
| + | Muchos problemas combinatorios se resuelven mejor taduciéndolos a lógica proposicional y usando sistemas SAT que con algoritmos específicos. El objetivo del proyecto es la verificación formal de los traductores algunos de dichos problemas. | ||
== Proyectos pasados == | == Proyectos pasados == | ||
Revisión del 10:03 22 oct 2008
Sumario
Proyectos futuros
Solución declarativa de problemas
El objetivo es construir una colección de problemas y comparar sus soluciones usando distintos sistemas de programación declarativa:
- Programación lógica: SWI-Prolog y GNU Prolog.
- Programación lógica con restricciones: ECLIPSe y CHR.
- Programación basada en conjuntos de respuestas: DLV, Smodels, Cmodels y clasp.
- Programación funcional:
- Programación basada en reglas de producción: CLIPS y Jess.
- Programación en sistemas de demostración: Otter/Mace2, Prover9/Mace4, ACL2, PVS e Isabelle.
Verificación de SAT
El objetivo es construir en ACL2 un sistema SAT cuya eficiencia sea comparable a los más avanzados y formalmente verificado en ACL2.
Verificación de traductores de problemas combinatorios en SAT
Muchos problemas combinatorios se resuelven mejor taduciéndolos a lógica proposicional y usando sistemas SAT que con algoritmos específicos. El objetivo del proyecto es la verificación formal de los traductores algunos de dichos problemas.
Proyectos pasados
- 2004-08 Sistemas verificados para el razonamiento en la web semántica. (MEC TIN2004-038844).
- Directed by José A. Alonso Jiménez.
- 2003-06 Development and verification of Intelligent Systems with logic and algebraic technics. Evolution of information systems. Theory and interdisciplinary applications (en tramitación)
- Directed by Luis M. Laita de la Rica.
- 2000-03 Development and formal verification of reasoning systems (DGI TIC2000-1368-C03-02)
- Directed by José A. Alonso Jiménez.
- 2000-03 Development and verification of Expert Systems with logic and algebraic technics. Theory and interdisciplinary applications (DGI TIC2000-1368-C03)
- Directed by Luis M. Laita de la Rica.
- 1997-00 Verification of knowledge bases and reasoning systems (DGES PB96-0098-C04-04)
- Directed by José A. Alonso Jiménez.
- 1997-00 Verification and automatic extraction of conclusions in knowledge and information systems. Theoretical foundations and implementation (DGES PB96-0098-C04)
- Directed by Luis M. Laita de la Rica.
- 1997-00 Classification of the computable functions by means of arithmetic specifications: methodology and design (DGES PB96-1345)
- Directed by Alejandro Fernández Margarit.
- 1995-96 Verification of expert systems: formal models and implementation (DGICYT PB 94-0424)
- Directed by Luis M. Laita de la Rica.
- 1992-93 Verification of knowledge bases in expert systems II (CICYT TIC 92-1191)
- Directed by Luis M. Laita de la Rica.
- 1992-93 A model for verification of expert systems (CICYT TIC 92-0069)
- Directed by Luis M. Laita de la Rica.
- 1990-91 Verification of knowledge bases in expert systems II (PRONTIC 90-2738)
- Directed by Luis M. Laita de la Rica.
