Diferencia entre revisiones de «Projects»

De WikiGLC
Saltar a: navegación, buscar
Línea 1: Línea 1:
 +
== Proyectos futuros ==
 +
* 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.
 +
 +
* 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.
 +
 +
* 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: [http://www.swi-prolog.org/ SWI-Prolog] y [http://www.gprolog.org/ GNU Prolog],
 +
*:* Programación lógica con restricciones: [http://www.eclipse-clp.org/ ECLIPSe]
 +
*:* Programación basada en conjuntos de respuestas: [http://www.dbai.tuwien.ac.at/proj/dlv/ DLV], [http://www.tcs.hut.fi/Software/smodels/ Smodels], [http://www.cs.utexas.edu/users/tag/cmodels.html Cmodels].
 +
*:* Programación funcional:
 +
*:** con Haskell: [http://cvs.haskell.org/Hugs/index.html Hugs] y [http://haskell.org/ghc/index.html GHC],
 +
*:** con Lisp: [http://clisp.cons.org/ CLISP] y [http://www.gnu.org/software/gcl/ GCL].
 +
*:* Programación basada en reglas de producción: [http://clipsrules.sourceforge.net/ CLIPS] y [ http://herzberg.ca.sandia.gov/ Jess].
 +
 +
== Proyectos pasados ==
 
* 2004-08 Sistemas verificados para el razonamiento en la web semántica. (MEC TIN2004-038844).
 
* 2004-08 Sistemas verificados para el razonamiento en la web semántica. (MEC TIN2004-038844).
 
*:  Directed by José A. Alonso Jiménez.
 
*:  Directed by José A. Alonso Jiménez.

Revisión del 09:44 22 oct 2008

Proyectos futuros

  • 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.
  • 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.
  • 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:

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.