| Libro | 2017 |
Future and Emerging Trends in Language Technology. Machine Learning and Big Data: Second International Workshop, FETLT 2016, Seville, Spain, November 30 –December 2, 2016, Revised Selected Papers
|
Future and Emerging Trends in Language Technology. Machine Learning and Big Data: Second International Workshop, FETLT 2016, Seville, Spain, November 30 –December 2, 2016, Revised Selected Papers |
| Ponencia | 2017 |
Using abstract stobjs in ACL2 to compute matrix normal forms
|
Lecture Notes in Computer Science |
| Ponencia | 2016 |
Future and emergent trends in language technology: First international workshop, FETLT 2015 Seville, Spain, november 19–20, 2015 revised selected papers
|
Lecture Notes in Computer Science |
| Editorial | 2016 |
Preface
|
Lecture Notes in Computer Science |
| Ponencia | 2016 |
Towards a veri fiable Topology of Data
|
XV Encuentro de Álgebra computacional y aplicaciones: EACA 2016 |
| Artículo | 2015 |
Modelling algebraic structures and morphisms in ACL2
|
APPLICABLE ALGEBRA IN ENGINEERING COMMUNICATION AND COMPUTING |
| Ponencia | 2014 |
Artificial intelligence and symbolic computation: 12th international conference, AISC 2014 Seville, Spain, December 11-13, 2014 proceedings
|
Lecture Notes in Computer Science |
| Artículo | 2014 |
Formally Verified Tableau-Based Reasoners for a Description Logic
|
JOURNAL OF AUTOMATED REASONING |
| Editorial | 2014 |
Preface
|
Lecture Notes in Computer Science |
| Artículo | 2014 |
Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm
|
Logic Journal of the IGPL |
| Ponencia | 2013 |
Certified symbolic manipulation: Bivariate simplicial polynomials
|
Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC |
| Artículo | 2012 |
Formalization of a normalization theorem in simplicial topology
|
ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE |
| Ponencia | 2011 |
Applying ACL2 to the formalization of algebraic topology: Simplicial polynomials
|
Lecture Notes in Computer Science |
| Capítulo | 2011 |
Computational logic and knowledge representation issues in data analysis for the semantic web
|
Data Management in the Semantic Web |
| Artículo | 2011 |
Proof Pearl: a Formal Proof of Higman's Lemma in ACL2
|
JOURNAL OF AUTOMATED REASONING |
| Ponencia | 2010 |
Expert System to Real Time Control of Machining Processes
|
CURRENT TOPICS IN ARTIFICIAL INTELLIGENCE |
| Ponencia | 2010 |
Sensorización y control de un proceso de mecanizado utilizando un sistema experto basado en reglas.
|
Proceedings from the 14th International Congress on Project Management and Engineering. Comunicaciones presentadas al XIV Congreso Internacional de Ingeniería de Proyectos: 1st Latin American Conference on Project Engineering: Madrid 30 de junio, 1 y 2 de julio de 2010 |
| Capítulo | 2010 |
Topología simplicial en ACL2
|
Contribuciones científicas en honor de Mirian Andrés Gómez |
| Ponencia | 2009 |
ACL2 verification of simplicial degeneracy programs in the kenzo system
|
INTELLIGENT COMPUTER MATHEMATICS, PROCEEDINGS |
| Ponencia | 2009 |
Verificación y eficiencia en programas para el cálculo simbólico: estudio de un caso
|
Programación y lenguajes: IX Jornadas sobre Programación y Lenguajes, PROLE'09, I Taller de Programación Funcional, TPF'09, San Sebastián, España, del 8 al 11 de septiembre de 2009 |
| Ponencia | 2007 |
A formally verified prover for the ALC description logic
|
THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS |
| Ponencia | 2007 |
A formally verified prover for the ALC description logic
|
Lecture Notes in Computer Science |
| Ponencia | 2007 |
KRRT: Knowledge Representation and Reasoning Tutor system
|
COMPUTER AIDED SYSTEMS THEORY- EUROCAST 2007 |
| Ponencia | 2007 |
KRRT: Knowledge representation and reasoning tutor system
|
Lecture Notes in Computer Science |
| Artículo | 2006 |
Formal correctness of a quadratic unification algorithm
|
JOURNAL OF AUTOMATED REASONING |
| Artículo | 2006 |
Foundational challenges in automated Semantic Web data and ontology cleaning
|
IEEE INTELLIGENT SYSTEMS |
| Artículo | 2005 |
Proof pearl: A formal proof of Higman's lemma in ACL2
|
THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS |
| Ponencia | 2005 |
Proof pearl: A formal proof of Higman's Lemma in ACL2
|
Lecture Notes in Computer Science |
| Artículo | 2005 |
Rete algorithm applied to robotic soccer
|
Computer Aided Systems Theory – EUROCAST 2005: 10th International Conference on Computer Aided Systems Theory, Las Palmas de Gran Canaria, Spain, February 7-11, 2005, Revised Selected Papers |
| Capítulo | 2005 |
Topología Simplicial en ACL2
|
Manual de responsabilidad pública: homenaje a Pedro González Gutiérrez-Barquín |
| Artículo | 2004 |
Formal reasoning about efficient data structures: A case study in ACL2
|
Lecture Notes in Computer Science |
| Artículo | 2004 |
Formal verification of a generic framework to synthesize SAT-provers
|
JOURNAL OF AUTOMATED REASONING |
| Ponencia | 2004 |
Formal verification of molecular computational models in ACL2: A case study
|
Lecture Notes in Computer Science |
| Artículo | 2003 |
A formal proof of Dickson's Lemma in ACL2
|
LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS |
| Artículo | 2003 |
Verification in ACL2 of a generic framework to synthesize SAT-provers
|
LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION |
| Artículo | 2002 |
Formal proofs about rewriting using ACL2
|
ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE |
| Capítulo | 2001 |
Formalización del razonamiento ecuacional en una lógica computacional
|
Actas del Encuentro de Matemáticos Andaluces |
| Artículo | 2001 |
Formalizing rewriting in the ACL2 theorem prover
|
ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION |
| Ponencia | 2001 |
Formalizing rewriting in the ACL2 theorem prover
|
Lecture Notes in Computer Science |
| Artículo | 2001 |
Verifying an applicative ATP using multiset relations
|
COMPUTER AIDED SYSTEMS THEORY - EUROCAST 2001 |
| Ponencia | 2001 |
Verifying an applicative ATP using multiset relations
|
Lecture Notes in Computer Science |
