Investigación - Historial de revisiones

Fmartin: /* Proyectos */

2021-07-12T11:25:08Z

Proyectos

← Revisión anterior		Revisión del 11:25 12 jul 2021
Línea 178:		Línea 178:

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

Fmartin: /* Congresos */

2021-07-12T11:20:33Z

Congresos

← Revisión anterior		Revisión del 11:20 12 jul 2021
Línea 87:		Línea 87:
	== Congresos ==		== 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.		* '''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. 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.		* '''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.		* '''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.

Fmartin: /* Congresos */

2021-07-12T11:17:06Z

Congresos

← Revisión anterior		Revisión del 11:17 12 jul 2021
Línea 90:		Línea 90:

	* '''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.		* '''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 ==		== Proyectos ==

Fmartin: /* Congresos */

2021-07-12T11:04:18Z

Congresos

← Revisión anterior		Revisión del 11:04 12 jul 2021
Línea 86:		Línea 86:

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

	== Proyectos ==		== Proyectos ==

Fmartin: /* Publicaciones */

2021-07-12T10:57:34Z

Publicaciones

← Revisión anterior		Revisión del 10:57 12 jul 2021
Línea 24:		Línea 24:

	* '''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.		* '''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 ==		== Congresos ==

	== Proyectos ==		== Proyectos ==

Fmartin: /* Publicaciones */

2021-07-12T10:41:39Z

Publicaciones

← Revisión anterior		Revisión del 10:41 12 jul 2021
Línea 1:		Línea 1:
	== Publicaciones ==		== 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.		* '''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.		* '''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.		* '''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.

	== Congresos ==		== Congresos ==

	== Proyectos ==		== Proyectos ==

Fmartin: /* Publicaciones */

2021-07-12T10:36:25Z

Publicaciones

← Revisión anterior		Revisión del 10:36 12 jul 2021
Línea 2:		Línea 2:

	* '''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.		* '''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.

	== Congresos ==		== Congresos ==

	== Proyectos ==		== Proyectos ==

Fmartin: /* Publicaciones */

2021-07-12T10:12:37Z

Publicaciones

← Revisión anterior		Revisión del 10:12 12 jul 2021
Línea 1:		Línea 1:
	== Publicaciones ==		== 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.		* '''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 ==		== Congresos ==

	== Proyectos ==		== Proyectos ==

Fmartin en 10:11 12 jul 2021

2021-07-12T10:11:26Z

← Revisión anterior		Revisión del 10:11 12 jul 2021
Línea 2:		Línea 2:

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

Fmartin: /* Publicaciones */

2021-07-12T10:11:01Z

Publicaciones

← Revisión anterior		Revisión del 10:11 12 jul 2021
Línea 1:		Línea 1:
	== 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}~~		* 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.

	== Proyectos ==		== Proyectos ==