PhD Gilberto Pérez Vega  

(TIT-EU DR)

Department Computer Science
Knowledgment area Algebra
Research  Research group Information Retrieval Lab
Research lines - 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.
Keywords Verificación Formal, Métodos Formales, Teoría de Prueba, Lógica Intucionista, Answer Set Programming (ASP).
Contacto UDC directory

Teaching

Subjects taught

This section shows the teaching given in degrees, masters and other officers studies in last 6 years.

Subject and involved studies Total hours
Algebra 89
Algorithms 12
Discrete Mathematics 120
Final Project. Mention in Computer Science 4
Software Verification and Validation 35
Subject and involved studies Total hours
Algebra
Degree in Computer Engineering
105
Algorithms
Degree in Computer Engineering
10
Discrete Mathematics
Degree in Computer Engineering
100
Final Project. Mention in Computer Science
Degree in Computer Engineering
4
Software Verification and Validation
Degree in Computer Engineering
35
Subject and involved studies Total hours
Algebra
Degree in Computer Engineering
120
Discrete Mathematics
Degree in Computer Engineering
73
Software Verification and Validation
Degree in Computer Engineering
35
Subject and involved studies Total hours
Algebra
Degree in Computer Engineering
88
Discrete Mathematics
Degree in Computer Engineering
120
Software Verification and Validation
Degree in Computer Engineering
42
Subject and involved studies Total hours
Discrete Mathematics
Degree in Computer Engineering
160
Software Verification and Validation
Degree in Computer Engineering
39
Subject and involved studies Total hours
Discrete Mathematics
Degree in Computer Engineering
155
Software Validation and Verification
Degree in Computer Engineering
17
Software Verification and Validation
Degree in Computer Engineering
32

Defined tutoring by teacher for 2018/2019 academic course.

Faculty of Computer Science

Quarter Day Site
1st quarter Monday
12:30 a 13:30
Despacho
1st quarter Monday
15:30 a 16:30
Despacho
1st quarter Thursday
10:30 a 12:30
Despacho

EOG works and final master thesis directed

Directed or codirected by current teacher since 2013 year.

Rule-Based Decision Support System for Lever Transplantation
A Diagrammatic Reasoning Tool for Logic Programming
A type system for functional Answer Set programming.

Research results

Select merit type and year to query research merits.

RAZONAMIENTO AUTOMATICO TEMPORAL PARA SISTEMAS INTELIGENTES DINAMICOS (TARDIS)

Funding entity Ministerio de Economía y Competitividad (MINECO)
Main researches Pedro Cabalar Fernández
Type Proyecto Programas Nacionales
Dates From 01/01/2018 to 31/12/2020

Axudas para acreditación, estructuración e mellora de Centros de Investigación Singulares do Sistema Universitario de Galicia

Funding entity Consellería de Cultura, Educación e Ordenación Universitaria
Main researches M. G. Penedo
Type Proyecto Programas Autonomicos
Dates From 01/01/2016 to 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)"

Funding entity Consellería de Cultura, Educación e Ordenación Universitaria
Main researches Manuel Vilares Ferro
Type Proyecto Programas Autonomicos
Dates From 01/01/2014 to 31/12/2015

MERLOT: RAZONAMIENTO MÉDICO CON HERRAMIENTAS LÓGICAS

Funding entity Ministerio de Economía y Competitividad (MINECO)
Main researches José Pedro Cabalar Fernández
Type Proyecto Programas Nacionales
Dates From 01/01/2014 to 31/12/2016

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

Funding entity Ministerio de Economía y Competitividad
Type Proyecto Otros Programas
Dates From 01/01/2010 to 31/12/2012

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

Funding entity Dirección Xeral de Investigación, Desenvolvemento e Innovación
Type Proyecto Otros Programas
Dates From 01/01/2008 to 31/10/2011

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

Type Proyecto Otros Programas
Dates From 01/10/2006 to 30/09/2009

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

Type Proyecto Otros Programas
Dates From 01/10/2006 to 30/09/2009

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

