Francisco J. Martín Mateos - Contribuciones del usuario [es]

Docencia

2021-07-12T11:55:52Z

Fmartin: /* Titulaciones de Máster */

== Programas de Doctorado ==

* Codirección de la tesis doctoral '''Formalización en Isar de la metalógica de primer orden''' de D. Fabián Fernando Serrano Suárez. La tesis fue defendida en la Universidad de Sevilla el 12 de junio de 2012 obteniendo una calificación de sobresaliente cum Laude por Unanimidad.

== Titulaciones de Máster ==

=== Docencia ===

* '''Representación del Conocimiento y Razonamiento''' del ''Máster Universitario en Ingeniería Biomédica y Salud Digital'' de la Universidad de Sevilla, desde 2019 hasta la actualidad.

* '''Aprendizaje Automático''' del ''Máster Oficial en Ingeniería Informática'' de la Universidad de Sevilla, desde 2018 hasta la actualidad.

* '''Ingeniería del Conocimiento''' del ''Máster Universitario en Lógica, Computación e Inteligencia Artificial'' de la Universidad de Sevilla, desde 2010 hasta la actualidad.

=== Trabajos fin de Máster ===

* '''Aprendizaje por refuerzo en juegos: La plataforma GYM''', Paloma Carrasco Fernández, 2021.
* '''Integración en Web de sistemas basados en conocimiento: El juego de los gatos y el ratón.''', Luis Cristóbal Cedeño Valarezo, 2020.
* '''Integración en Web de sistemas basados en conocimiento: El juego Ratsuk''', Manuel Casas Alaminos, 2019.
* '''Aplicando Deep Forecast a la red de estaciones de Sevici''', Juan Pablo Navarro Sánchez, 2019.
* '''Clasificación de frutas mediante el análisis de imágenes con Deep Learning''', Ana María Prado Machado, 2018.
* '''Sistema experto para la diagnosis y tratamiento de la migraña''', Antonio Sánchez Cabanillas, 2019.
* '''Aprendizaje por refuerzo aplicado a la resolución del Cubo de Rubik''', Camilo Abel Monreal Agüero, 2019.
* '''Sistema experto para la verificación de secuencias de acordes de armonía clásica''', Fernando Reyes Jurado, 2019.
* '''Algoritmos genéticos en CLIPS''', José Luis García Sánchez, 2019.
* '''Sistema experto preparador deportivo''', Miguel Ángel Terrón Morgado, 2017.
* '''Software de soporte para la decisión de cirugía plantar''', Rafael Rodríguez León, 2016.

== Titulaciones de Grado ==

Docencia

2021-07-12T11:42:25Z

Fmartin: /* Titulaciones de Máster */

Docencia

2021-07-12T11:39:34Z

Fmartin: /* Titulaciones de Máster */

Docencia

2021-07-12T11:32:48Z

Fmartin: /* Titulaciones de Máster */

Docencia

2021-07-12T11:31:20Z

Fmartin: /* Titulaciones de Máster */

Docencia

2021-07-12T11:29:50Z

Fmartin: /* Programas de Doctorado */

Docencia

2021-07-12T11:28:19Z

Fmartin:

== Programas de Doctorado ==

== Titulaciones de Máster ==

== Titulaciones de Grado ==

Página principal

2021-07-12T11:26:18Z

Fmartin: /* Docencia */

== [[Investigación]] ==

Líneas de investigación: Razonamiento Automático, Aprendizaje Automático, Inteligencia Artificial

Mi trabajo como investigador se enmarca de forma general dentro la Lógica Computacional, entendida como la aplicación de la Lógica a las Ciencias de la Computación e Inteligencia Artificial, y en particular en el campo del Razonamiento Automático: aplicación de sistemas de razonamiento automático para la formalización y verificación de propiedades de sistemas software, hardware y teorías matemáticas.

== [[Docencia]] ==

Mi actividad docente se desarrolla en las titulaciones de Grado en Informática, Grado en Matemáticas, Máster Universitario en Lógica Computacional e Inteligencia Artificial, Máster Oficial en Ingeniería Informática, Máster Universitario en Ingeniería Biomédica y Salud Digital y Programa de Doctorado en Ciencias de la Computación e Inteligencia Artificial.

Investigación

2021-07-12T11:25:08Z

Fmartin: /* Proyectos */

== 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.

== Congresos ==

* '''Using Abstract Stobjs in ACL2 to compute Matrix Normal Forms''', L. Lambán, F.J. Martín Mateos, J. Rubio, J.L. Ruiz. En ''Interactive Theorem Proving – ITP 2017'', Interactive Theorem Proving - Eighth International Conference, pp. 354-370, Brasilia, 2017.

