Dr. Gilberto Pérez Vega  

Titular de universidad (TIT-UN)

Departamento Ciencias de la Computación y Tecnologías de la Información
Área Álgebra
Investigación  Grupo de investigación Information Retrieval Lab
Líneas de investigación - Métodos formales (verificación, certificación y formalización), aplicados a sistemas de control de software, algoritmos genéticos, protocolos y semántica denotacional. - Lógica de Equilibrio (una caracterización de Answer Set programming para programación lógica) con la inclusión de operadores modales temporales: Temporal Equilibrium Logic, que permite formalismos más expresivos para el razonamiento no monótono.
Palabras clave Verificación Formal, Métodos Formales, Teoría de Prueba, Lógica Intucionista, Answer Set Programming (ASP).
Contacto Directorio de la UDC
Orcid id0000-0001-6269-6101 Scopus55418023500

Docencia

Docencia impartida

En este apartado se muestra la docencia impartida en grados, másteres y resto de estudios oficiales en los últimos 6 años.

Asignatura y estudios en la que se imparte Horas a distancia Horas totales
Álgebra 0 30
Álgebra 0 22
Algoritmos 0 12
Lógica 0 5
Matemática Discreta 0 98
Matemática Discreta 0 20
Matemática Discreta 0 5
Trabajo Fin de Grado. Mención en Tecnologías de la Información
Grado en Ingeniería Informática. Curso Puente
0 3
Validación y Verificación del Software
Grado en Ingeniería Informática. Curso Puente (Obligatorio)
0 32
Asignatura y estudios en la que se imparte Horas a distancia Horas totales
Álgebra
Grado en Ingeniería Informática
0 48
Algoritmos
Grado en Ingeniería Informática
0 8
Lógica
Grado en Inteligencia Artificial
0 5
Matemática Discreta
Grado en Ingeniería Informática
0 90
Matemática Discreta
Grado en Ciencia e Ingeniería de Datos
0 30
Validación y Verificación del Software
Grado en Ingeniería Informática
Grado en Ingeniería Informática. Curso Puente (Obligatorio)
0 42
Asignatura y estudios en la que se imparte Horas a distancia Horas totales
Álgebra
Grado en Ingeniería Informática
0 46
Algoritmos
Grado en Ingeniería Informática
0 10
Matemática Discreta
Grado en Ingeniería Informática
0 93
Matemática Discreta
Grado en Ciencia e Ingeniería de Datos
0 30
Validación y Verificación del Software
Grado en Ingeniería Informática
Grado en Ingeniería Informática. Curso Puente (Obligatorio)
0 42
Asignatura y estudios en la que se imparte Horas a distancia Horas totales
Álgebra
Grado en Ingeniería Informática
0 40
Algoritmos
Grado en Ingeniería Informática
0 12
Matemática Discreta
Grado en Ingeniería Informática
0 89
Matemática Discreta
Grado en Ciencia e Ingeniería de Datos
0 30
Validación y Verificación del Software
Grado en Ingeniería Informática
Grado en Ingeniería Informática. Curso Puente (Obligatorio)
0 35
Asignatura y estudios en la que se imparte Horas a distancia Horas totales
Álgebra
Grado en Ingeniería Informática
0 34
Algoritmos
Grado en Ingeniería Informática
0 11
Matemática Discreta
Grado en Ingeniería Informática
0 80
Matemática Discreta
Grado en Ciencia e Ingeniería de Datos
0 60
Trabajo Fin de Grado. Mención en Ingeniería del Software
Grado en Ingeniería Informática
Grado en Ingeniería Informática. Curso Puente
0 4
Validación y Verificación del Software
Grado en Ingeniería Informática
Grado en Ingeniería Informática. Curso Puente (Obligatorio)
0 35
Asignatura y estudios en la que se imparte Horas a distancia Horas totales
Álgebra
Grado en Ingeniería Informática
0 89
Algoritmos
Grado en Ingeniería Informática
0 12
Matemática Discreta
Grado en Ingeniería Informática
0 120
Trabajo Fin de Grado. Mención en Computación
Grado en Ingeniería Informática
0 4
Validación y Verificación del Software
Grado en Ingeniería Informática
Grado en Ingeniería Informática. Curso Puente (Obligatorio)
0 35