Funding entity Ministerio de Ciencia y Tecnología
Main researches Víctor M. Gulías Fernández
Type Proyecto Programas Nacionales
Dates From 05/11/2002 to 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

Funding entity Secretaria Xeral de Investigación e Desenvolvemento Tecnolóxico
Main researches José María Cardesín Díaz
Type Proyecto Programas Autonomicos
Dates From 08/10/2002 to 08/10/2005

Representación de coalgebras y categorías derivadas

Funding entity Secretaria Xeral de Investigación e Desenvolvemento Tecnolóxico
Type Proyecto Otros Programas
Dates From 25/08/2000 to 25/08/2002

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

Funding entity Dirección Xeral de Universidades
Type Proyecto Otros Programas
Dates From 24/10/1996 to 24/10/1998

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

Funding entity Dirección Xeral de Universidades
Main researches José Luis Freire Nistal
Type Proyecto Otros Programas
Dates From 01/01/1994 to 31/12/1995

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

Funding entity Consellería de Educación e Ordenación Universitaria
Main researches Antonio Ángel Blanco Ferro
Type Proyecto Programas Autonomicos
Dates From 07/04/1994 to 07/04/1997

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

Authors Mª Felicidad Aguado Martín, Pablo Fernández Ascariz, José Pedro Cabalar Fernández, Gilberto Pérez Vega, Concepción Vidal Martín
Journal LOGIC JOURNAL OF THE IGPL Vol. 25 Num. 2 (pages 195 to 213)
DOI https://doi.org/10.1093/jigpal/jzw060

Temporal logic programs with variables

Authors Mª Felicidad Aguado Martín, José Pedro Cabalar Fernández, Martín Diéguez Lodeiro, Gilberto Pérez Vega, Concepción Vidal Martín
Journal THEORY AND PRACTICE OF LOGIC PROGRAMMING Vol. 17 Num. 2 (pages 226 to 243)
DOI https://doi.org/10.1017/s1471068416000570

Temporal Equilibrium Logic with past operators

Authors Mª Felicidad Aguado Martín, José Pedro Cabalar Fernández, Martín Diéguez Lodeiro, Gilberto Pérez Vega, Concepción Vidal Martín
Journal Journal of Applied Non-Classical Logics Vol. 27 Num. 3-4 (pages 161 to 177)
DOI https://doi.org/10.1080/11663081.2018.1427987

A denotational semantics for equilibrium logic

Authors Mª Felicidad Aguado Martín, José Pedro Cabalar Fernández, Gilberto Pérez Vega, Concepción Vidal Martín, David Pearce
Journal THEORY AND PRACTICE OF LOGIC PROGRAMMING Vol. 15 Num. 4-5 (pages 620 to 634)
DOI https://doi.org/10.1017/s1471068415000277

Temporal Equilibrium Logic: a survey

Authors Mª Felicidad Aguado Martín, José Pedro Cabalar Fernández, Gilberto Pérez Vega, Concepción Vidal Martín, Martín Diéguez Lodeiro
Journal Journal of Applied Non-Classical Logics Vol. 23 Num. 1-2 (pages 2 to 24)
DOI https://doi.org/10.1080/11663081.2013.798985

Integrating Temporal Extensions of Answer Set Programming

Authors Mª Felicidad Aguado Martín, Gilberto Pérez Vega, Concepción Vidal Martín
Journal LECTURE NOTES IN COMPUTER SCIENCE Vol. 8148 (pages 23 to 35)
DOI https://doi.org/10.1007/978-3-642-40564-8_3

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

Authors Concepción Vidal Martín, Gilberto Pérez Vega, Mª Felicidad Aguado Martín, José Mª Molinelli Barba
Journal LOGIC JOURNAL OF THE IGPL Vol. 19 Num. 2 (pages 405 to 414)

Loop Formulas for Splitable Temporal Logic Programs

Authors Mª Felicidad Aguado Martín, José Pedro Cabalar Fernández, Gilberto Pérez Vega, Concepción Vidal Martín
Journal LECTURE NOTES IN COMPUTER SCIENCE Vol. 6645 (pages 80 to 92)
DOI https://doi.org/10.1007/978-3-642-20895-9_9