* '''Certified Symbolic Manipulation: Bivariate Simplicial Polynomials''', L. Lambán, F.J. Martín Mateos, J. Rubio, J.L. Ruiz. ''International Symposium on Symbolic and Algebraic Computation - ISSAC 2013''. Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation, 243–250, Northeastern University, Boston, USA, 2013.

* '''Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials''', L. Lambán, F.J. Martín-Mateos, J. Rubio, J.L. Ruiz Reina, ''Interactive Theorem Proving - Second International Conference, ITP 2011'', Interactive Theorem Proving - Second International Conference, pp. 200-214, Berg en Dal, The Netherlands, 2011.

* '''Sensorización y Control de un Proceso de Mecanizado Utilizando un Sistema Experto Basado en Reglas''', L.C. González, R. Serrano, F.J. Martín, ''XIV Congreso Internacional de Proyectos de Ingeniería'', XIV Congreso Internacional de Proyectos de Ingeniería, pp 2088-2100, Madrid, 2010.

* '''Expert System for Machining Process Control''', L.C. González, R. Serrano, F.J. Martín, ''Rapid Product Developement Event, RPD 2010'', Rapid Product Developement Event, RPD 2010, Marinha Grande, Açores, Portugal, 2010.

* '''Formalizing Mathematical Abstract Concepts in ACL2''', F.J. Martín, J.L. Ruiz, L. Lambán, ''Algebraic computing, soft computing and program verification'', Castro Urdiales, 2010.

* '''Sistema experto para el control en tiempo real de procesos de mecanizado''', F.J. Martín, ''II Jornadas de Lógica, Computación e Inteligencia Artificial'', Sevilla, 2009.

* '''Sistema experto para el control en tiempo real de procesos de mecanizado''', F.J. Martín, L.C. González, R. Serrano, ''XIII Conferencia de la Asociación Española para la Inteligencia Artificial, CAEPIA-TTIA-09'', Actas de la XIII Conferencia de la Asociación Española para la Inteligencia Artificial, pp 477-486, Sevilla, 2009.

* '''Polinomios simpliciales: una herramienta para la formalización de la Topología Simplicial en ACL2''', F.J. Martín, J.L. Ruiz, L. Lambán, ''Computational Logics and Artificial Intelligence, CLAI 2009'', Computational Logics and Artificial Intelligence, pp 35-45, Sevilla, 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, PROLE 2009'', IX Jornadas sobre Programación y Lenguajes, pp 7-14, San Sebastián, 2009.

* '''ACL2 verification of simplicial degeneracy programs in the Kenzo system''', F.J. Martín, J. Rubio, J.L. Ruiz, ''16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, CALCULEMUS'09'', Intelligent Computer Mathematics, pp 106-121, Ontario (Canadá), 2009.

* '''Arquitectura para la optimización de un proceso de mecanizado en tiempo real mediante un sistema experto''', R. Serrano, L.C. González, F.J. Martín, ''Third Manufacturing Engineering Society International Conference, MESIC-09'', Third Manufacturing Engineering Society International Conference, pp 378-341, Alcoy, 2009.

* '''Constructing Formally Verified Reasoners for the ALC Description Logic''', M.J. Hidalgo, J.A. Alonso, F.J. Martín, J.L. Ruiz, ''Third International Workshop on Automated Specification and Verification of Web Systems, WWV'07'', Proceedings of the 3rd International Workshop on Automated Specification and Verification of Web Systems, pp 87-102, Venecia (Italia), 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, ''Theorem Proving in Higher Order Logics, TPHOLs 2007'', Theorem Proving in Higher Order Logics, pp 135-150, Kaiserslautern (Alemania), 2007.

* '''El sistema de razonamiento automático OTTER''', F.J. Martín, ''Jornadas de Ingeniería y Tecnologías Informáticas, 2007'', Cádiz, 2007.

* '''Sistema Experto para la Simulación de Sistemas Tácticos de Baloncesto con Software Libre''', M. Palomo, F.J. Martín, ''Free/Libre/Open Source Systems International Conference, FLOSS 2007'', Free/Libre/Open Source Systems International Conference, FLOSS 2007, Jérez de la Frontera, 2007.

* '''KRRT: Knowledge Representation \& Reasoning Tutor System''', J.A. Alonso, G.A. Aranda, F.J. Martín, ''Computer Aided Systems Theory, EUROCAST 2007'', Computer Aided Systems Theory, EUROCAST 2007, pp 280-283, Las Palmas de Gran Canaria, 2007.

* '''FITS: Formalization with an Intelligent Tutor System''', J.A. Alonso, G.A. Aranda, F.J. Martín, ''IV International Conference on Multimedia and Information and Communication Technologies in Education, m-ICTE2006'', Current Developments in Technology-Assisted Education (2006), pp 861-865, Sevilla, 2006.

