Investigación

Publicaciones

• Modelling Algebraic Structures and Morphisms in ACL2, J. Heras, F.J. Martín Mateos, V. Pascual. Applicable Algebra in Engineering, Communication and Computing (ISSN 0938-1279) 26(3), 277-303, Springer, 2015.

• Formally Verified Tableau-Based Reasoners for a Description Logic, M.J. Hidalgo, J.A. Alonso, J. Borrego, F.J. Martín Mateos, J.L. Ruiz, Journal of Automated Reasoning (ISSN 0168-7433), 52(3), 331-360, Springer, 2014.

• Verifying the Bridge between Simplicial Topology and Algebra: the Eilenberg–Zilber Algorithm, L. Lambán, J. Rubio, F.J. Martín Mateos, J.L. Ruiz, Logic Journal of the IGPL (ISSN 1367-0751), 22(1), 39-65, Oxford University Press, 2014.

• Formalization of a Normalization Theorem in Simplicial Topology, L. Lambán, F.J. Martín, J. Rubio, J.L. Ruiz, Annals of Mathematics and Artificial Intelligence (ISSN 1012-2443), 64(1), 1-37, Kluwer Academic Publishers, 2012.

• Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials, L. Lambán, F.J. Martín, J. Rubio, J.L. Ruiz, Lecture Notes in Computer Science (ISSN 0302-9743), 6898, 200-215, Springer-Verlag, 2011.

• Proof Pearl: A Formal Proof of Higman's Lemma in ACL2, F.J. Martín, J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, Journal of Automated Reasoning (ISSN 0168-7433), 47(3), 229-250, Kluwer Academic Publishers, 2011.

• Topología Simplicial en ACL2, L. Lambán, F.J. Martín, J.L. Ruiz, Contribuciones científicas en honor de Mirian Andrés Gómez (ISBN 978-84-96487-50-5), 1-20, Logroño, España, 2010.

• Expert System to Real Time Control of Machining Processes, F.J. Martín, L.C. González, R. Serrano, Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science) (ISSN 0302-9743), 5988, 281-290, Springer-Verlag, 2010.

• Sistema experto para el control en tiempo real de procesos de mecanizado, F.J. Martín, L.C. González, R. Serrano, Actas de la XIII Conferencia de la Asociación Española para la Inteligencia Artificial (ISBN 978-84-692-6424-9), 1, 477-496, Sevilla, España, 2009.

• Verificación y eficiencia en programas para el cálculo simbólico: estudio de un caso, F.J. Martín, J.L. Ruiz, J. Rubio, L. Lambán, IX Jornadas sobre Programación y Lenguajes (ISBN 978-84-692-4600-9), 1, 7-14, San Sebastián, España, 2009.

• ACL2 verification of simplicial degeneracy programs in the Kenzo system, F.J. Martín, J. Rubio, J.L. Ruiz, Lecture Notes in Artificial Intelligence (ISSN 0302-9743), 5625, 106-121, Springer-Verlag, 2009.

• Architecture for the Optimization of a Machining Process in Real Time through Rule-Based Expert System, R. Serrano, L.C. Gonzalez, F.J. Martín, Third Manufacturing Engineering Society International Conference: MESIC-09, AIP Conference Proceedings (ISSN 0094-243X), 1181, 652-661, American Institute of Physics, 2009.

• Constructing Formally Verified Reasoners for the ALC Description Logic, J.A. Alonso, M.J. Hidalgo, F.J. Martín, J.L. Ruiz, Electronic Notes Theoretical Computer Sciences (ISSN 1571-0661), 200(3), 87-102, Edición electrónica, 2008.

• KRRT: Knowledge Representation & Reasoning Tutor System, J.A. Alonso, G.A. Aranda, F.J. Martín, Lectures Notes in Computer Science (ISSN 0302-9743), 4739, 400-407, Berlín (Alemania), 2007.

• A Formally Verified Prover for the ALC Description Logic, J.A. Alonso, J. Borrego, M.J. Hidalgo, F.J. Martín, J.L. Ruiz, Lecture Notes in Computer Science (ISSN 0302-9743), 4732, 135-150, Springer-Verlag, 2007.

• KRRT: Knowledge Representation \& Reasoning Tutor System, J.A. Alonso, G.A. Aranda, F.J. Martín, Computer Aided Systems Theory (ISBN 978-84-690-3603-7), 400-407, IUCTC Universidad de Las Palmas de Gran Canaria, 2007.

• Sistema experto para la simulación de sistemas tácticos de baloncesto con software libre, M. Palomo, F.J. Martín, Proceedings of the FLOSS International Conference (ISBN 978-84-9828-124-8), 38-51, Servicio de publicaciones de la Universidad de Cádiz, 2007.

• FITS: Formalization with an Intelligent Tutor System, J.A. Alonso, G.A. Aranda, F.J. Martín, Current Developments in Technology-Assisted Education (ISBN 84-690-2472-8), 2, 861-865, FORMATEX, Badajoz, 2006.

• Formal Correctness of a Quadratic Unification Algorithm, J.L. Ruiz, F.J. Martín, J.A. Alonso, M.J. Hidalgo, Journal of Automated Reasoning (ISSN 0168-7433), 37:1-2, 67-92, Kluwer Academic Publishers, Holanda, 2006.

• Foundational challenges in Automated Data and Ontology cleaning in the Semantic Web, J.A. Alonso, J. Borrego, A.M. Chávez, F.J. Martín, IEEE Intelligent Systems (ISSN 1541-1672), 21:1, 42-52, IEEE Computer Society, USA, 2006.