Tutorías definidas por el/la docente para el curso académico 2023/2024.

Facultad de Informática

Cuatrimestre Día Lugar
Segundo cuatrimestre lunes
12:30 a 14:30
Despacho 4.1
Segundo cuatrimestre lunes
08:30 a 10:30
Despacho 4.1

Resultados de investigación

Puede consultar los méritos de investigación seleccionando un tipo de mérito y el año.

AXUDAS PARA A CONSOLIDACIÓN E ESTRUTURACIÓN DE UNIDADES DE INVESTIGACIÓN COMPETITIVAS.GPC 2022

Entidad financiadora Consellería de Educación
Investigadores principales Álvaro Barreiro García
Tipo Proyecto Programas Autonomicos
Fechas Desde 01/01/2022 a 20/11/2024

Razonamiento Automático y Aprendizaje con Inducción de Conocimiento

Entidad financiadora Ministerio de Ciencia e Innovación
Investigadores principales Pedro Cabalar Fernández/ José Santos Reyes
Tipo Proyecto Programas Nacionales
Fechas Desde 01/09/2021 a 31/08/2024

AXUDAS PARA A CONSOLIDACIÓN E ESTRUTURACIÓN DE UNIDADES DE INVESTIGACIÓN COMPETITIVAS. GPC

Entidad financiadora CONSELLERIA DE EDUCACIÓN, UNIVERSIDADE E FORMACIÓN PROFESIONAL
Investigadores principales ÁLVARO BARREIRO GARCÍA
Tipo Proyecto Programas Autonomicos
Fechas Desde 01/01/2019 a 20/11/2021

RAZONAMIENTO AUTOMATICO TEMPORAL PARA SISTEMAS INTELIGENTES DINAMICOS (TARDIS)

Entidad financiadora Ministerio de Economía y Competitividad (MINECO)
Investigadores principales Pedro Cabalar Fernández
Tipo Proyecto Programas Nacionales
Fechas Desde 01/01/2018 a 31/12/2020

Red de investigación IEMath-Galicia

Entidad financiadora Xunta de Galicia
Investigadores principales Juan José Nieto Roig
Tipo Proyecto Programas Autonomicos
Fechas Desde 01/01/2017 a 31/12/2018

Axudas para a acreditación, estruturación e mellora de centros de investigación singulares e agrupacións estratéxicas consolidadas do Sistema universitario de Galicia, cofinanciadas polo Fondo Europeo de Desenvolvemento Rexional (Feder), no marco do programa operativo Feder Galicia 2014-2020

Entidad financiadora Consellería de Cultura, Educación e Ordenación Universitaria
Investigadores principales Manuel F. González Penedo
Tipo Proyecto Programas Autonomicos
Fechas Desde 01/01/2016 a 30/11/2019

Ayudas para la consolidación y estructuración de unidades de investigación competitivas. Modalidad de Redes: "Rede de Procesamento da Linguaxe e Recuperación da Información (REDPLIR)"

Entidad financiadora Consellería de Cultura, Educación e Ordenación Universitaria
Investigadores principales Manuel Vilares Ferro
Tipo Proyecto Programas Autonomicos
Fechas Desde 01/01/2014 a 31/12/2015

Red de Investigación IEMath-Galicia

Entidad financiadora Consellería de Cultura, Educación e Ordenación Universitaria
Investigadores principales Juan José Nieto Roig
Tipo Proyecto Programas Autonomicos
Fechas Desde 01/01/2014 a 31/12/2015

MERLOT: RAZONAMIENTO MÉDICO CON HERRAMIENTAS LÓGICAS