* '''Verified Computer Algebra in a Computational Logic''', F.J. Martín, ''Mathematics, Algorithms and Proofs, MAP 2006'', Castro Urdiales, 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, ''Theorem Proving in Higher Order Logics, TPHOLs 2005'', Theorem Proving in Higher Order Logics, pp 358-372, Oxford (Gran Bretaña), 2005.

* '''Rete algorithm applied to robotic soccer''', M. Palomo, F.J. Martín, J.A. Alonso, ''Computer Aided Systems Theory, EUROCAST 2005'', Cast and Tools for Robotics, Vehicular and Communication Systems, pp 280-283, Las Palmas de Gran Canaria, 2005.

* '''A Formally Verified Proof (in PVS) of the Strong Completeness Theorem of Propositional SLD-resolution''', J.A. Alonso, M.J. Hidalgo, F.J. Martín, J.L. Ruiz, ''Computer Aided Systems Theory, EUROCAST 2005'', Cast and Tools for Robotics, Vehicular and Communication Systems, pp 83-86, Las Palmas de Gran Canaria, 2005.

* '''A Formally Verified Quadratic Unification Algorithm''', J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, ''ACL2 Workshop 2004'', ACL2 Workshop 2004 Proceedings, Austin, TX (Estados Unidos), 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, ''Conferencia de la Asociación Española para la Inteligencia Artificial, CAEPIA 2003'', CAEPIA - TTIA 2003, Volumen 1, pp 235-240, San Sebastián, 2003.

* '''A Formal Proof of Dickson's Lemma in ACL2''', F.J. Martín, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz, ''International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2003'', Logic for Programming, Artificial Intelligence, and Reasoning, pp 49-58, Almaty (Kazakhstan), 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, ''International Workshop on Logic Based Program Synthesis and Transformation, LOPSTR 2003'', Preproceedings of the International Workshop on Logic Based Program Synthesis and Transformation, pp 97-112, Uppsala (Suecia), 2003.

* '''Verificación formal y eficiencia: un caso de estudio aplicado a la unificación de términos''', J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, ''I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, IDEIA 2002'', Actas del I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, pp 77-90, Sevilla, 2002.

* '''Una introducción al Análisis Formal de Conceptos en PVS''', J.A. Alonso, J. Borrego, M.J. Hidalgo, F.J. Martín, J.L. Ruiz, ''I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, IDEIA 2002'', Actas del I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, pp 33-46, Sevilla, 2002.

* '''Desarrollo formal y verificación de sistemas proposicionales''', F.J. Martín, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz, ''I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, IDEIA 2002'', Actas del I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, pp 1-12, Sevilla, 2002.

* '''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, ''International Conference on Unconventional Models of Computation, UMC 2002)'', Proceedings of the Third International Conference on Unconventional Models of Computation, pp 126-136, Kobe (Japón), 2002.

* '''Verification in ACL2 of a generic framework to synthesize SAT-provers''', F.J. Martín, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz, ''International Workshop on Logic Based Program Development and Transformation, LOPSTR 2002'', Preproceedings of the International Workshop on Logic Based Program Development and Transformation, pp 182-197, Madrid, 2002.

* '''A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory''', F.J. Martín, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz, ''ACL2 Workshop 2002'', Third Intl. Workshop on the ACL2 Theorem Prover and its Applications, pp 188-203, Grenoble (Francia), 2002.

* '''Molecular Computation Models in ACL2: a Simulation of Lipton's Experiment Solving SAT''', F.J. Martín, J.A. Alonso, M.J. Pérez, F. Sancho, ''ACL2 Workshop 2002'', Third Intl. Workshop on the ACL2 Theorem Prover and its Applications, pp 175-187, Grenoble (Francia), 2002.

* '''Progress Report: Term Dags Using Stobjs''', J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, ''ACL2 Workshop 2002'', Third Intl. Workshop on the ACL2 Theorem Prover and its Applications, pp 101-108, Grenoble (Francia), 2002.

* '''A Theory About First-order Terms in ACL2''', J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, ''ACL2 Workshop 2002'', Third Intl. Workshop on the ACL2 Theorem Prover and its Applications, pp 78-100, Grenoble (Francia), 2002.

* '''Verifying an applicative ATP using multiset relations''', F.J. Martín, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz, ''Computer Aided Systems Theory, EUROCAST 2001'', Computer Aided Systems Theory, EUROCAST 2001, pp 616-626, Las Palmas de Gran Canaria, 2001.

* '''Formalización del razonamiento ecuacional en una lógica computacional''', J.A. Alonso, M.J. Hidalgo, F.J. Martín, J.L. Ruiz, ''Encuentro de Matemáticos Andaluces'', Actas del Encuentro de Matemáticos Andaluces, Volumen II, pp 41-50, Sevilla, 2000.

* '''Formalizing rewriting in the ACL2 theorem prover''', J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, ''Int. Conference on Artificial Intelligence and Symbolic Computation, AISC 2000'', Artificial Intelligence and Symbolic Computation, AISC 2000, Revised Papers, pp 92-106, Madrid, 2000.

