Diferencia entre revisiones de «Projects»

De WikiGLC
Saltar a: navegación, buscar
Línea 4: Línea 4:
 
# [[Verificación de sistemas SAT]]
 
# [[Verificación de sistemas SAT]]
 
# [[Verificación de traductores de problemas combinatorios en SAT]]
 
# [[Verificación de traductores de problemas combinatorios en SAT]]
−
 
−
=== APLI2++ (APLIcaciones de Ayuda Para Lógica Informática) ===
 
−
El objetivo del proyecto consiste en crear herramientas de ayuda para la enseñanza de la Lógica en Informática. Ya se ha desarrollado [http://www.glc.us.es/~jalonso/apli2 APLI2] (APLIcación de Ayuda Para Lógica Informática) que es una herramienta para ayudar en el aprendizaje de la representación del conocimiento en lógica de primer orden. APLI2 se usa en la enseñanza de las asignaturas de [http://www.cs.us.es/~jalonso/cursos/li/ Lógica informática] y [http://www.cs.us.es/cursos/ra/ Razonamiento automático]. Las ampliaciones previstas son:
 
−
* desarrollo de un editor de fórmulas integrado en APLI2; es decir, que se interactúe con el editor a través de la Red, que genere bases de conocimiento para APLI2 y que genera la traza de la edición para su estudio posterior.
 
−
* desarrollo de un editor de demostraciones integrado en APLI2; es decir, que se interactúe con el editor a través de la Red, que admita la base de conocimiento existente en APLI2 y que genera la traza del razonamiento para su estudio posterior.
 
−
* desarrollo de una aplicación que use técnicas de minería de datos a un conjunto de datos qenerado por la interacción con APLI2. El objetivo fundamental es la extracción de conocimiento sobre el proceso de aprendizaje de la lógica.
 
−
A más largo plazo se plantea ampliar las lógicas para incluir lógicas modales, descriptivas, temporales y de orden superior. Se contemplan dos vías, por reducción a primer orden o por integración de otros demostradores.
 
−
 
−
=== 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] y [http://www.cs.kuleuven.be/~dtai/projects/CHR/ CHR].
 
−
* 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].
 
−
* 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].
 
−
** 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 sistemas 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 traducié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 ==
−
* 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.
  
−
* 2003-06 Development and verification of Intelligent Systems with logic and algebraic technics. Evolution of information systems. Theory and interdisciplinary applications (en tramitación)
+
# 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.
+
#: Directed by Luis M. Laita de la Rica.
  
−
* 2000-03 Development and formal verification of reasoning systems (DGI TIC2000-1368-C03-02)
+
# 2000-03 Development and formal verification of reasoning systems (DGI TIC2000-1368-C03-02)
−
*: Directed by José A. Alonso Jiménez.
+
#: 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)
+
# 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.
+
#: Directed by Luis M. Laita de la Rica.
  
−
* 1997-00 Verification of knowledge bases and reasoning systems (DGES PB96-0098-C04-04)
+
# 1997-00 Verification of knowledge bases and reasoning systems (DGES PB96-0098-C04-04)
−
*: Directed by José A. Alonso Jiménez.
+
#: 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)
+
# 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.
+
#: 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)
+
# 1997-00 Classification of the computable functions by means of arithmetic specifications: methodology and design (DGES PB96-1345)
−
*: Directed by Alejandro Fernández Margarit.
+
#: Directed by Alejandro Fernández Margarit.
  
−
* 1995-96 Verification of expert systems: formal models and implementation (DGICYT PB 94-0424)
+
# 1995-96 Verification of expert systems: formal models and implementation (DGICYT PB 94-0424)
−
*: Directed by Luis M. Laita de la Rica.
+
#: Directed by Luis M. Laita de la Rica.
  
−
* 1992-93 Verification of knowledge bases in expert systems II (CICYT TIC 92-1191)
+
# 1992-93 Verification of knowledge bases in expert systems II (CICYT TIC 92-1191)
−
*: Directed by Luis M. Laita de la Rica.
+
#: Directed by Luis M. Laita de la Rica.
  
−
* 1992-93 A model for verification of expert systems (CICYT TIC 92-0069)
+
# 1992-93 A model for verification of expert systems (CICYT TIC 92-0069)
−
*: Directed by Luis M. Laita de la Rica.
+
#: Directed by Luis M. Laita de la Rica.
  
−
* 1990-91 Verification of knowledge bases in expert systems II (PRONTIC 90-2738)
+
# 1990-91 Verification of knowledge bases in expert systems II (PRONTIC 90-2738)
−
*: Directed by Luis M. Laita de la Rica.
+
#: Directed by Luis M. Laita de la Rica.

Revisión del 14:19 22 oct 2008

Proyectos futuros

  1. APLI2S (APLIcaciones de Ayuda Para Lógica Informática)
  2. Solución declarativa de problemas
  3. Verificación de sistemas SAT
  4. Verificación de traductores de problemas combinatorios en SAT

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.
  1. 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.
  1. 2000-03 Development and formal verification of reasoning systems (DGI TIC2000-1368-C03-02)
    Directed by José A. Alonso Jiménez.
  1. 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.
  1. 1997-00 Verification of knowledge bases and reasoning systems (DGES PB96-0098-C04-04)
    Directed by José A. Alonso Jiménez.
  1. 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.
  1. 1997-00 Classification of the computable functions by means of arithmetic specifications: methodology and design (DGES PB96-1345)
    Directed by Alejandro Fernández Margarit.
  1. 1995-96 Verification of expert systems: formal models and implementation (DGICYT PB 94-0424)
    Directed by Luis M. Laita de la Rica.
  1. 1992-93 Verification of knowledge bases in expert systems II (CICYT TIC 92-1191)
    Directed by Luis M. Laita de la Rica.
  1. 1992-93 A model for verification of expert systems (CICYT TIC 92-0069)
    Directed by Luis M. Laita de la Rica.
  1. 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=174»