Strongly equivalent temporal logic problems

Authors Mª Felicidad Aguado Martín, José Pedro Cabalar Fernández, Gilberto Pérez Vega, Concepción Vidal Martín
Journal LECTURE NOTES IN COMPUTER SCIENCE Vol. 5293 (pages 8 to 20)

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

Authors Mª Felicidad Aguado Martín, José Luis Doncel Juárez, José Mª Molinelli Barba, Gilberto Pérez Vega, Concepción Vidal Martín
Journal Journal of Formalized Reasoning (pages 25 to 37)

Certified Genetic Algorithms: Crossover Operators for Permutations

Authors Mª Felicidad Aguado Martín, José Luis Doncel Juárez, José Mª Molinelli Barba, Gilberto Pérez Vega, Concepción Vidal Martín, Ana Maria Vieites Rodriguez
Journal LECTURE NOTES IN COMPUTER SCIENCE Vol. 4739 (pages 282 to 289)

Minimal Logic Programs

Authors José Pedro Cabalar Fernández, Gilberto Pérez Vega
Journal LECTURE NOTES IN COMPUTER SCIENCE Vol. 4670 (pages 104 to 118)

Temporal Equilibrium Logic: a first approach

Authors José Pedro Cabalar Fernández, Gilberto Pérez Vega
Journal LECTURE NOTES IN COMPUTER SCIENCE Vol. 4739 (pages 241 to 248)

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

Authors Concepción Vidal Martín, Ana Maria Vieites Rodriguez, Mª Felicidad Aguado Martín, Gilberto Pérez Vega, Manuel Ladra González, Felipe Gago Couso
Publishing 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
International

Authors Mª Felicidad Aguado Martín, José Pedro Cabalar Fernández, Jorge Fandiño, David Pearce, Gilberto Pérez Vega, Concepción Vidal Martín
Place Espoo (Finlandia)

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

Authors José Pedro Cabalar Fernández, Carlos Pérez Ramil, Gilberto Pérez Vega
Place New York (Estados Unidos)

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

Authors Mª Felicidad Aguado Martín, José Pedro Cabalar Fernández, David Pearce, Gilberto Pérez Vega, Concepción Vidal Martín
Organization Association for Logic Programming
Place Cork (Irlanda)

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

Authors Mª Felicidad Aguado Martín, José Pedro Cabalar Fernández, Gilberto Pérez Vega, Concepción Vidal Martín
Place Coruña, A (España)

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

Authors Concepción Vidal Martín, Mª Felicidad Aguado Martín, Gilberto Pérez Vega
Place Coruña, A (España)

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

Authors Mª Felicidad Aguado Martín, José Pedro Cabalar Fernández, Martín Diéguez Lodeiro, Gilberto Pérez Vega, Concepción Vidal Martín
Organization International Conference on Logic Programming ICLP
Place Budapest (Hungría)

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

Authors Gilberto Pérez Vega, Mª Felicidad Aguado Martín, Concepción Vidal Martín
Organization Real Sociedad Matemática Española
Place Á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)
International

Authors Mª Felicidad Aguado Martín, José Mª Molinelli Barba, Gilberto Pérez Vega, Concepción Vidal Martín
Place 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
International

Authors Mª Felicidad Aguado Martín, José Mª Molinelli Barba, Gilberto Pérez Vega, Concepción Vidal Martín, Ana Maria Vieites Rodriguez
Place San José (Costa Rica)

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
International

Authors Mª Felicidad Aguado Martín, José Mª Molinelli Barba, Gilberto Pérez Vega, Concepción Vidal Martín, Ana Maria Vieites Rodriguez
Place 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
International

Authors Gilberto Pérez Vega, José Luis Freire Nistal, José Mª Molinelli Barba
Place Cali (Colombia)

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

Authors Gilberto Pérez Vega
Place Valencia (España)

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

Authors Gilberto Pérez Vega, José María Barja Pérez
Place Madrid (España)