* '''Multiset relations: a tool for proving termination''', J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, ''ACL2 Workshop 2000'', ACL2 Workshop 2000 Proceedings, Austin, TX (Estados Unidos), 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, ''Third International Workshop on First order Theorem Proving, FTP 2000'', FTP'2000 Third International Workshop on First order Theorem Proving, pp 206-216, St. Andrews (Escocia), 2000.

* '''Mechanical verification of a rule-based unification algorithm in the Boyer-Moore theorem prover''', J.L. Ruiz, F.J. Martín, J.A. Alonso y M.J. Hidalgo, ''Joint Conference on Declarative Programming, AGP 1999'', Conference on Declarative Programming, AGP-99, pp 289-304, L'Aquila (Italia), 1999.

* '''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, ''IV Jornades sobre l'Ensenyament Universitari de la Infomàtica, JENUI 1998'', IV Jornades sobre l'Ensenyament Universitari de la Infomàtica, JENUI 1998, pp 297-304, Sant Julià de Lòria (Andorra), 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, ''IV Jornades sobre l'Ensenyament Universitari de la Infomàtica, JENUI 1998'', IV Jornades sobre l'Ensenyament Universitari de la Infomàtica, JENUI 1998, pp 289-296, Sant Julià de Lòria (Andorra), 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, ''XIII Congreso Nacional de Ingeniería de Proyectos'', Actas del XIII Congreso Nacional de Ingeniería de Proyectos, pp 627-634, Sevilla, 1997.

* '''Razonamiento automático en lógicas polivalentes mediante métodos algebraicos en MAPLE''', F.J. Martín, ''II Congreso de Usuarios de MAPLE'', Actas del II Congreso de Usuarios de MAPLE, Sevilla, 1996.

== Proyectos ==

* '''Lógica computacional para la ciencia del dato'''. Entidad financiadora: Programa Estatal de Fomento de la Investigación Cientifica y Técnica de Excelencia. TIN2013-41086-P. Duración: del 1 de enero de 2014 al 31 de diciembre de 2016. Investigador principal: Joaquín Borrego Díaz.

* '''Gestión mecanizada del conocimiento matemático. Los casos de la topología algebraica y la lógica'''. Entidad financiadora: Ministerio de Ciencia e Innovación. MTM2009-13842-C02-01. Duración: del 1 de enero de 2011 al 31 de diciembre de 2012. Investigador principal: Julio Rubio García.

* '''Informe técnico sobre aplicabilidad de sistemas basados en el conocimiento al proyecto SOLEME'''. Entidad financiadora: Clever S.L, FIDETIA P025-11/E19. Duración: del 1 de enero de 2011 al 30 de mayo de 2011. Investigador Principal: Francisco J. Martín Mateos.

* '''Gestión mecanizada del conocimiento matemático. Aplicaciones en lógica'''. Entidad financiadora: Ministerio de Ciencia e Innovación. MTM2009-13842-C02-02. Duración: del 1 de enero de 2010 al 31 de diciembre de 2010. Investigador principal: José Luis Ruiz Reina.

* '''Realización del estudio del arte para el proyecto Evaprex'''. Entidad financiadora: Instituto Andaluz de Tecnología, FIDETIA P029-08/E19. Duración: del 20 de septiembre de 2008 al 15 de octubre de 2008. Investigador Principal: Francisco J. Martín Mateos.

* '''Investigación de los factores críticos de los procesos de fabricación básicos del sector aeronáutico andaluz, Sensor-IA'''. Entidad financiadora: Instituto Andaluz de Tecnología, FIDETIA P044-07/E19. Duración: del 5 de octubre de 2007 al 16 de junio de 2008. Investigador Principal: Francisco J. Martín Mateos.

* '''Sistemas verificados para razonamiento en la web semántica'''. Entidad financiadora: Ministerio de Ciencia y Tecnología. TIN2004-03884. Duración: del 28 de diciembre de 2004 al 27 de diciembre de 2007. Investigador principal: José A. Alonso Jiménez.

* '''Desarrollo y verificación formal de sistemas de razonamiento'''. Entidad financiadora: Ministerio de Educación. DGI TIC2000-1368-C03-02. Duración: del 28 de diciembre de 2000 al 27 de diciembre de 2003. Investigador principal: José A. Alonso Jiménez.

Investigación

2021-07-12T11:20:33Z

Fmartin: /* Congresos */

Investigación

2021-07-12T11:17:06Z

Fmartin: /* Congresos */

== 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.

== Congresos ==

* '''Using Abstract Stobjs in ACL2 to compute Matrix Normal Forms''', L. Lambán, F.J. Martín Mateos, J. Rubio, J.L. Ruiz. En ''Interactive Theorem Proving – ITP 2017''. Lecture Notes in Computer Science (ISSN 0302-9743) 10499, 354–370, Springer, 2017.

* '''Certified Symbolic Manipulation: Bivariate Simplicial Polynomials''', L. Lambán, F.J. Martín Mateos, J. Rubio, J.L. Ruiz. En ''International Symposium on Symbolic and Algebraic Computation - ISSAC 2013''. Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation, 243–250, Northeastern University, Boston, USA.

* '''Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials''', L. Lambán, F.J. Martín-Mateos, J. Rubio, J.L. Ruiz Reina, ''Interactive Theorem Proving - Second International Conference, ITP 2011'', Interactive Theorem Proving - Second International Conference, pp. 200-214, Berg en Dal, The Netherlands, 2011.

* '''Sensorización y Control de un Proceso de Mecanizado Utilizando un Sistema Experto Basado en Reglas''', L.C. González, R. Serrano, F.J. Martín, ''XIV Congreso Internacional de Proyectos de Ingeniería'', XIV Congreso Internacional de Proyectos de Ingeniería, pp 2088-2100, Madrid, 2010.

* '''Expert System for Machining Process Control''', L.C. González, R. Serrano, F.J. Martín, ''Rapid Product Developement Event, RPD 2010'', Rapid Product Developement Event, RPD 2010, Marinha Grande, Açores, Portugal, 2010.

* '''Formalizing Mathematical Abstract Concepts in ACL2''', F.J. Martín, J.L. Ruiz, L. Lambán, ''Algebraic computing, soft computing and program verification'', Castro Urdiales, 2010.

* '''Sistema experto para el control en tiempo real de procesos de mecanizado''', F.J. Martín, ''II Jornadas de Lógica, Computación e Inteligencia Artificial'', Sevilla, 2009.

* '''Sistema experto para el control en tiempo real de procesos de mecanizado''', F.J. Martín, L.C. González, R. Serrano, ''XIII Conferencia de la Asociación Española para la Inteligencia Artificial, CAEPIA-TTIA-09'', Actas de la XIII Conferencia de la Asociación Española para la Inteligencia Artificial, pp 477-486, Sevilla, 2009.

* '''Polinomios simpliciales: una herramienta para la formalización de la Topología Simplicial en ACL2''', F.J. Martín, J.L. Ruiz, L. Lambán, ''Computational Logics and Artificial Intelligence, CLAI 2009'', Computational Logics and Artificial Intelligence, pp 35-45, Sevilla, 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, PROLE 2009'', IX Jornadas sobre Programación y Lenguajes, pp 7-14, San Sebastián, 2009.

* '''ACL2 verification of simplicial degeneracy programs in the Kenzo system''', F.J. Martín, J. Rubio, J.L. Ruiz, ''16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, CALCULEMUS'09'', Intelligent Computer Mathematics, pp 106-121, Ontario (Canadá), 2009.

* '''Arquitectura para la optimización de un proceso de mecanizado en tiempo real mediante un sistema experto''', R. Serrano, L.C. González, F.J. Martín, ''Third Manufacturing Engineering Society International Conference, MESIC-09'', Third Manufacturing Engineering Society International Conference, pp 378-341, Alcoy, 2009.

* '''Constructing Formally Verified Reasoners for the ALC Description Logic''', M.J. Hidalgo, J.A. Alonso, F.J. Martín, J.L. Ruiz, ''Third International Workshop on Automated Specification and Verification of Web Systems, WWV'07'', Proceedings of the 3rd International Workshop on Automated Specification and Verification of Web Systems, pp 87-102, Venecia (Italia), 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, ''Theorem Proving in Higher Order Logics, TPHOLs 2007'', Theorem Proving in Higher Order Logics, pp 135-150, Kaiserslautern (Alemania), 2007.

* '''El sistema de razonamiento automático OTTER''', F.J. Martín, ''Jornadas de Ingeniería y Tecnologías Informáticas, 2007'', Cádiz, 2007.

* '''Sistema Experto para la Simulación de Sistemas Tácticos de Baloncesto con Software Libre''', M. Palomo, F.J. Martín, ''Free/Libre/Open Source Systems International Conference, FLOSS 2007'', Free/Libre/Open Source Systems International Conference, FLOSS 2007, Jérez de la Frontera, 2007.

* '''KRRT: Knowledge Representation \& Reasoning Tutor System''', J.A. Alonso, G.A. Aranda, F.J. Martín, ''Computer Aided Systems Theory, EUROCAST 2007'', Computer Aided Systems Theory, EUROCAST 2007, pp 280-283, Las Palmas de Gran Canaria, 2007.

* '''FITS: Formalization with an Intelligent Tutor System''', J.A. Alonso, G.A. Aranda, F.J. Martín, ''IV International Conference on Multimedia and Information and Communication Technologies in Education, m-ICTE2006'', Current Developments in Technology-Assisted Education (2006), pp 861-865, Sevilla, 2006.

* '''Verified Computer Algebra in a Computational Logic''', F.J. Martín, ''Mathematics, Algorithms and Proofs, MAP 2006'', Castro Urdiales, 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, ''Theorem Proving in Higher Order Logics, TPHOLs 2005'', Theorem Proving in Higher Order Logics, pp 358-372, Oxford (Gran Bretaña), 2005.

* '''Rete algorithm applied to robotic soccer''', M. Palomo, F.J. Martín, J.A. Alonso, ''Computer Aided Systems Theory, EUROCAST 2005'', Cast and Tools for Robotics, Vehicular and Communication Systems, pp 280-283, Las Palmas de Gran Canaria, 2005.

* '''A Formally Verified Proof (in PVS) of the Strong Completeness Theorem of Propositional SLD-resolution''', J.A. Alonso, M.J. Hidalgo, F.J. Martín, J.L. Ruiz, ''Computer Aided Systems Theory, EUROCAST 2005'', Cast and Tools for Robotics, Vehicular and Communication Systems, pp 83-86, Las Palmas de Gran Canaria, 2005.

* '''A Formally Verified Quadratic Unification Algorithm''', J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, ''ACL2 Workshop 2004'', ACL2 Workshop 2004 Proceedings, Austin, TX (Estados Unidos), 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, ''Conferencia de la Asociación Española para la Inteligencia Artificial, CAEPIA 2003'', CAEPIA - TTIA 2003, Volumen 1, pp 235-240, San Sebastián, 2003.

* '''A Formal Proof of Dickson's Lemma in ACL2''', F.J. Martín, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz, ''International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2003'', Logic for Programming, Artificial Intelligence, and Reasoning, pp 49-58, Almaty (Kazakhstan), 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, ''International Workshop on Logic Based Program Synthesis and Transformation, LOPSTR 2003'', Preproceedings of the International Workshop on Logic Based Program Synthesis and Transformation, pp 97-112, Uppsala (Suecia), 2003.

