Diferencia entre revisiones de «Projects»

De WikiGLC
Saltar a: navegación, buscar
(→‎Proyectos futuros)
 
(No se muestran 27 ediciones intermedias de 6 usuarios)
Línea 1: Línea 1:
 
== Proyectos futuros ==
 
== Proyectos futuros ==
−
=== Solución declarativa de problemas ===
+
# [[Razonamiento formalizado]]
−
El objetivo es construir una colección de problemas y comparar sus soluciones usando distintos sistemas de programación declarativa:
+
# [[APLI2S (APLIcaciones de Ayuda Para Lógica Informática)]]
−
* Programación lógica: [http://www.swi-prolog.org/ SWI-Prolog] y [http://www.gprolog.org/ GNU Prolog].
+
# [[Solución declarativa de problemas]]
−
* Programación lógica con restricciones: [http://www.eclipse-clp.org/ ECLIPSe] y [http://www.cs.kuleuven.be/~dtai/projects/CHR/ CHR].
+
# [[Programas sencillos para problemas complejos]]
−
* 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] y [http://www.cs.uni-potsdam.de/clasp/ clasp].
+
# [[Verificación de sistemas SAT]]
−
* Programación funcional:
+
# [[Verificación de traductores de problemas combinatorios en SAT]]
−
** con Haskell: [http://cvs.haskell.org/Hugs/index.html Hugs] y [http://haskell.org/ghc/index.html GHC].
+
# [[Proyectos relacionados]]
−
** con Lisp: [http://clisp.cons.org/ CLISP] y [http://www.gnu.org/software/gcl/ GCL].
 
−
** con Scheme: [http://plt-scheme.org/ PLT Scheme] (incluye [http://www.drscheme.org/ DrScheme].
 
−
* 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].
 
  
−
=== Verificación de SAT ===
+
== Proyectos en ejecución ==
−
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 ===
+
# 2009-2010  [[Gestión Mecanizada del conocimiento matemático]]. (MTM2009-13842-C02-02, subprograma MTM)
−
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.
+
#: Investigador principal: José Luis Ruiz Reina
 +
# 2009-2012 [[Marco Lógico-computacional para la evolución de teorías sobre conceptos formales (TIN2009-09492, subprograma TIN)]]
 +
#: Investigador principal: Joaquín Borrego Díaz
 +
# 2008-2009 [[Weteve (Proyecto Minerva plataforma de servicios en movilidad 2C-040)]]
 +
#: Director: Joaquín Borrego Díaz
  
 
== Proyectos pasados ==
 
== 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.
 +
# 2008 [[Realización del Estudio del Arte para el Proyecto EVAPREX]]. (FIDETIA P029-08/E19).
 +
#: Directed by {{fmartin}}.
 +
# 2007-08 [[Investigación de los Factores Críticos de los Procesos de Fabricación Básicos del Sector Aeronáutico Andaluz, SENSOR-IA]]. (FIDETIA P044-07/E19).
 +
#: Directed by {{fmartin}}.
 +
# 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.
  
−
* 2003-06 Development and verification of Intelligent Systems with logic and algebraic technics. Evolution of information systems. Theory and interdisciplinary applications (en tramitación)
+
[[Category:Projects]]
−
*: 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.
 

Revisión actual del 11:56 18 oct 2013

Proyectos futuros

  1. Razonamiento formalizado
  2. APLI2S (APLIcaciones de Ayuda Para Lógica Informática)
  3. Solución declarativa de problemas
  4. Programas sencillos para problemas complejos
  5. Verificación de sistemas SAT
  6. Verificación de traductores de problemas combinatorios en SAT
  7. Proyectos relacionados

Proyectos en ejecución

  1. 2009-2010 Gestión Mecanizada del conocimiento matemático. (MTM2009-13842-C02-02, subprograma MTM)
    Investigador principal: José Luis Ruiz Reina
  2. 2009-2012 Marco Lógico-computacional para la evolución de teorías sobre conceptos formales (TIN2009-09492, subprograma TIN)
    Investigador principal: Joaquín Borrego Díaz
  3. 2008-2009 Weteve (Proyecto Minerva plataforma de servicios en movilidad 2C-040)
    Director: Joaquín Borrego Díaz

Proyectos pasados

  1. 2004-08 Sistemas verificados para el razonamiento en la web semántica. (MEC TIN2004-038844).
    Directed by José A. Alonso Jiménez.
  2. 2008 Realización del Estudio del Arte para el Proyecto EVAPREX. (FIDETIA P029-08/E19).
    Directed by Francisco J. Martín.
  3. 2007-08 Investigación de los Factores Críticos de los Procesos de Fabricación Básicos del Sector Aeronáutico Andaluz, SENSOR-IA. (FIDETIA P044-07/E19).
    Directed by Francisco J. Martín.
  4. 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.
  5. 2000-03 Development and formal verification of reasoning systems (DGI TIC2000-1368-C03-02)
    Directed by José A. Alonso Jiménez.
  6. 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.
  7. 1997-00 Verification of knowledge bases and reasoning systems (DGES PB96-0098-C04-04)
    Directed by José A. Alonso Jiménez.
  8. 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.
  9. 1997-00 Classification of the computable functions by means of arithmetic specifications: methodology and design (DGES PB96-1345)
    Directed by Alejandro Fernández Margarit.
  10. 1995-96 Verification of expert systems: formal models and implementation (DGICYT PB 94-0424)
    Directed by Luis M. Laita de la Rica.
  11. 1992-93 Verification of knowledge bases in expert systems II (CICYT TIC 92-1191)
    Directed by Luis M. Laita de la Rica.
  12. 1992-93 A model for verification of expert systems (CICYT TIC 92-0069)
    Directed by Luis M. Laita de la Rica.
  13. 1990-91 Verification of knowledge bases in expert systems II (PRONTIC 90-2738)
    Directed by Luis M. Laita de la Rica.
Obtenido de «https://www.glc.us.es/web/index.php?title=Projects&oldid=1213»