Entidad financiadora Ministerio de Economía y Competitividad (MINECO)
Investigadores principales José Pedro Cabalar Fernández
Tipo Proyecto Programas Nacionales
Fechas Desde 01/01/2014 a 31/12/2016

Feast: Fundamentos y extensiones de la tecnología answer set programming. Expediente económico: PIA12009-43.-

Entidad financiadora Ministerio de Economía y Competitividad
Investigadores principales José Pedro Cabalar Fernández
Tipo Proyecto Otros Programas
Fechas Desde 01/01/2010 a 31/12/2013

Algoritmos xenéticos en problemas de satisfactibilidade: estudo formal e aplicación a answer set programming.

Entidad financiadora Dirección Xeral de Investigación, Desenvolvemento e Innovación
Tipo Proyecto Otros Programas
Fechas Desde 01/01/2008 a 31/10/2011

Lógicas, deducción y programación para sistemas inteligentes (ampliaciones y aplicaciones de Answer Set Programming)

Tipo Proyecto Otros Programas
Fechas Desde 01/10/2006 a 30/09/2009

LÓGICAS, DEDUCCIÓN Y PROGRAMACIÓN PARA SISTEMAS INTELIGENTES (AMPLIACIONES Y APLICACIONES DE ANSWER SET PROGRAMMING)

Tipo Proyecto Otros Programas
Fechas Desde 01/10/2006 a 30/09/2009

Verificación, rendimiento y disponibilidad de aplicaciones distribuidas en un entorno real (VRDADER)

Entidad financiadora Ministerio de Ciencia y Tecnología
Investigadores principales Víctor M. Gulías Fernández
Tipo Proyecto Programas Nacionales
Fechas Desde 05/11/2002 a 05/11/2005

Construyendo ciudad, habitando entre redes, formulando proyectos de vida: un modelo de simulación basado en una aplicación informática vía web

Entidad financiadora Secretaria Xeral de Investigación e Desenvolvemento Tecnolóxico
Investigadores principales José María Cardesín Díaz
Tipo Proyecto Programas Autonomicos
Fechas Desde 08/10/2002 a 08/10/2005

Representación de coalgebras y categorías derivadas

Entidad financiadora Secretaria Xeral de Investigación e Desenvolvemento Tecnolóxico
Tipo Proyecto Otros Programas
Fechas Desde 25/08/2000 a 25/08/2002

Sócrates (Sistema objetual y cooperativo para la racionalización de la actividad y la tecnología de la empresa )

Entidad financiadora Dirección Xeral de Universidades
Tipo Proyecto Otros Programas
Fechas Desde 24/10/1996 a 24/10/1998

Sistema de cálculo simbólico con arquitectura cliente/servidor y núcleo funcional

Entidad financiadora Dirección Xeral de Universidades
Investigadores principales José Luis Freire Nistal
Tipo Proyecto Otros Programas
Fechas Desde 01/01/1994 a 31/12/1995

Generación óptima de conexiones en mapas: aplicación en redes de distribución.

Entidad financiadora Consellería de Educación e Ordenación Universitaria
Investigadores principales Antonio Ángel Blanco Ferro
Tipo Proyecto Programas Autonomicos
Fechas Desde 07/04/1994 a 07/04/1997

Verification for ASP denotational semantics: A case study using the PVS theorem prover

Autores Felicidad Aguado, Pablo Fernández Ascariz, Pedro Cabalar, Gilberto Pérez, Concepción Vidal
Revista LOGIC JOURNAL OF THE IGPL Vol. 25 Núm. 2 (págs. 195 a 213)
DOI https://doi.org/10.1093/jigpal/jzw060

Temporal logic programs with variables

Autores Felicidad Aguado, Pedro Cabalar, Martín Diéguez Lodeiro, Gilberto Pérez, Concepción Vidal
Revista THEORY AND PRACTICE OF LOGIC PROGRAMMING Vol. 17 Núm. 2 (págs. 226 a 243)
DOI https://doi.org/10.1017/s1471068416000570

Temporal Equilibrium Logic with past operators