* '''Verificación formal y eficiencia: un caso de estudio aplicado a la unificación de términos''', J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, ''I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, IDEIA 2002'', Actas del I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, pp 77-90, Sevilla, 2002.

* '''Una introducción al Análisis Formal de Conceptos en PVS''', J.A. Alonso, J. Borrego, M.J. Hidalgo, F.J. Martín, J.L. Ruiz, ''I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, IDEIA 2002'', Actas del I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, pp 33-46, Sevilla, 2002.

* '''Desarrollo formal y verificación de sistemas proposicionales''', F.J. Martín, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz, ''I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, IDEIA 2002'', Actas del I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, pp 1-12, Sevilla, 2002.

* '''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, ''International Conference on Unconventional Models of Computation, UMC 2002)'', Proceedings of the Third International Conference on Unconventional Models of Computation, pp 126-136, Kobe (Japón), 2002.

* '''Verification in ACL2 of a generic framework to synthesize SAT-provers''', F.J. Martín, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz, ''International Workshop on Logic Based Program Development and Transformation, LOPSTR 2002'', Preproceedings of the International Workshop on Logic Based Program Development and Transformation, pp 182-197, Madrid, 2002.

* '''A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory''', F.J. Martín, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz, ''ACL2 Workshop 2002'', Third Intl. Workshop on the ACL2 Theorem Prover and its Applications, pp 188-203, Grenoble (Francia), 2002.

* '''Molecular Computation Models in ACL2: a Simulation of Lipton's Experiment Solving SAT''', F.J. Martín, J.A. Alonso, M.J. Pérez, F. Sancho, ''ACL2 Workshop 2002'', Third Intl. Workshop on the ACL2 Theorem Prover and its Applications, pp 175-187, Grenoble (Francia), 2002.