• Proof Pearl: A Formal Proof of Higman's Lemma in ACL2, F.J. Martín, J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, Lecture Notes in Computer Science (ISSN 0302-9743), 3603, 358-372, Springer-Verlag, 2005.

• Rete Algorithm Applied to Robotic Soccer, M. Palomo, F.J. Martín, J.A. Alonso, Lecture Notes in Computer Science (ISSN 0302-9743), 3643, 571-576, Springer-Verlag, 2005.

• Verification of the Formal Concept Analysis, J.A. Alonso, M.J. Hidalgo, F.J. Martín, J.L. Ruiz, Revista de la Real Academia de Ciencias. Serie A: Matemáticas (ISSN 1578-7303), 98, 3-16, Real Academia de Ciencias Exactas, Físicas y Naturales, 2004.

• Formal verification of a generic framework to synthesize SAT-provers, F.J. Martín, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz, Journal of Automated Reasoning (ISSN 0168-7433), 32:4, 287-313, Kluwer Academic Publishers, 2004.

• Formal Verification of Molecular Computational Models in ACL2: A Case Study, F.J. Martín, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz, Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science) (ISSN 0302-9743), 3040, 344-353, Springer-Verlag, 2004.

• Formal Reasoning about Efficient Data Structures: A Case Study in ACL2, J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, Lecture Notes in Computer Science (ISSN 0302-9743), 3018, 75-91, Springer-Verlag, 2004.

• Formal Verification of Molecular Computational Models in ACL2: A Case Study, F.J. Martín, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz, CAEPIA - TTIA 2003 (ISBN 84-8373-564-4), 1, 235-244, Universidad del País Vasco, 2003.

• Termination in ACL2 using multiset relation, J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, Thirty Five Years of Automating Mathematics Applied Logic Series (ISBN 1-4020-1656-5), 28, 217-245, Kluwer Academic Publishers, 2003.

• A Formal Proof of Dickson's Lemma in ACL2, F.J. Martín, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz, Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science) (ISSN 0302-9743), 2850, 49-58, Springer-Verlag, 2003.

• Formal Reasoning About Efficient Data Structures: A Case Study in ACL2, J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, LOPSTR 2003 (Technical Report CW-365), 97-112, Dep. of Computer Science Katholieke Universiteit Leuven, 2003.

• Verification in ACL2 of a generic framework to synthesize SAT-provers, F.J. Martín, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz, Lecture Notes in Computer Science (ISSN 0302-9743), 2664, 182-198, Springer-Verlag, 2003.

• Specification of Adleman's Restricted Model Using An Automated Reasoning System: Verification of Lipton's Experiment, C. Graciani, F.J. Martín, M.J. Pérez, Lecture Notes in Computer Science (ISSN 0302-9743), 2509, 126-136, Springer-Verlag, 2002.

• Formal proofs about rewriting using ACL2, J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, Annals of Mathematics and Artificial Intelligence (ISSN 1012-2443), 36:3, 239-262, Kluwer Academic Publishers, 2002.

• Verifying an Applicative ATP Using Multiset Relations, F.J. Martín, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz, Lecture Notes in Computer Science (ISSN 0302-9743), 2178, 612-626, Springer-Verlag, 2001.

• Formalización del razonamiento ecuacional en una lógica computacional, J.A. Alonso, M.J. Hidalgo, F.J. Martín, J.L. Ruiz, Actas del Encuentro de Matemáticos Andaluces (ISBN 84-472-0290-9), II, 41-50, Secretariado de Publicaciones Universidad de Sevilla, 2001.

• Formalizing Rewriting in the ACL2 Theorem Prover, J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science) (ISSN 0302-9743), 1930, 92-106, Springer-Verlag, 2001.

• Multiset relations: a tool for proving termination, J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, ACL2 Workshop 2000 (Technical Report TR-00-29), Dep. of Computer Sciences Univ. of Texas at Austin, 2000.

• A mechanical proof of Knuth-Bendix critical pair theorem (using ACL2), J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, Proceedings of FTP'2000 (Technical Report 5-2000), 206-216, Fachberichte Informatik Universitat Koblenz-Landau, 2000.

• Verificación automática de sistemas de razonamiento (aplicación a la enseñanza de la Inteligencia Artificial), J.L. Ruiz, F.J. Martín, J.A. Alonso y M.J. Hidalgo, Jornades sobre l'Ensenyament Universitari de la Infomàtica JENUI'98 (ISBN 84-922538-3-5), 297-304, Enginyeria i Arquitectura La Salle, 1998.

• Razonamiento automático en sistemas de representación del conocimiento (y su relación con la enseñanza de la Inteligencia Artificial), F.J. Martín, J.A. Alonso, M.J. Hidalgo y J.L. Ruiz, Jornades sobre l'Ensenyament Universitari de la Infomàtica JENUI'98 (ISBN 84-922538-3-5), 289-296, Enginyeria i Arquitectura La Salle, 1998.

• GTI: Una herramienta de edición de cursos adaptativos, J.J. Arrabal, D. Balbontín, J.A. Alonso, F.F. Lara, F.J. Martín, M.J. Pérez, J.L. Ruiz, Actas del XIII Congreso Nacional de Ingeniería de Proyectos (ISBN 84-88783-30-2), 627-634, Minerva, 1997.

• Razonamiento automático en lógicas polivalentes mediante métodos algebraicos en MAPLE, F.J. Martín, II Congreso de Usuarios de MAPLE. Revista Electrónica de Cálculo Simbólico (ISSN 1139-658X), 3, 52-70, Edición electrónica, 1996.