Autores Felicidad Aguado, Pedro Cabalar, Martín Diéguez Lodeiro, Gilberto Pérez, Concepción Vidal
Revista Journal of Applied Non-Classical Logics Vol. 27 Núm. 3-4 (págs. 161 a 177)
DOI https://doi.org/10.1080/11663081.2018.1427987

A denotational semantics for equilibrium logic

Autores Felicidad Aguado, Pedro Cabalar, Gilberto Pérez, Concepción Vidal, David Pearce
Revista THEORY AND PRACTICE OF LOGIC PROGRAMMING Vol. 15 Núm. 4-5 (págs. 620 a 634)
DOI https://doi.org/10.1017/s1471068415000277

Temporal Equilibrium Logic: a survey

Autores Felicidad Aguado, Pedro Cabalar, Gilberto Pérez, Concepción Vidal, Martín Diéguez Lodeiro
Revista Journal of Applied Non-Classical Logics Vol. 23 Núm. 1-2 (págs. 2 a 24)
DOI https://doi.org/10.1080/11663081.2013.798985

Integrating Temporal Extensions of Answer Set Programming

Autores Felicidad Aguado, Gilberto Pérez, Concepción Vidal
Revista LECTURE NOTES IN COMPUTER SCIENCE Vol. 8148 (págs. 23 a 35)
DOI https://doi.org/10.1007/978-3-642-40564-8_3

Crossover operators for permutations equivalence between position and order-based crossover

Autores Concepción Vidal, Gilberto Pérez, Felicidad Aguado, Lin, J
Revista LOGIC JOURNAL OF THE IGPL Vol. 19 Núm. 2 (págs. 405 a 414)

Loop Formulas for Splitable Temporal Logic Programs

Autores Felicidad Aguado, Pedro Cabalar, Gilberto Pérez, Concepción Vidal
Revista LECTURE NOTES IN COMPUTER SCIENCE Vol. 6645 (págs. 80 a 92)
DOI https://doi.org/10.1007/978-3-642-20895-9_9

Strongly equivalent temporal logic programs

Autores Felicidad Aguado, Pedro Cabalar, Gilberto Pérez, Concepción Vidal
Revista LECTURE NOTES IN COMPUTER SCIENCE Vol. 5293 (págs. 8 a 20)

Genetic algorithms in Coq: Generalization and formalization of the crossover operator

Autores Felicidad Aguado, José Luis Doncel Juárez, Lin, J, Gilberto Pérez, Concepción Vidal
Revista Journal of Formalized Reasoning (págs. 25 a 37)

Certified Genetic Algorithms: Crossover Operators for Permutations

Autores Felicidad Aguado, José Luis Doncel Juárez, Lin, J, Gilberto Pérez, Concepción Vidal, Ana Maria Vieites Rodriguez
Revista LECTURE NOTES IN COMPUTER SCIENCE Vol. 4739 (págs. 282 a 289)

Minimal Logic Programs

Autores Pedro Cabalar, Gilberto Pérez
Revista LECTURE NOTES IN COMPUTER SCIENCE Vol. 4670 (págs. 104 a 118)

Temporal Equilibrium Logic: a first approach

Autores Pedro Cabalar, Gilberto Pérez
Revista LECTURE NOTES IN COMPUTER SCIENCE Vol. 4739 (págs. 241 a 248)

TEORIA DE GRAFOS: EJERCICIOS RESUELTOS Y PROPUESTOS. LABORATORIO CON SAGE

Autores Concepción Vidal, Ana Maria Vieites Rodriguez, Felicidad Aguado, Gilberto Pérez, Manuel Ladra González, Felipe Gago Couso
Editorial Ediciones Paraninfo S.A, Madrid (España)
ISBN 978-84-283-3707-6

Forgetting Auxiliary Atoms in Forks
10th Workshop on Answer Set Programming and Other Computing Paradigms, co-located with the 14th International Conference on Logic Programming and Nonmonotonic Reasoning, ASPOCP@LPNMR 2017
Internacional