* '''Progress Report: Term Dags Using Stobjs''', J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, ''ACL2 Workshop 2002'', Third Intl. Workshop on the ACL2 Theorem Prover and its Applications, pp 101-108, Grenoble (Francia), 2002.

* '''A Theory About First-order Terms in ACL2''', J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, ''ACL2 Workshop 2002'', Third Intl. Workshop on the ACL2 Theorem Prover and its Applications, pp 78-100, Grenoble (Francia), 2002.

* '''Verifying an applicative ATP using multiset relations''', F.J. Martín, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz, ''Computer Aided Systems Theory, EUROCAST 2001'', Computer Aided Systems Theory, EUROCAST 2001, pp 616-626, Las Palmas de Gran Canaria, 2001.

* '''Formalización del razonamiento ecuacional en una lógica computacional''', J.A. Alonso, M.J. Hidalgo, F.J. Martín, J.L. Ruiz, ''Encuentro de Matemáticos Andaluces'', Actas del Encuentro de Matemáticos Andaluces, Volumen II, pp 41-50, Sevilla, 2000.

* '''Formalizing rewriting in the ACL2 theorem prover''', J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, ''Int. Conference on Artificial Intelligence and Symbolic Computation, AISC 2000'', Artificial Intelligence and Symbolic Computation, AISC 2000, Revised Papers, pp 92-106, Madrid, 2000.

