Publicaciones de José A. Alonso

Relación (en orden cronológico inverso) de artículos, libros y comunicaciones en congresos hasta el 9 de febrero de 2024.

• Lógica, programación y demostración Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 9 de febrero de 2024.
• El paraíso de Hilbert: Demostración automática en matemáticas (Día Mundial de la Lógica, Sevilla, 11 de enero de 2024).
• Calculemus (Vol. 2: Demostraciones con Lean4). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2023.
• Piensa en Haskell y en Python (Ejercicios de programación con Haskell y con Python). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2023.
• Matemáticas en Lean4. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2023.
• Soluciones de los problemas de Exercitium con Python. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2023.
• Introducción a la programación con Haskell y Python. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2023.
• Exercitium (Ejercicios de programación funcional con Haskell). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2023.
• Curso "Programación lógica con Prolog". Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2022.
• Temas de programación lógica con Prolog. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2022.
• Ejercicios de programación lógica con Prolog. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2022.
• Curso "Programación funcional con Haskell". Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2022.
• Temas de programación funcional con Haskell. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2022.
• Vídeos de Programación funcional con Haskell. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2022.
• Razonando con Lean. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2022.
• Ejercicios de programación funcional con Haskell. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2022. (En colaboración con M.J. Hidalgo).
• Lógica en Haskell. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2021.
• Lean para matemáticos. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2021.
• Formalización de las matemáticas en Lean. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2021.
• Calculemus (Ejercicios de demostración con Isabelle/HOL y Lean). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2021.
• Exámenes de “Programación funcional con Haskell”. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2021.
• Demostración asistida por ordenador con Lean. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2021.
• Lógica con Lean. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2020.
• Ejercicios de lógica proposicional con Lean. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2020.
• Ejercicios de lógica de primer orden con Lean. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2020.
• Matemáticas en Lean. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2020.
• Exámenes de programación funcional con Haskell. Vol. 11 (Curso 2019–20). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2020.
• Temas interactivos de programación funcional con Haskell. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2019.
• Temas de “Programación funcional” (curso 2019–20). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2019.
• Exámenes de programación funcional con Haskell. Vol. 10 (Curso 2018–19). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2019.
• Exámenes de programación funcional con Haskell. Vol. 9 (Curso 2017–18). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2018.
• A logic-algebraic tool for reasoning with Knowledge-Based Systems. Journal of Logical and Algebraic Methods in Programming. Volume 101, December 2018, Pages 88-109. (En colaboración con G.A. Aranda, J. Borrego, M.M. Fernández y M.J. Hidalgo).
• Demostración asistida por ordenador con Isabelle/HOL. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2018.
• Demostración asistida por ordenador con Coq. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2018.
• Ejercicios de "Informática de 1º de Matemáticas" (2017-18). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2018.
• Exámenes de programación funcional con Haskell. Vol. 8 (Curso 2016–17). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2017.
• Temas de programación funcional con Haskell (2017-18). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2017.
• Ejercicios de "Informática de 1º de Matemáticas" (2016-17). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2017.
• Temas de programación funcional con Haskell (2016-17). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2017.
• Ejercicios de "Informática de 1º de Matemáticas" (2015-16). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2017.
• Temas de programación funcional con Haskell (2015-16). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2017.
• Exámenes de programación funcional con Haskell. Vol. 7 (Curso 2015–16). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2016.
• Proving termination with multiset orderings in PVS: theory, methodology and applications. ESCIM 2015 (En colaboración con M.J. Hidalgo y F.J. Martín).
• Exámenes de programación funcional con Haskell. Vol. 6 (Curso 2014–15). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2015.
• Manual de la librería de diccionarios Data.Map. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2015.
• Manual de la librería de conjuntos Data.Set. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2015.
• Manual de la librería de números primos. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2015.
• Manual de la librería de matrices Data.Matrix. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2014.
• Manual de la librería de vectores Data.Vector. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2014.
• Manual de tipos abstractos de datos. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2014.
• Manual de funciones básicas de Haskell. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2014.
• Resumen de funciones predefinidas de Haskell. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2015.
• Exámenes de programación funcional con Haskell. Vol. 5 (Curso 2013–14). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2014.
• Revisiting four-valued logics from Maple using the Logics Explorer package. Mathematics and Computers in Simulation. Vol. 104, October 2014, Pages 31–42. (En colaboración con E. Roanes-Lozano y A. Hernando).
• An approach from answer set programming to decision making in a railway interlocking system. Revista de la Real Academia de Ciencias Exactas, Fisicas y Naturales. Serie A. Matematicas. Vol 100, September 2014, No. 2. (En colaboración con E. Roanes-Lozano y A. Hernando).
• Exámenes de programación funcional con Haskell. Vol. 4 (Curso 2012–13). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2013.
• Introducción a la demostración asistida por ordenador con Isabelle/HOL. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2013.
• Exámenes de programación funcional con Haskell. Vol. 3 (Curso 2011–12). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
• Temas de programación funcional con Haskell (2012-13). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2013.
• Temas de programación lógica e inteligencia artificial. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2013.
• Piensa en Haskell (Ejercicios de programación funcional con Haskell). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
• Exámenes de programación funcional con Haskell. Vol. 2 (Curso 2010–11). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2011.
• The Logics' Explorer: a Maple package for exploring finite many-valued propositional logics. Revista de la Real Academia de Ciencias Exactas, Fisicas y Naturales. September 2011, Volume 105, Issue 2, pp 323–337. (En colaboración con E. Roanes-Lozano, A. Hernando, L.M. Laita y E. Roanes-Macías).
• Exámenes de programación funcional con Haskell. Vol. 1 (Curso 2009–10). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2010.
• Introducción al cálculo simbólico con Maxima. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2010.
• A logic approach to decision taking in a railway interlocking system using Maple. Mathematics and Computers in Simulation. Volume 82, Issue 1, September 2011, Pages 15-28. (En colaboración con E. Roanes, A. Hernando y L.M. Laita).
• Proof Pearl: A formal proof of Higman's lemma in ACL2. Journal of Automated Reasoning. October 2011, Volume 47, Issue 3, pp 229–250
• Formalización de la demostración de completitud de la lógica proposicional en Isabelle/Isar. Workshop on Computational Logics and Artificial Intelligence (CLAI 2009). (En colaboración con F.F. Serrano).
• Sistema certificado de decisión proposicional basado en polinomios. Workshop on Computational Logics and Artificial Intelligence (CLAI 2009). (En colaboración con G. Aranda y J. Borrego).
• Algoritmo para resolver k-SAT basado en cláusulas. Workshop on Computational Logics and Artificial Intelligence (CLAI 2009). (En colaboración con E.S. Barraza).
• Inconsistency, logic databases and ontologies. Handbook of Research on Innovations in Database Technologies and Applications: Current and Future Trends. Hershey Pa. Igi Global. 2009. Pag. 452-459. (En colaboración con J. Borrego y A.M. Chávez).
• Formalización de la demostración de completitud de la lógica proposicional en Isabell/Isar. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2009. (En colaboración con F.F. Serrano).
• Extending attribute explorations by means of boolean derivatives. Proceedings of the Sixth International Conference on Concept Lattices and Their Applications. Olomouc, Chequia. Radim Belohlavek and Sergei O. Kuznetsov. Vol. 1. 2008. Pag. 121-132. (En colaboración con G. Aranda, J. Borrego, M. Fernández y M.J. Hidalgo).
• Introducción a la demostración asistida por ordenador (con Isabelle/Isar). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2008.
• Constructing formally verified reasoners for the ALC description logic. Electronic Notes in Theoretical Computer Science. Volume 200, Issue 3, 23 May 2008, Pages 87-102. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• Lógica en Haskell. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2007.
• Pragmatic knowledge integration based on semantic interoperability in business. E-Commerce 2007 IADIS International Conference, 2007. pp. 1-37. (En colaboración con A. Paredes, J. Borrego y G. Aranda).
• KRRT: Knowledge Representation and Reasoning Tutor System. En "Computer Aided Systems Theory (EUROCAST 2007)". Lecture Notes in Computer Science, Volume 4739 (2007), pp. 400-407. (En colaboración con G. Aranda y F.J. Martín).
• A formally verified prover for the ALC description logic. En "Theorem Proving in Higher Order Logics". Lecture Notes in Computer Science. Vol. 4732. 2007. Pag. 135-150. (En colaboración con J. Borrego, M.J. Hidalgo, F.J. Martín y J.L. Ruiz)
• Soluciones de exámenes de "Lógica informática". Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2007.
• FITS: Formalization With an Intelligent Tutor System. Current Developments in Technology-Assisted Education (2006). Badajoz, España. Formatex. Vol. 3. 2006. Pag. 861-865. (En colaboración con G. Aranda y F.J. Martín).
• Semantic Web Verification: Verifying Reasoning in the Logic ALC. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2007. (En colaboración con J. Borrego, M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• Formal correctness of a quadratic unification algorithm. Journal of Automated Reasoning. August 2006, Volume 37, Issue 1–2, pp 67–92 (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• Introducción al razonamiento automático con OTTER. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2006.
• Ejercicios de programación declarativa con Prolog. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2006.
• Introducción a la programación lógica con Prolog. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2006.
• Solución declarativa del Sudoku mediante ASP Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2006.
• A formally verified proof (in PVS) of the strong completeness theorem of propositional SLD-resolution. Actas del Congreso EUROCAST. 2005. Pag. 83-86. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• Temas de "Lógica informática" (2005-06) Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2006.
• Temas de "Programación declarativa" (2005-06) Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2006. (En colaboración con A. Cordón).
• Foundational challenges in automated data and ontology cleaning in the Semantic Web. IEEE Intelligent Systems Vol. 21, no. 1, 2006, pp. 42-52. (En colaboración con J. Borrego, A.M. Chávez y F.J. Martín)
• Formalización en PVS de la buena fundamentación del orden de multiconjuntos. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2005. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• Formalización de la lógica descriptiva ALC en PVS. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2005. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• Proof pearl: a formal proof of Higman's lemma in ACL2. TPHOLs 2005, pp. 358-372. Lecture Notes in Computer Science, Vol. 3603, Springer-Verlag, 2005. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz) © Springer-Verlag.
• Rete algorithm applied to robotic soccer. EUROCAST 2005, pp. 571-576. Lecture Notes in Computer Science, Vol. 3643, Springer-Verlag, 2005. (En colaboración con F.J. Martín y F. Palomo) © Springer-Verlag.
• Desarrollo de teorías computacionales. MAT.ES, 2005.
• Logic databases and inconsistency handling. Encyclopedia of Databases Technologies and Applications. Idea Group Publishing, 2005, pp. 336-340. (En colaboración con J. Borrego y A.M. Chávez).
• Temas de "Lógica y programación" (2004-05) Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2005. (En colaboración con F.J. Martín y J.L. Ruiz).
• Temas de "Lógica informática" (2004-05) Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2005.
• Temas de "Programación declarativa" (2004-05) Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2005.
• Towards a tool for ontology engineering. World Automation Congress: Advances in Robotics, Manufacturing, Automation, Control, Soft Computing, Multimedia, Biomedicine, Image Processing and Financial Engineering. Vol. IV. Tsi Press. 2004. Pag. 1-100. (En colaboración con J. Borrego y M.A. Chávez).
• Formal verification of a generic framework to synthesize SAT-provers. Journal of Automated Reasoning, Vol. 32, Núm. 4, 2004, pp. 287-313. (En colaboración con M.J. Hidalgo, FJ. Martín y J.L. Ruiz).
• Verified computer algebra in ACL2 (Gröbner bases computation). AISC 2004. pp. 171-184. Lecture Notes in Computer Science, Vol. 3249, Springer-Verlag, 2004. (En colaboración con I. Medina, F. Palomo y J.L. Ruiz).
• Formal verification of molecular computational models in ACL2: A case study. CAEPIA-TTIA 2003,pp. 344-354. Lecture Notes in Computer Science, Vol. 3040, Springer-Verlag, 2004. (En colaboración con M.J. Hidalgo, FJ. Martín y J.L. Ruiz). © Springer-Verlag.
• Verification of the formal concept analysis. RACSAM (Revista de la Real Academia de Ciencias),Serie A: Matemáticas, Vol. 98, 2004, pp. 3-16. (En colaboración con J. Borrego, M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• Ontology cleaning by mereotopological reasoning. Database and Expert Systems Applications. (DEXA 2004). IEEE Press. 2004. pp. 132-137. (En colaboración con J. Borrego y A.M. Chávez).
• A formally verified quadratic unification algorithm. Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2004). University of Austin, 2004. Pag. 1-32. (En colaboración con M.J. Hidalgo, FJ. Martín y J.L. Ruiz).
• Formal reasoning about efficient data structures: A case study in ACL2. LOPSTR 2003,pp. 75-91. Lecture Notes in Computer Science, Vol. 3018, Springer-Verlag, 2004. (En colaboración con M.J. Hidalgo, FJ. Martín y J.L. Ruiz). © Springer-Verlag.
• Temas de "Lógica informática" (2003-04) Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2004.
• A formal proof of Dickson's lemma in ACL2. LPAR 2003 pp. 49-58. Lecture Notes in Computer Science, Vol. 2850, Springer-Verlag, 2003. (En colaboración con M.J. Hidalgo, FJ. Martín y J.L. Ruiz).
• Verification in ACL2 of a generic framework to synthesize SAT-provers. LPOSTR 2002, pp. 182-198. Lecture Notes in Computer Science, Vol. 2664, Springer-Verlag. (En colaboración con M.J. Hidalgo, FJ. Martín y J.L. Ruiz).
• Towards a practical argumentative reasoning with qualitative spatial databases. IEA/AIE 2003,Lecture Notes in Artificial Intelligence, Vol. 2718, Springer-Verlag, 2003. Pag. 789-798. (En colaboración con J. Borrego, A.M. Chávez, M.A. Gutiérrez y J.D. Navarro).
• Generalizing logic programs via subsumption. EUROCAST 2003, Lecture Notes in Computer Science, Vol. 2809, Springer-Verlag, 2003. (En colaboración con J. Borrego y M.A. Gutiérrez).
• Termination in ACL2 using multiset relation. En Thirty Five Years of Automating Mathematics. Kluwer Academic Publishers, 2003, pp. 217-245. (En colaboración con M.J. Hidalgo, FJ. Martín y J.L. Ruiz).
• Verificación formal y eficiencia: Un caso de estudio aplicado a la unificación de términos. I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, IBERAMIA 2002, pp. 77-90. (En colaboración con M.J. Hidalgo, FJ. Martín y J.L. Ruiz).
• Towards a practical argumentative reasoning with qualitative spatial database. I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, IBERAMIA 2002, pp. 111-120. (En colaboración con J. Borrego, A.M. Chávez, M.A. Gutiérrez y J.D. Navarro).
• Desarrollo formal y verificación de sistemas proposicionales. I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, IBERAMIA 2002, pp. 1-12. (En colaboración con M.J. Hidalgo, FJ. Martín y J.L. Ruiz).
• Algoritmos polinómicos en ACL2 (Una aproximación al algoritmo de Buchberger). I Taller Iberoamericano sobre Deduccion Automatica e Inteligencia Artificial, IBERAMIA 2002. (En colaboración con I. Medina y F. Palomo).
• Una introducción al análisis formal de conceptos en PVS. I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, IBERAMIA 2002, pp. 33-46. (En colaboración con M.J. Hidalgo, FJ. Martín y J.L. Ruiz).
• A quasi-metric for machine learning. IBERAMIA 2002,pp. 193-203. Lecture Notes in Computer Science, Vol. 2527, Springer-Verlag, 2002. (En colaboración con J. Borrego y M.A. Gutiérrez).
• Agentes inteligentes: Una aproximación desde la Lógica Computacional. Editorial Kronos,2002. (En colaboración con J. Borrego).
• A methodology for the computer-aided cleaning of complex knowledge databases. IECON 2002.IEEE Industrial Electronic Society, 2002, pp. 1806-1811. (En colaboración con J. Borrego, A.M. Chávez, M.A. Gutiérrez y J.D. Navarro).
• Deducción automática (Vol. 1: Construcción lógica de sistemas lógicos). (Ed. Kronos, 2002). (En colaboración con J. Borrego)
• Formal proofs about rewriting using ACL2. Annals of Mathematics and Artificial Intelligence Vol. 36, no. 3, 2002, pp. 239-262. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• A generic instantiation tool and a case study: a generic multiset theory. 3rd Intl. Workshop on the ACL2 Theorem Prover and its Applications. Grenoble, 2002. Proceedings of the Conference. 2002. Pag. 188-203. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• A theory about first-order terms in ACL2. 3rd Intl. Workshop on the ACL2 Theorem Prover and its Applications. Grenoble, 2002. Proceedings of the Conference. 2002. Pag. 78-100. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• Implementation in ACL2 of well-founded polynomial orderings. 3rd Intl. Workshop on the ACL2 Theorem Prover and its Applications. Grenoble, 2002. (En colaboración con I. Medina y F. Palomo).
• Molecular computation models in ACL2: a simulation of Lipton's experiment solving SAT. 3rd Intl. Workshop on the ACL2 Theorem Prover and its Applications. Grenoble, 2002. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• Progress report: term dags using stobjs. 3rd Intl. Workshop on the ACL2 Theorem Prover and its Applications. Grenoble, 2002. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• A certified polynomial-based decision procedure for propositional logic. TPHOLs 2001, pp. 297-312. Lecture Notes in Computer Science, Vol. 2152, Springer-Verlag, 2002. (En colaboración con I. Medina y F. Palomo).
• Certification of matrix multiplication algorithms. Strassen's algorithm in ACL2. 14th International Conference Theorem Proving in Higher Order Logics: TPHOLs 2001, Edimburgo (Escocia), 2001. (En colaboración con I. Medina y F. Palomo).
• A certified algorithm for translating formulas into polynomials. An ACL2 approach. IJCAR 2001. pp. 103-112, Siena, 2001. (En colaboración con I. Medina y F. Palomo).
• Verifying an applicative ATP using multiset relations. EUROCAST 2001, pp. 616-626. Lecture Notes in Computer Science, Vol. 2178, Springer-Verlag, 2001. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• Formalizing rewriting in the ACL2 theorem prover. En AISC 2000, pp. 92-106. Lecture Notes in Artíficial Intelligence, Vol. 1930, Springer-Verlag, 2001. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• Deducción automática (y el trabajo del grupo de lógica computacional de la Universidad de Sevilla). Conferencias del año mundial de las Matemáticas. Sevilla, 2000.
• Deducción automática en anillos ternarios: algunos métodos de procesamiento del conocimiento matemático. Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 23-32. (En colaboración con J. Borrego y A. Chávez).
• Formalización del razonamiento ecuacional en una lógica computacional. Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 41-50. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• Proximidad entre cláusulas en Programación Lógica Inductiva. Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 33-40. (En colaboración con J. Borrego y M.A. Gutiérrez).
• A mechanical proof of Knuth-Bendix critical pair theorem (using ACL2). Proceedings of FTP'2000, pp. 206-216. Technical Report 5-2000, Fachberichte Informatik, Universitat Koblenz-Landau, 2000. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• A topological study of the upward refinement operators in ILP. Inductive Logic Programming 2000, pp. 120-137. CEUR-WS Vol. 35, 2000. (En colaboración con J. Borrego y M.A. Gutiérrez)
• Reasoning about matrix arithmetic in ACL2. AOC Workshop 2000. Lyon, Francia, 2000. (En colaboración con I. Medina y F. Palomo).
• Automatic verification of polynomial rings: fundamental properties in ACL2. ACL2 Workshop 2000. Technical Report TR-00-29, Dep. of Computer Sciences, Univ. of Texas at Austin, 2000. (En colaboración con I. Medina y F. Palomo).
• Multiset relations: a tool for proving termination. ACL2 Workshop 2000. Technical Report TR-00-29, Dep. of Computer Sciences, Univ. of Texas at Austin (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• Estrategias para la demostración automática de teoremas. Actas IV CINTE, pp. 276-283. Cádiz, 2000. (En colaboración con J. Borrego y A. Chávez)
• Inserción y fusión con listas ordenadas: un ejemplo de razonamiento automático con ACL2. Actas IV CINTE, pp. 284-291. Cádiz, 2000. (En colaboración con I. Medina y F. Palomo).
• Razonamiento automático en programación genérica con ACL2: estudio de un caso. Actas IV CINTE, pp. 292-299. Cádiz, 2000. (En colaboración con I. Medina y F. Palomo).
• Una quasi-métrica basada en subsunción. Actas IV CINTE, pp. 260-267. Cádiz, 2000. (En colaboración con J. Borrego y M.A. Gutiérrez).
• Verificación automática de bases de conocimiento. Demostración automática versus model checking. Actas IV CINTE, pp. 268-275. Cádiz, 2000. (En colaboración con J. Borrego y F. Olías).
• A computer algebra approach to verification and deduction in many-valued knowledge systems. Soft Computing. June 1999, Volume 3, Issue 1, pp 7–19. (En colaboración con L.M. Laita, L. Ledesma y E. Roanes).
• Interpretación reactiva de sistemas basados en conocimiento. IV Congreso ISKO-España EOCONSID'99, pp. 187-193. Granada, 1999. Pag. 187-193. (En colaboración con J. Borrego y M.J. Pérez).
• Mechanical verification of a rule-based unification algorithm in the Boyer-Moore theorem prover. Joint Conference on Declarative Programming, AGP-99, pp. 289-304. L'Aquila (Italia), 1999. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• Curso práctico de teoría de conjuntos. Ediciones la Ñ, Sevilla, 1998. (En colaboración con J. Borrego, M.J. Pérez y J.L. Ruiz).
• Disparo de reglas como método deductivo en sistemas basados en conocimiento. Trabajo interno. Sevilla, 1988. (En colaboración con A. Fernández y L. Laita).
• Razonamiento automático en sistemas de representación del conocimiento (y su relación con la enseñanza de la Inteligencia Artificial). Jornades sobre l'Ensenyament Universitari de la Infomàtica (JENUI'98), pp. 289-296. Barcelona, 1998. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• Verificación automática de sistemas de razonamiento (aplicación a la enseñanza de la Inteligencia Artificial). Jornades sobre l'Ensenyament Universitari de la Infomàtica (JENUI'98), pp. 297-304. Barcelona, 1998. (En colaboración con M.J. Hidalgo, F.J. Martín y J.L. Ruiz).
• Temas de "Teoría de conjuntos" (1997-98). Departamento de Ciencias de la Computación e Inteligencia Artificial. Universidad de Sevilla, 1998.
• Ejercicios de "Teoría de conjuntos" (1997-98). Departamento de Ciencias de la Computación e Inteligencia Artificial. Universidad de Sevilla, 1998. (En colaboración con M.J. Pérez).
• Una aproximación a la inteligencia artificial. Conferencia. Sevilla, 1997.
• GTI: Una herramienta de edición de cursos adaptativos. XIII Congreso Nacional de Ingeniería del Diseño, pp. 627-634. Sevilla, 1997. (En colaboración con J.J. Arrabal, D. Balbontín, F.F. Lara, F.J. Martín, M.J. Pérez y J.L. Ruiz).
• Hacia una enseñanza permanente y automatizada: WWW y evaluación automática con GTI. International Congress on Historical Information Systems. Vitoria. 1997. Pag. 1-10. (En colaboración con J.J. Arrabal y R. Fernández).
• Lógica computacional. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 1996.
• Razonamiento automático. En Lógica formal (Orígenes, métodos y aplicaciones), pp. 189-211. Ed. Kronos, Sevilla, 1996. (En colaboración con A. Fernández y M.J. Pérez)
• Verificación automática de SBC basada en lógica trievaluada: teoría e implementación. I Jornadas sobre Inteligencia Artificial, control y sistemas expertos, pp. 241-254. Universidad de Alcalá, 1996. (En colaboración con E. Briales, L.M. Laita y E. Roanes).
• Deducción automática y programación lógica. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 1995.
• Aprende Matemáticas. Primer Encuentro de Informática Educativa (EDIE). CEES (Madrid). Asociacion para el Desarrollo de la Informatica Educativa. 1994. Pag. 20-25. (En colaboración con D. Balbontín, M.L. de la Vega y J.J. Arrabal).
• Automatización de la aritmética. Lenguajes Naturales y Lenguajes Formales X, pp. 167-182. Sevilla, 1994. (En colaboración con J.J. Arrabal, A. Fernández y M.J. Pérez).
• Ejercicios de "Teoría de conjuntos" (1993-94). Departamento de Ciencias de la Computación e Inteligencia Artificial. Universidad de Sevilla, 1993. (En colaboración con M.J. Pérez).
• Especificación formal de bases de datos con un demostrador automático de teoremas. Programación Declarativa PRODE'93, pp. 343-345. Blanes, 1993. (En colaboración con J.J. Arrabal, D. Balbontín y J. Herrera).
• Sobre la enseñanza de la Lógica. I Congreso de la Sociedad de Lógica, Metodología y Filosofía de la Ciencia, pp. 6-9. Madrid, 1993. (En colaboración con A. Nepomuceno, M.J. Hidalgo y F.J. Salguero).
• Ejercicios de "Teoría de conjuntos" (1992-93). Departamento de Ciencias de la Computación e Inteligencia Artificial. Universidad de Sevilla, 1992. (En colaboración con M.J. Pérez).
• Automated proofs in group theory with OTTER. Fifth International Symposium on Knowledge Engineering, pp. 326-331. Sevilla, 1992. (En colaboración con J.J. Arrabal, D. Balbontín y J. Herrera).
• Razonamiento automático en lógica de primer orden Lenguajes Naturales y Lenguajes Formales VIII Gerona, 1992. (En colaboración con J.J. Arrabal, D. Balbontín y J. Herrera).
• Ejercicios de "Teoría de conjuntos" (1991-92). Departamento de Álgebra, Computación, Geometría y Topología. Universidad de Sevilla, 1991.
• Lógica computacional. Departamento de Álgebra, Computación, Geometría y Topología. Universidad de Sevilla, 1991.
• Curso de programación en Lisp. Departamento de Álgebra, Computación, Geometría y Topología. Universidad de Sevilla, 1991.
• Manual de Lisp. Departamento de Álgebra, Computación, Geometría y Topología. Universidad de Sevilla, 1991.
• Multi-valued logic and Gröbner bases with applications to modal logic. Journal of Symbolic Computation. Volume 11, Issue 3, March 1991, Pages 181-194. (En colaboración con E. Briales, J. Chazarain y A. Riscos).
• Ejercicios de "Implementación de algoritmos y cálculo simbólico" (1990-91). Departamento de Álgebra, Computación, Geometría y Topología. Universidad de Sevilla, 1990.
• Curso de Lisp (con Golden Common Lisp). Departamento de Álgebra, Computación, Geometría y Topología. Universidad de Sevilla, 1990.
• Manual de Golden Common Lisp. Departamento de Álgebra, Computación, Geometría y Topología. Universidad de Sevilla, 1990.
• Lógicas polivalentes y bases de Gröbner. Lenguajes Naturales y Lenguajes Formales V, pp. 307-315. Barcelona, 1990. (En colaboración con E. Briales).
• Preuve automatique dans le calcul propositionnel et les logiques trivalentes. Computacional Topology and Geometry and Computation in Teaching Matemathics, pp. 15-24. Sevilla, 1990. (En colaboración con E. Briales y A. Riscos).
• Ejercicios de "Teoría de conjuntos" (1989-90). Departamento de Álgebra, Computación, Geometría y Topología. Universidad de Sevilla, 1989.
• Representación en modelos no-estándard de sublenguajes de la aritmética. Lenguajes Naturales y Lenguajes Formales IV, pp. 441-464. Barcelona, 1989. (En colaboración con A. Fernández).
• Algebraic methods of automated reasoning in monadic logic. Departamento de Álgebra, Computación, Geometría y Topología. Universidad de Sevilla, 1989.
• Métodos algebraicos de razonamiento automático. En Tesis Doctorales (Resúmenes), pp. 339-341. Universidad de Sevilla, 1989.
• Decidability of modal system S5: a recursive algorithm. Departamento de Álgebra, Computación, Geometría y Topología. Universidad de Sevilla, 1988. (En colaboración con A. Briales).
• Preuve automatique dans le calcul propositionnel et les logiques trivalentes. Congress on Computacional Topology and Geometry and Computation in Teaching Matemathics. Sevilla, 31 de Agosto a 4 de Septiembre de 1987. (En colaboración con E. Briales y A. Riscos).