Autores Felicidad Aguado, Pedro Cabalar, Jorge Fandinno, David Pearce, Gilberto Pérez, Concepción Vidal
Lugar Espoo (Finlandia)

Equilibrium Graphs
9th Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2016), workshop of ICLP 2016
Internacional

Autores Pedro Cabalar, Carlos Pérez Ramil, Gilberto Pérez
Lugar New York (Estados Unidos)

A denotational semantics for equilibrium logic
International Conference of Logic Programming ICLP 2015
Internacional

Autores Felicidad Aguado, Pedro Cabalar, David Pearce, Gilberto Pérez, Concepción Vidal
Organizador Association for Logic Programming
Lugar Cork (Irlanda)

Loop formulas for splitable temporal logic programs
12th International Conference on Logic Programming and Nonmonotonic Reasoning LPNMR13
Internacional

Autores Felicidad Aguado, Pedro Cabalar, Gilberto Pérez, Concepción Vidal
Lugar Coruña, A (España)

Integrating Temporal Extensions of Answer Set Programming
12th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'13)
Internacional

Autores Concepción Vidal, Felicidad Aguado, Gilberto Pérez
Lugar Coruña, A (España)

Paving the way for temporal grounding
28th International Conference on Logic Programming ICLP 2012
Internacional

Autores Felicidad Aguado, Pedro Cabalar, Martín Diéguez Lodeiro, Gilberto Pérez, Concepción Vidal
Organizador International Conference on Logic Programming ICLP
Lugar Budapest (Hungría)

Fórmulas de ciclo para programas lógicos temporales: una primera aproximación
RSME 11
Nacional

Autores Gilberto Pérez, Felicidad Aguado, Concepción Vidal
Organizador Real Sociedad Matemática Española
Lugar Ávila (España)

Crossover Operators for Permutations. Equivalence between Position and Order Based Crossover
9th International Conference Computational and Mathematical Methods in Science and Engineering (CMMSE 2009)
Internacional

Autores Felicidad Aguado, Lin, J, Gilberto Pérez, Concepción Vidal
Lugar Gijón (España)

Generalización de los cruces basados en el orden y en la posición. Una implementación verificada
CLEI 2007, XXXIII Conferencia Latinoamericana de Informática
Internacional

Autores Felicidad Aguado, Lin, J, Gilberto Pérez, Concepción Vidal, Ana Maria Vieites Rodriguez
Lugar San José (Costa Rica)

Extracción de programas a partir de pruebas : Certificación de la Forma Normal de la Reducción de Polinomios
CLEI 2005. XXXI Conferencia Latinoamericana de Informática
Internacional

Autores Gilberto Pérez, José Luis Freire Nistal, Lin, J
Lugar Cali (Colombia)

Formalización de las Bases de Gröbner en Coq
Primer Congreso Conjunto de Matemáticas RSME - SCM - SEIO - SEMA. MAT.ES
Nacional

Autores Gilberto Pérez
Lugar Valencia (España)

Lógica, matemática, deducción automática
Primer Congreso Anual de la Real Sociedad Matemática Española
Nacional

Autores Gilberto Pérez, José María Barja Pérez
Lugar Madrid (España)

Cargos

Cargos académicos o de gestión para el/la docente.

Claustro

Profesorado doctor con vinculación permanente

Desde 15/03/2023.

Junta de la Facultad de Informática

PDI (Miembros Natos)

Desde 15/03/2023.

Consejo del Departamento Ciencias de la Computación y Tecnologías de la Información

PDI (Miembros Natos)

Desde 15/03/2023.

Junta de la Facultad de Informática

PDI (Miembros Natos)

Desde 10/03/2021 a 14/03/2023.

Consejo del Departamento Ciencias de la Computación y Tecnologías de la Información

PDI (Miembros Natos)

Desde 10/03/2021 a 14/03/2023.

Claustro

Profesorado doctor con vinculación permanente