* '''Multiset relations: a tool for proving termination''', J.L. Ruiz, J.A. Alonso, M.J. Hidalgo, F.J. Martín, ''ACL2 Workshop 2000'', ACL2 Workshop 2000 Proceedings, Austin, TX (Estados Unidos), 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, ''Third International Workshop on First order Theorem Proving, FTP 2000'', FTP'2000 Third International Workshop on First order Theorem Proving, pp 206-216, St. Andrews (Escocia), 2000.

* '''Mechanical verification of a rule-based unification algorithm in the Boyer-Moore theorem prover''', J.L. Ruiz, F.J. Martín, J.A. Alonso y M.J. Hidalgo, ''Joint Conference on Declarative Programming, AGP 1999'', Conference on Declarative Programming, AGP-99, pp 289-304, L'Aquila (Italia), 1999.

* '''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, ''IV Jornades sobre l'Ensenyament Universitari de la Infomàtica, JENUI 1998'', IV Jornades sobre l'Ensenyament Universitari de la Infomàtica, JENUI 1998, pp 297-304, Sant Julià de Lòria (Andorra), 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, ''IV Jornades sobre l'Ensenyament Universitari de la Infomàtica, JENUI 1998'', IV Jornades sobre l'Ensenyament Universitari de la Infomàtica, JENUI 1998, pp 289-296, Sant Julià de Lòria (Andorra), 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, ''XIII Congreso Nacional de Ingeniería de Proyectos'', Actas del XIII Congreso Nacional de Ingeniería de Proyectos, pp 627-634, Sevilla, 1997.

* '''Razonamiento automático en lógicas polivalentes mediante métodos algebraicos en MAPLE''', F.J. Martín, ''II Congreso de Usuarios de MAPLE'', Actas del II Congreso de Usuarios de MAPLE, Sevilla, 1996.

== Proyectos ==

Investigación

2021-07-12T11:04:18Z

Fmartin: /* Congresos */

Investigación

2021-07-12T10:57:34Z

Fmartin: /* Publicaciones */

Investigación

2021-07-12T10:41:39Z

Fmartin: /* Publicaciones */

Investigación

2021-07-12T10:36:25Z

Fmartin: /* Publicaciones */

Investigación

2021-07-12T10:12:37Z

Fmartin: /* Publicaciones */

Investigación

2021-07-12T10:11:26Z

Fmartin:

== 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.

== Congresos ==

== Proyectos ==

Investigación

2021-07-12T10:11:01Z

Fmartin: /* Publicaciones */

Investigación

2021-07-12T10:09:18Z

Fmartin: /* Publicaciones */

== Publicaciones ==

* {J. Heras, F.J. Martín Mateos, V. Pascual} {Modelling Algebraic Structures and Morphisms in ACL2} {Applicable Algebra in Engineering, Communication and Computing (ISSN 0938-1279)} {Pendiente}{Pendiente}{Springer}{2015}{A}

== Proyectos ==

Investigación

2021-07-12T10:07:10Z

Fmartin: Página creada con «== Publicaciones == == Proyectos ==»

== Publicaciones ==

== Proyectos ==

Página principal

2021-07-12T10:06:22Z

Fmartin: /* Investigación */

Página principal

2021-07-12T10:05:07Z

Fmartin: /* Investigación */

== [[Investigación]] ==

Mi trabajo como investigador se enmarca de forma general dentro la Lógica Computacional, entendida como la aplicación de la Lógica a las Ciencias de la Computación e Inteligencia Artificial, y en particular en el campo del Razonamiento Automático: aplicación de sistemas de razonamiento automático para la formalización y verificación de propiedades de sistemas software, hardware y teorías matemáticas.

== [[Docencia]] ==

Mi actividad docente se desarrolla en las titulaciones de Grado en Informática, Grado en Matemáticas, Máster Universitario en Lógica Computacional e Inteligencia Artificial, Máster Oficial en Ingeniería Informática, Máster Universitario en Ingeniería Biomédica y Salud Digital

Página principal

2021-07-12T10:04:15Z

Fmartin: /* Docencia */

== [[Investigación]] ==

Mi trabajo como investigador se enmarca de forma general dentro la "Lógica Computacional", entendida como la aplicación de la Lógica a las Ciencias de la Computación e Inteligencia Artificial, y en particular en el campo del "Razonamiento Automático": aplicación de sistemas de razonamiento automático para la formalización y verificación de propiedades de sistemas software, hardware y teorías matemáticas.

== [[Docencia]] ==

Mi actividad docente se desarrolla en las titulaciones de Grado en Informática, Grado en Matemáticas, Máster Universitario en Lógica Computacional e Inteligencia Artificial, Máster Oficial en Ingeniería Informática, Máster Universitario en Ingeniería Biomédica y Salud Digital

Página principal

2021-07-12T10:01:49Z

Fmartin:

Docencia

2021-07-12T09:48:12Z

Fmartin: Página creada con «== Curso 2020/2021 == * Ingeniería del Conocimiento»

== Curso 2020/2021 ==
* Ingeniería del Conocimiento

Página principal

2021-07-12T09:47:32Z

Fmartin:

== [[Docencia]] ==
== [[Investigación]] ==

Página principal

2021-07-12T09:47:21Z

Fmartin: /* Investigación */

== [[Docencia]] ==
Asignaturas impartidas durante los últimos años

== [[Investigación]] ==

Página principal

2021-07-12T09:46:50Z

Fmartin: /* Docencia */

== [[Docencia]] ==
Asignaturas impartidas durante los últimos años

== Investigación ==
Líneas de investigación y publicaciones

Página principal

2021-07-12T09:43:41Z

Fmartin: /* [Docencia] */

== Docencia ==
Asignaturas impartidas durante los últimos años

== Investigación ==
Líneas de investigación y publicaciones

Página principal

2021-07-12T09:43:24Z

Fmartin: /* Docencia */

== [Docencia] ==
Asignaturas impartidas durante los últimos años

== Investigación ==
Líneas de investigación y publicaciones

Página principal

2021-07-12T09:42:59Z

Fmartin:

== Docencia ==
Asignaturas impartidas durante los últimos años
== Investigación ==
Líneas de investigación y publicaciones

Página principal

2021-07-12T09:35:17Z

Fmartin:

== Docencia ==
Asignaturas impartidas durante los últimos años

== Investigación ==
== Primeros pasos ==
* [https://www.mediawiki.org/wiki/Special:MyLanguage/Manual:Configuration_settings Lista de ajustes de configuración]
* [https://www.mediawiki.org/wiki/Special:MyLanguage/Manual:FAQ Preguntas frecuentes sobre MediaWiki]
* [https://lists.wikimedia.org/mailman/listinfo/mediawiki-announce Lista de correo de anuncios de publicación de MediaWiki]
* [https://www.mediawiki.org/wiki/Special:MyLanguage/Localisation#Translation_resources Traducir MediaWiki a tu idioma]
* [https://www.mediawiki.org/wiki/Special:MyLanguage/Manual:Combating_spam Aprende a combatir el spam en tu wiki]

Página principal

2021-07-12T09:16:53Z

Fmartin: /* Docencia */

<strong>MediaWiki se ha instalado.</strong>

Consulta la [https://www.mediawiki.org/wiki/Special:MyLanguage/Help:Contents guía] para obtener información sobre el uso del software wiki.

== Docencia ==
Asignaturas impartidas durante los últimos años

== Investigación ==
== Primeros pasos ==
* [https://www.mediawiki.org/wiki/Special:MyLanguage/Manual:Configuration_settings Lista de ajustes de configuración]
* [https://www.mediawiki.org/wiki/Special:MyLanguage/Manual:FAQ Preguntas frecuentes sobre MediaWiki]
* [https://lists.wikimedia.org/mailman/listinfo/mediawiki-announce Lista de correo de anuncios de publicación de MediaWiki]
* [https://www.mediawiki.org/wiki/Special:MyLanguage/Localisation#Translation_resources Traducir MediaWiki a tu idioma]
* [https://www.mediawiki.org/wiki/Special:MyLanguage/Manual:Combating_spam Aprende a combatir el spam en tu wiki]

Página principal

2021-07-12T09:13:34Z

Fmartin: /* Primeros pasos */

<strong>MediaWiki se ha instalado.</strong>

Consulta la [https://www.mediawiki.org/wiki/Special:MyLanguage/Help:Contents guía] para obtener información sobre el uso del software wiki.

== Docencia ==
== Investigación ==
== Primeros pasos ==
* [https://www.mediawiki.org/wiki/Special:MyLanguage/Manual:Configuration_settings Lista de ajustes de configuración]
* [https://www.mediawiki.org/wiki/Special:MyLanguage/Manual:FAQ Preguntas frecuentes sobre MediaWiki]
* [https://lists.wikimedia.org/mailman/listinfo/mediawiki-announce Lista de correo de anuncios de publicación de MediaWiki]
* [https://www.mediawiki.org/wiki/Special:MyLanguage/Localisation#Translation_resources Traducir MediaWiki a tu idioma]
* [https://www.mediawiki.org/wiki/Special:MyLanguage/Manual:Combating_spam Aprende a combatir el spam en tu wiki]