https://www.glc.us.es/web/api.php?action=feedcontributions&feedformat=atom&user=WikiSysop 2026-07-18T00:58:01Z Contribuciones del usuario MediaWiki 1.31.0 https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=1297 2020-02-27T10:47:12Z

<p>WikiSysop: </p> <hr /> <div>* the CLG Wiki<br /> ** mainpage|Home<br /> ** Group members|People<br /> ** Projects|Projects<br /> ** Publications|Publications<br /> ** Theories|Theories<br /> ** Tecnologías|Technologies<br /> ** Related courses|Teaching<br /> ** Seminario de Lógica y Computación|Seminar<br /> ** Lecturas|Readings<br /> ** Enlaces|Links<br /> ** recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Seminario_de_L%C3%B3gica_y_Computaci%C3%B3n&diff=1296 2020-02-27T10:44:48Z

<p>WikiSysop: /* Seminario del 4 de marzo de 2020 */</p> <hr /> <div>Los Seminarios de Lógica y Computación se celebrarán en el seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial. Las sesiones son abiertas y pueden acudir todas las personas interesadas. <br /> <br /> == Próximas sesiones del seminario ==<br /> <br /> === &lt;span id=&quot;4-marzo-20&quot;&gt;Seminario del 4 de marzo de 2020&lt;/span&gt; ===<br /> * &#039;&#039;&#039;Título:&#039;&#039;&#039; &#039;&#039;Como decíamos ayer&#039;&#039;<br /> * &#039;&#039;&#039;Ponente:&#039;&#039;&#039; {{jalonso}} (Grupo de Lógica Computacional - Universidad de Huelva). <br /> * &#039;&#039;&#039;Lugar:&#039;&#039;&#039; Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.<br /> * &#039;&#039;&#039;Hora:&#039;&#039;&#039; De 11:30 a 12:30.<br /> * &#039;&#039;&#039;Resumen:&#039;&#039;&#039; Se comentarán los objetivos de la nueva fase del Seminario y sus precedentes.<br /> <br /> == Sesiones anteriores ==<br /> <br /> Las sesiones de años anteriores se encuentran [[Seminario del Grupo de Lógica Computacional|aquí]].</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Seminario_de_L%C3%B3gica_y_Computaci%C3%B3n&diff=1295 2020-02-27T10:44:35Z

<p>WikiSysop: </p> <hr /> <div>Los Seminarios de Lógica y Computación se celebrarán en el seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial. Las sesiones son abiertas y pueden acudir todas las personas interesadas. <br /> <br /> == Próximas sesiones del seminario ==<br /> <br /> === &lt;span id=&quot;4-marzo-20&quot;&gt;Seminario del 4 de marzo de 2020&lt;/span&gt; ===<br /> * &#039;&#039;&#039;Título:&#039;&#039;&#039; &#039;&#039;Como decíamos ayer&#039;&#039;<br /> * &#039;&#039;&#039;Ponente:&#039;&#039;&#039; {{garanda}} (Grupo de Lógica Computacional - Universidad de Huelva). <br /> * &#039;&#039;&#039;Lugar:&#039;&#039;&#039; Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.<br /> * &#039;&#039;&#039;Hora:&#039;&#039;&#039; De 11:30 a 12:30.<br /> * &#039;&#039;&#039;Resumen:&#039;&#039;&#039; Se comentarán los objetivos de la nueva fase del Seminario y sus precedentes.<br /> <br /> == Sesiones anteriores ==<br /> <br /> Las sesiones de años anteriores se encuentran [[Seminario del Grupo de Lógica Computacional|aquí]].</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Seminario_de_L%C3%B3gica_y_Computaci%C3%B3n&diff=1294 2020-02-27T10:40:13Z

<p>WikiSysop: Página creada con « == Sesiones anteriores == Las sesiones de años anteriores se encuentran aquí.»</p> <hr /> <div><br /> == Sesiones anteriores ==<br /> <br /> Las sesiones de años anteriores se encuentran [[Seminario del Grupo de Lógica Computacional|aquí]].</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=1293 2020-02-27T10:38:27Z

<p>WikiSysop: </p> <hr /> <div>* the CLG Wiki<br /> ** mainpage|Home<br /> ** Group members|People<br /> ** Projects|Projects<br /> ** Publications|Publications<br /> ** Theories|Theories<br /> ** Tecnologías|Technologies<br /> ** Related courses|Teaching<br /> ** Seminario de Lógica y Computación|Seminar<br /> ** Seminario del Grupo de Lógica Computacional|Seminar2<br /> ** Lecturas|Readings<br /> ** Enlaces|Links<br /> ** recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Computational_Logic_Group&diff=345 2008-10-30T07:49:10Z

<p>WikiSysop: </p> <hr /> <div>The research activities of our group in the area of [http://www.cs.miami.edu/~tptp/OverviewOfATP.html automated theorem proving] begun at the end of the eighties, mainly focused on the application of algebraic methods (Gröbner basis) to deduction in multivalued logics.<br /> <br /> In the first half of the nineties, our work was centred around the [http://www-unix.mcs.anl.gov/AR/otter/ OTTER] theorem prover, [http://rewriting.loria.fr/ term rewriting systems] and [http://www.afm.sbu.ac.uk/logic-prog/ logic programming].<br /> <br /> In the second half of the nineties, we started to apply algebraic methods to the [http://www.csd.abdn.ac.uk/~apreece/Research/KQpage.html verification of knowledge-based systems]. In 1997, we begun our project to apply [http://www.afm.sbu.ac.uk/ formal methods] to the verification of [http://www-formal.stanford.edu/clt/ARS/systems.html reasoning systems]. Using [http://www.cs.utexas.edu/users/moore/acl2/ ACL2] we have developed a number of basic [[Theories|computational theories]] for automated deduction.<br /> <br /> Currently, the group is formed by seven [[Group members|members]]. Our main research interests are:<br /> * the study of techniques allowing to increase the efficiency of the algorithms of the computational theories previously developed,<br /> * the application of the techniques developed to the verification, with the [http://pvs.csl.sri.com/ PVS] verification system, of other intelligent systems (like [http://www.upriss.org.uk/fca/fca.html formal concept analysis]), and<br /> * the study of the validation of knowledge bases in complex ontologies and its applications to the [http://www.semanticweb.org/ Semantic Web]. <br /> <br /> During all these years, the group has been involved in several [[Projects|research projects]] with public financial support. At the same time, [[Related courses|education in Computational Logic]] has been one of our major concerns.</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Computational_Logic_Group&diff=344 2008-10-30T07:48:29Z

<p>WikiSysop: </p> <hr /> <div>&lt;meta name=&quot;verify-v1&quot; content=&quot;jnLuGK1oMQMoc9awiDMsOPpV1F0uY8aZhBj31ZftfzM=&quot; /&gt;<br /> The research activities of our group in the area of [http://www.cs.miami.edu/~tptp/OverviewOfATP.html automated theorem proving] begun at the end of the eighties, mainly focused on the application of algebraic methods (Gröbner basis) to deduction in multivalued logics.<br /> <br /> In the first half of the nineties, our work was centred around the [http://www-unix.mcs.anl.gov/AR/otter/ OTTER] theorem prover, [http://rewriting.loria.fr/ term rewriting systems] and [http://www.afm.sbu.ac.uk/logic-prog/ logic programming].<br /> <br /> In the second half of the nineties, we started to apply algebraic methods to the [http://www.csd.abdn.ac.uk/~apreece/Research/KQpage.html verification of knowledge-based systems]. In 1997, we begun our project to apply [http://www.afm.sbu.ac.uk/ formal methods] to the verification of [http://www-formal.stanford.edu/clt/ARS/systems.html reasoning systems]. Using [http://www.cs.utexas.edu/users/moore/acl2/ ACL2] we have developed a number of basic [[Theories|computational theories]] for automated deduction.<br /> <br /> Currently, the group is formed by seven [[Group members|members]]. Our main research interests are:<br /> * the study of techniques allowing to increase the efficiency of the algorithms of the computational theories previously developed,<br /> * the application of the techniques developed to the verification, with the [http://pvs.csl.sri.com/ PVS] verification system, of other intelligent systems (like [http://www.upriss.org.uk/fca/fca.html formal concept analysis]), and<br /> * the study of the validation of knowledge bases in complex ontologies and its applications to the [http://www.semanticweb.org/ Semantic Web]. <br /> <br /> During all these years, the group has been involved in several [[Projects|research projects]] with public financial support. At the same time, [[Related courses|education in Computational Logic]] has been one of our major concerns.</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Lecturas&diff=238 2008-10-27T08:26:02Z

<p>WikiSysop: </p> <hr /> <div>En esta sección se recogen los comentarios de los miembros del Grupo de algunas de las lecturas de publicaciones relacionadas con los temas de investigación del Grupo. <br /> # K.R. Apt y M.G. Wallace &#039;&#039;&#039;[[Constraint Logic Programming using Eclipse]]&#039;&#039;&#039;.<br /> # J. Harrison &#039;&#039;&#039;[[A short survey of automated reasoning]]&#039;&#039;&#039;<br /> # C.E. Veni Madhavan &#039;&#039;&#039;[[Mathematics and computer science: The interplay]]&#039;&#039;&#039;<br /> <br /> [[Category:Lecturas]]</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=215 2008-10-24T07:16:48Z

<p>WikiSysop: </p> <hr /> <div>* the CLG Wiki<br /> ** mainpage|Home<br /> ** Group members|People<br /> ** Projects|Projects<br /> ** Publications|Publications<br /> ** Theories|Theories<br /> ** Tecnologías|Technologies<br /> ** Related courses|Teaching<br /> ** Seminario del Grupo de Lógica Computacional|Seminar<br /> ** Lecturas|Readings<br /> ** Enlaces|Links<br /> ** recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=157 2008-10-22T06:35:54Z

<p>WikiSysop: </p> <hr /> <div>* the CLG Wiki<br /> ** mainpage|Home<br /> ** Group members|People<br /> ** Projects|Projects<br /> ** Publications|Publications<br /> ** Theories|Theories<br /> ** Tecnologías|Technologies<br /> ** Related courses|Teaching<br /> ** Seminario del Grupo de Lógica Computacional|Seminar<br /> ** Lecturas|Readings<br /> ** recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=145 2008-10-19T16:32:50Z

<p>WikiSysop: </p> <hr /> <div>* the CLG Wiki<br /> ** mainpage|Home<br /> ** Group members|People<br /> ** Projects|Projects<br /> ** Publications|Publications<br /> ** Theories|Theories<br /> ** Seminario del Grupo de Lógica Computacional|Seminar<br /> ** Tecnologías|Technologies<br /> ** Related courses|Teaching<br /> ** recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=58 2008-04-25T05:21:55Z

<p>WikiSysop: </p> <hr /> <div>* the CLG Wiki<br /> ** mainpage|Home<br /> ** Group members|People<br /> ** Projects|Projects<br /> ** Publications|Publications<br /> ** Theories|Theories<br /> ** Seminario del Grupo de Lógica Computacional|Seminar<br /> ** Related courses|Teaching<br /> ** recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=42 2008-04-16T16:39:56Z

<p>WikiSysop: </p> <hr /> <div>* the CLG Wiki<br /> ** mainpage|Home<br /> ** Group members|People<br /> ** Projects|Projects<br /> ** Publications|Publications<br /> ** Theories|Theories<br /> ** Related courses|Teaching<br /> ** recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=41 2008-04-16T16:39:16Z

<p>WikiSysop: </p> <hr /> <div>*<br /> ** mainpage|Home<br /> ** Group members|People<br /> ** Projects|Projects<br /> ** Publications|Publications<br /> ** Theories|Theories<br /> ** Related courses|Teaching<br /> ** recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=40 2008-04-16T16:38:45Z

<p>WikiSysop: </p> <hr /> <div>* CLG Wiki<br /> ** mainpage|Home<br /> ** Group members|People<br /> ** Projects|Projects<br /> ** Publications|Publications<br /> ** Theories|Theories<br /> ** Related courses|Teaching<br /> ** recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=39 2008-04-16T16:37:58Z

<p>WikiSysop: </p> <hr /> <div>*<br /> ** mainpage|Home<br /> ** Group members|People<br /> ** Projects|Projects<br /> ** Publications|Publications<br /> ** Theories|Theories<br /> ** Related courses|Teaching<br /> ** recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=38 2008-04-16T16:37:25Z

<p>WikiSysop: </p> <hr /> <div>* mainpage|Home<br /> * Group members|People<br /> * Projects|Projects<br /> * Publications|Publications<br /> * Theories|Theories<br /> * Related courses|Teaching<br /> * recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=37 2008-04-16T16:36:54Z

<p>WikiSysop: </p> <hr /> <div>** mainpage|Home<br /> ** Group members|People<br /> ** Projects|Projects<br /> ** Publications|Publications<br /> ** Theories|Theories<br /> ** Related courses|Teaching<br /> ** recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=36 2008-04-16T06:24:38Z

<p>WikiSysop: </p> <hr /> <div>* navigation<br /> ** mainpage|Home<br /> ** Group members|People<br /> ** Projects|Projects<br /> ** Publications|Publications<br /> ** Theories|Theories<br /> ** Related courses|Teaching<br /> ** recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=35 2008-04-16T05:59:00Z

<p>WikiSysop: </p> <hr /> <div>* navigation<br /> ** mainpage|Home<br /> ** Group members|Members<br /> ** Publications|Publications<br /> ** Theories|Theories<br /> ** Projects|Projects<br /> ** Related courses|Teaching<br /> ** recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=34 2008-04-16T05:58:03Z

<p>WikiSysop: </p> <hr /> <div>* navigation<br /> ** mainpage|Home<br /> ** Projects|Projects<br /> ** Group members|Members<br /> ** Publications|Publications<br /> ** Theories|Theories<br /> ** Related courses|Teaching<br /> ** recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Mainpage&diff=32 2008-04-16T05:54:16Z

<p>WikiSysop: New page: Computational Logic Group</p> <hr /> <div>Computational Logic Group</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Theories&diff=31 2008-04-15T19:35:23Z

<p>WikiSysop: /* Theories */</p> <hr /> <div>== Theories ==<br /> * [http://www.cs.us.es/~jruiz/acl2-rewr/ Formalizing equational reasoning and rewriting (using ACL2)]<br /> * [http://www.cs.us.es/~jruiz/acl2-mul/ Multiset relations: a tool for proving termination (in ACL2)]<br /> * [http://www.cs.us.es/~jruiz/acl2-fot/ Reasoning about first-order terms using the ACL2 theorem prover]<br /> * [http://www.cs.us.es/~jruiz/unificacion-dag/ An unification algorithm in ACL2 using dags]<br /> * [http://www.cs.us.es/~fmartin/acl2/gen-sat/ A generic framework for propositional SAT-provers (formalization in ACL2)]<br /> * [http://www.cs.us.es/~fmartin/acl2/dickson/ Formalization and proof of Dickson&#039;s Lemma in ACL2]<br /> <br /> == Resources ==<br /> * [http://www.glc.us.es/~jalonso/apli2/ APLI2] (APLIcación de Ayuda Para Lógica Informática).</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Theories&diff=30 2008-04-15T19:29:56Z

<p>WikiSysop: New page: == Theories == * [http://www.cs.us.es/~jruiz/acl2-rewr/ Formalizing equational reasoning and rewriting (using ACL2)] * [http://www.cs.us.es/~jruiz/acl2-mul/ Multiset relations: a tool for ...</p> <hr /> <div>== Theories ==<br /> * [http://www.cs.us.es/~jruiz/acl2-rewr/ Formalizing equational reasoning and rewriting (using ACL2)]<br /> * [http://www.cs.us.es/~jruiz/acl2-mul/ Multiset relations: a tool for proving termination (in ACL2)]<br /> * [http://www.cs.us.es/~jruiz/acl2-fot/ Reasoning about first-order terms using the ACL2 theorem prover]<br /> * [http://www.cs.us.es/~jruiz/unificacion-dag/ An unification algorithm in ACL2 using dags]<br /> * [http://www.cs.us.es/~fmartin/acl2/tab-prop/ Formalizing properties of propositional logic (using ACL2)]<br /> * [http://www.cs.us.es/~fmartin/acl2/gen-sat/ A generic framework for propositional SAT-provers (formalization in ACL2)]<br /> * [http://www.cs.us.es/~fmartin/acl2/dickson/ Formalization and proof of Dickson&#039;s Lemma in ACL2]<br /> <br /> == Resources ==<br /> * [http://www.glc.us.es/~jalonso/apli2/ APLI2] (APLIcación de Ayuda Para Lógica Informática).</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Related_courses&diff=29 2008-04-15T19:26:06Z

<p>WikiSysop: </p> <hr /> <div>* PhD studies: [http://www.cs.us.es/docencia/doctorado/ Logic, computation and artificial intelligence]<br /> ** Automated Reasoning<br /> ** Synthesis, verification and reasoning on agents<br /> ** Automatic learning<br /> ** Logic programming<br /> ** Formal methods in Computation and Artificial intelligence<br /> <br /> * Computer Science studies:<br /> ** [http://www.cs.us.es/cursos/ia1/ Artificial Intelligence I]<br /> ** [http://www.cs.us.es/cursos/ia2/ Artificial Intelligence II]<br /> ** [http://www.cs.us.es/cursos/sia/ Artificial Intelligence Seminar]<br /> ** [http://www.cs.us.es/cursos/ra/ Automated Reasoning]<br /> ** [http://www.cs.us.es/cursos/pd/ Declarative Programming]<br /> ** [http://www.cs.us.es/cursos/agi/ Intelligent Agents]<br /> ** [http://www.cs.us.es/cursos/lp/ Logic and Programming]<br /> ** [http://www.cs.us.es/cursos/li/ Logic for Computer Science]</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Related_courses&diff=28 2008-04-15T19:21:12Z

<p>WikiSysop: </p> <hr /> <div>* PhD studies: Logic, computation and artificial intelligence<br /> ** Automated Reasoning<br /> ** Synthesis, verification and reasoning on agents<br /> ** Automatic learning<br /> ** Logic programming<br /> ** Formal methods in Computation and Artificial intelligence<br /> <br /> * Expert course: Computer Science and Knowledge Technologies<br /> <br /> * Computer Science studies:<br /> ** Automated Reasoning<br /> ** Intelligent Agents<br /> ** Artificial Intelligence Seminar<br /> ** Artificial Intelligence I<br /> ** Artificial Intelligence II<br /> ** Logic and Programming<br /> ** Declarative Programming<br /> ** Logic for Computer Science</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Related_courses&diff=27 2008-04-15T19:20:17Z

<p>WikiSysop: New page: * PhD studies: Logic, computation and artificial intelligence o Automated Reasoning o Synthesis, verification and reasoning on agents o Automatic learnin...</p> <hr /> <div> * PhD studies: Logic, computation and artificial intelligence<br /> o Automated Reasoning<br /> o Synthesis, verification and reasoning on agents<br /> o Automatic learning<br /> o Logic programming<br /> o Formal methods in Computation and Artificial intelligence<br /> <br /> * Expert course: Computer Science and Knowledge Technologies<br /> <br /> * Computer Science studies:<br /> o Automated Reasoning<br /> o Intelligent Agents<br /> o Artificial Intelligence Seminar<br /> o Artificial Intelligence I<br /> o Artificial Intelligence II<br /> o Logic and Programming<br /> o Declarative Programming<br /> o Logic for Computer Science</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Publications&diff=26 2008-04-15T19:18:41Z

<p>WikiSysop: /* Publicaciones en Revistas */</p> <hr /> <div>== Libros ==<br /> {{jalonso}}, {{jborrego}}: &#039;&#039;Agentes Inteligentes: una Aproximación desde la Lógica Computacional&#039;&#039;. Sevilla, España. Editorial Kronos. 2002. 127. ISBN: 84-86273-59-5<br /> <br /> {{jalonso}}, {{jborrego}}: &#039;&#039;Deducción Automática&#039;&#039;. Sevilla. Editorial Kronos. 2002. 1004. ISBN: 84-86273-58-7<br /> <br /> {{jalonso}}, {{jruiz}}, {{jborrego}}: &#039;&#039;Curso Práctico de Teoría de Conjuntos&#039;&#039;. Sevilla. La Ñ. 1998. 344. ISBN: 84-89524-45-9<br /> <br /> == Capítulos en Libros ==<br /> {{jalonso}}, {{jborrego}}, {{tchavez}}: &#039;&#039;Logic Databases and Inconsistgency Handling. Encyclopedia of Databases Technologies and Applications&#039;&#039;. Hershey (Pennsylvania), Estados Unidos. Idea Group Reference. Vol. 1. 2006. Pag. 336-340. ISBN: 1-59140-560-2<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, Jose Luis Ruiz Reina: &#039;&#039;Formal Verification of Molecular Computational Models in ACL2: a Case Study&#039;&#039;. CAEPIA-TTIA 2003. San Sebastián. Universidad del País Vasco. Vol. 2. 2003. Pag. 235-244. ISBN: 84-8373-564-4<br /> <br /> {{jalonso}}, {{jborrego}}: &#039;&#039;Generalizing Logic Programs Via Subsumption&#039;&#039;. Eurocast 2003 - Cast and Tools for Complexity in Biological, Physical and Engineering Systems (Extended Abstracts). Las Palmas de Gran Canaria, España. Iuctc Universidad de las Palmas de Gran Canaria. Vol. 1. 2003. Pag. 185-188. ISBN: 84-688-0820-2<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Termination in ACL2 Using Multiset Relation.&#039;&#039; Thirty Five Years of Automating Mathematics. Dordrecht, Holanda. Kluwer Academic Publishers. 2003. Pag. 217-245. ISBN: 1-4020-1656-5<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}, J.D. Navarro: &#039;&#039;A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases.&#039;&#039; IECON 2002. Sevilla, España. IEEE Industrial Electronic Society. 2002. Pag. 1806-1811. ISBN: 0-7803-7475-4<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}: &#039;&#039;Deducción Automática en Anillos Ternarios: Algunos Métodos de Procesamiento del Conocimiento Matemático.&#039;&#039; Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 23-32. ISBN: 84-472-0290-9<br /> <br /> {{jalonso}}, {{mjoseh}}, {{jruiz}}, {{fmartin}}: &#039;&#039;Formalización del Razonamiento Ecuacional en una Lógica Computacional.&#039;&#039; Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 41-50. ISBN: 84-472-0290-9<br /> <br /> {{jalonso}}, {{jborrego}}: &#039;&#039;Proximidad Entre Cláusulas en Programación Lógica Inductiva.&#039;&#039; Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 33-40. ISBN: 84-472-0290-9<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}: &#039;&#039;Estrategias para la Demostración Automática de Teoremas.&#039;&#039; Libro de Actas Cinte&#039;00. Cadiz. Servicio de Publicaciones de la Universidad de Cádiz. 2000. Pag. 276-283<br /> <br /> {{jalonso}}, {{jborrego}}: &#039;&#039;Interpretación Reactiva de Sistemas Basados en Conocimiento.&#039;&#039; Actas del IV Congreso Isko España. Granada. 1999. Pag. 187-193. ISBN: 84-699-0289-X<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Razonamiento Automático en Sistemas de Representación del Conocimiento (y su Relación con la Enseñanza de la Inteligencia Artificial).&#039;&#039; IV Jornades Sobre L&#039;ensenyament Universitari de la Informatica (Jenui 98). Barcelona, España. Enginyeria I Arquitectura la Salle. 1998. Pag. 289-296. ISBN: 84-922538-3-5<br /> <br /> J.J. Arrabal, D. Balbontín, {{jalonso}}, F.F. Lara, {{fmartin}}, M.J. Pérez, {{jruiz}}: &#039;&#039;GTI: una Herramienta de Edición de Cursos Adaptativos.&#039;&#039; Actas del XIII Congreso Nacional de Ingeniería de Proyectos. Sevilla. Antonio F. Martin Navarro. 1997. Pag. 627-634. ISBN: 84-88783-30-2<br /> <br /> L. Laita, E. Roanes, {{jalonso}}, E. Briales: &#039;&#039;Verificación Algebraica de SBC Basada en la Lógica Trievaluada, Teoría e Implementación.&#039;&#039; I Jornadas Sobre Inteligencia Artificial, Control y Sistemas Expertos. Madrid, España. Servicio de Publicaciones de la Universidad de Alcala. 1996. Pag. 241-255. ISBN: 84-8138-147-0<br /> <br /> {{jalonso}}, A. Fernández, M.J. Pérez: &#039;&#039;Razonamiento Automático. Lógica Formal : Orígenes, Métodos y Aplicaciones.&#039;&#039; Sevilla. Kronos S.A. 1995. Pag. 189-211. ISBN: 84-88620-56-X<br /> <br /> J.J. Arrabal, {{jalonso}}, A. Fernández, M.J. Pérez: &#039;&#039;Automatización de la Aritmética. Lenguajes Naturales y Lenguajes Formales,&#039;&#039; X. Barcelona. Ppu: Promociones y Publicaciones Universitarias. 1994. Pag. 167-182. ISBN: 84-477-0396-7<br /> <br /> == Publicaciones en Revistas ==<br /> {{jalonso}}, {{jborrego}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: &#039;&#039;A Formally Verified Prover for the ALC Description Logic&#039;&#039;. Lecture Notes in Computer Science. Vol. 4732. 2007. Pag. 135-150<br /> <br /> {{jruiz}}, {{fmartin}}, {{jalonso}}, {{mjoseh}}: &#039;&#039;Formal Correctness of a Quadratic Unification Algorithm.&#039;&#039; Journal of Automated Reasoning. Vol. 37. Núm. 1-2. 2006. Pag. 67-92<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}, {{fmartin}}: &#039;&#039;Foundational Challenges in Automated Semantic Web Data and Ontology Cleaning.&#039;&#039; IEEE Intelligent Systems. Vol. 21. Núm. 1. 2006. Pag. 42-52<br /> <br /> {{fmartin}}, {{jruiz}}, {{jalonso}}, {{mjoseh}}: &#039;&#039;Proof Pearl: a Formal Proof of Higman S Lemma in ACL2.&#039;&#039; Lecture Notes in Computer Science. Vol. 3603. 2005. Pag. 358-372<br /> <br /> M. Palomo, {{jalonso}}, {{fmartin}}: &#039;&#039;Rete Algorithm Applied to Robotic Soccer.&#039;&#039; Lecture Notes in Computer Science. Vol. 3643. 2005. Pag. 571-576<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Formal Reasoning About Efficient Data Structures: a Case Study in ACL2.&#039;&#039; Lecture Notes in Computer Science. Vol. 3018. 2004. Pag. 75-91<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Formal Verification of a Generic Framework to Synthesize SAT-Provers.&#039;&#039; Journal of Automated Reasoning. Vol. 32. Núm. 4. 2004. Pag. 287-313<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Formal Verification of Molecular Computational Models in ACL2: a Case Study.&#039;&#039; Lecture Notes in Computer Science. Vol. 3040. 2004. Pag. 344-353<br /> <br /> {{tchavez}}, {{jborrego}}, {{jalonso}}: &#039;&#039;Ontology Cleaning By Mereotopological Reasoning.&#039;&#039; Proceedings. 2004. Pag. 132-137<br /> <br /> {{jalonso}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: &#039;&#039;Verification of the Formal Concept Analysis.&#039;&#039; RACSAM. Revista de la Real Academia de Ciencias. Serie a: Matemáticas. Vol. 98. 2004. Pag. 3-16<br /> <br /> I. Medina, F. Palomo, {{jalonso}}, {{jruiz}}: &#039;&#039;Verified Computer Algebra in ACL2 (Grobner Bases Computation).&#039;&#039; Lecture Notes in Computer Science. Vol. 3249. 2004. Pag. 171-184<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;A Formal Proof of Dickson&#039;s Lemma in ACL2.&#039;&#039; Lecture Notes in Computer Science. Vol. 2850. 2003. Pag. 49-58<br /> <br /> M.A. Gutiérrez, {{jalonso}}, {{jborrego}}: &#039;&#039;Generalizing Programs Via Subsumption.&#039;&#039; Lecture Notes in Computer Science. Vol. 2809. 2003. Pag. 115-126<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}, M.A. Gutiérrez, J.D. Navarro: &#039;&#039;Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases.&#039;&#039; Lecture Notes in Computer Science. Vol. 2718. 2003. Pag. 789-798<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers.&#039;&#039; Lecture Notes in Computer Science. Vol. 2664. 2003. Pag. 182-198<br /> <br /> M.A. Gutiérrez, {{jalonso}}, {{jborrego}}: &#039;&#039;A Quasi-Metric for Machine Learning.&#039;&#039; Lecture Notes in Computer Science. Vol. 2527. 2002. Pag. 193-203<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Formal Proofs About Rewriting Using ACL2.&#039;&#039; Annals of Mathematics and Artificial Intelligence . Vol. 36. Núm. 3. 2002. Pag. 239-262<br /> <br /> I. Medina, F. Palomo, {{jalonso}}: &#039;&#039;A Certified Polynomial-Based Decision Procedure for Propositional Logic.&#039;&#039; Lecture Notes in Computer Science. Núm. 2152. 2001. Pag. 297-312<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Formalizing Rewriting in the Acl2 Theorem Prover.&#039;&#039; Lecture Notes in Computer Science. Vol. 1930. 2001. Pag. 92-106<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Verifying an Applicative ATP Using Multiset Relations.&#039;&#039; Lecture Notes in Computer Science. Vol. 2178. 2001. Pag. 612-626<br /> <br /> J. Chazarain, A. Riscos, {{jalonso}}, E. Briales: &#039;&#039;Multivalued-Logic and Gröbner Bases With Applications to Modal Logic.&#039;&#039; Journal of Symbolic Computation . Vol. 11. 1991. Pag. 181-194<br /> <br /> == Libros de Actas ==<br /> {{jalonso}}, {{jruiz}}, {{jborrego}}, M. Ojeda: &#039;&#039;IDIA 2002: I Taller Iberoamericano Sobre Deducción Automática e Inteligencia Artificial.&#039;&#039; Sevilla, España. Sevilla, España. Departamento de Ciencias de la Computacion e Inteligencia Artificial. Universidad de Sevilla. 2002<br /> <br /> == Aportaciones a Congresos == <br /> {{jalonso}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: &#039;&#039;A Formally Verified Proof (in PVS) of the Strong Completeness Theorem Of Propositional SLD-Resolution.&#039;&#039; Cast and Tools for Robotics, Vehicular and Communication Systems. Computer Aided Systems Theory, Eurocast 2005 (10). Num. 10. Las Palmas de Gran Canaria, España. Actas del Congreso. 2005. Pag. 83-86<br /> <br /> {{fmartin}}, {{jruiz}}, {{jalonso}}, {{mjoseh}}: &#039;&#039;Proof Pearl: a Formal Proof of Higman&#039;s Lemma in ACL2.&#039;&#039; Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics (18). Num. 18. Oxford, Reino Unido. Springer-Verlag. 2005. Pag. 358-372. ISBN: 3-540-28372-2<br /> <br /> M. Palomo, {{fmartin}}, {{jalonso}}: &#039;&#039;Rete Algorithm Applied to Robotic Soccer.&#039;&#039; Cast and Tools for Robotics, Vehicular and Communication Systems. Computer Aided Systems Theory, Eurocast 2005 (10). Num. 10. Las Palmas de Gran Canaria, España. Actas del Congreso. 2005. Pag. 280-283<br /> <br /> {{jruiz}}, {{fmartin}}, {{jalonso}}, {{mjoseh}}: &#039;&#039;A Formally Verified Quadratic Unification Algorithm.&#039;&#039; Proceedings of the Fifth International Workshop on the Acl2 Theorem Prover and Its Applications (Acl2-2004). Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (Acl2-2004) (5). Num. 5. Austin, Texas, EEUU. Unicersity of Austin. 2004. Pag. 1-32<br /> <br /> {{jalonso}}, {{jborrego}}: &#039;&#039;Generalizing Logic Programs Via Subsumption.&#039;&#039; Computer Aided System Theory - Eurocast 2003: 9th International Workshop on Computer Aided Systems Theory [recurso Electrónico]. International Workshop on Computer Aided Systems Theory. Num. 9. Las Palmas de Gran Canaria. Springer-Verlag. 2004. Pag. 115-126. ISBN: 3-540-20221-8<br /> <br /> {{tchavez}}, {{jalonso}}, {{jborrego}}: &#039;&#039;Ontology Cleaning By Mereotopological Reasoning.&#039;&#039; Database and Expert Systems Applications. Webs 2004. International Workshop on Web Semantics. Webs 2004. (Dexa 2004) (3). Num. 3. Zaragoza, España. IEEE Press. 2004. Pag. 132-137<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}: &#039;&#039;Towards a Tool for Ontology Engineering.&#039;&#039; World Automation Congress: Advances in Robotics, Manufacturing, Automation, Control, Soft Computing, Multimedia, Biomedicine, Image Processing and Financial Engineering. Vol. IV. World Automation Congress (). Sevilla, Spain. Tsi Press. 2004. Pag. 1-100. ISBN: 1-889335-20-7<br /> <br /> I. Medina, F. Palomo, {{jalonso}}, {{jruiz}}: &#039;&#039;Verified Computer Algebra in ACL2 (Gröbner Basis Computation).&#039;&#039; Proceedings of the 7th Int. Conference on Artificial Intelligence and Symbolic Computation (Aisc 2004). 7th Int. Conference on Artificial Intelligence and Symbolic Computation, Aisc 2004 (). Linz, Austria. Springer-Verlag. 2004. Pag. 171-184<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;A Formal Proof of Dickson&#039;s Lemma in ACL2.&#039;&#039; Proceedings of the International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2003. International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (). Almaty, Kazakhstan. Springer-Verlag. 2003. Pag. 49-58<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Formal Reasoning About Efficient Data Structures: a Case Study in ACL2.&#039;&#039; LOPSTR 2003, Preproceedings of the International Symposium of Logic Based Program Synthesis and Transformation. International Workshop on Logic Based Program Synthesis and Transformation (). Uppsala, Suecia. Katholieke Universiteit Leuven, Dep. of Computer Science. 2003. Pag. 97-112<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Formal Verification of Molecular Computational Models in ACL2: a Case Study.&#039;&#039; CAEPIA-TTIA 2003. X Conferencia de la Asocicación Española para la Inteligenciia Artificial. Asociación Española para la Inteligencia Artificial. Conferencia. Num. 10. San Sebastián. Universidad del País Vasco, Servicio Editorial. 2003. Pag. 235-240. ISBN: 84-8373-564-4<br /> <br /> M.A. Gutiérrez, {{jalonso}}, {{jborrego}}: &#039;&#039;Generalizing Logic Programs Via Subsumption.&#039;&#039; Eurocast 2003: Cast and Tools for Complexity in Biological, Physical and Engineering Systems: Extended Abstracts. International Conference on Computer Aided Systems Theory. Num. 9. Las Palmas de Gran Canaria. Universidad de las Palmas de Gran Canaria. 2003. Pag. 185-188. ISBN: 84-688-0820-2<br /> <br /> {{tchavez}}, {{jborrego}}, {{jalonso}}: &#039;&#039;Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases&#039;&#039; (Iea/Aie 2003). Libro de Actas del 16th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (Iea/Aie 2003). Iea/Aie 2003 (). Loughborough, United Kingdom. Springer, Berlín, Alemania. 2003. Pag. 789-798<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;A Generic Instantiation Tool and a Case Study: a Generic Multiset Theory.&#039;&#039; Third International Workshop on the ACL2 Theorem Prover and Its Applications. Third International Workshop on the ACL2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 188-203<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}, J.D. Navarro: &#039;&#039;A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases.&#039;&#039; Proc. of the 28th Annual Conference of IEEE Industrial Electronics Society. The 28th Annual Conference of IEEE Industrial Electronics Society. Sevilla, España. IEEE Press. 2002. Pag. 1806-1811<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}, M.A. Gutiérrez, J.D. Navarro: &#039;&#039;A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases.&#039;&#039; Proceedings of the Iecon&#039;02. Iecon&#039;02 (). Sevilla, España. IEEE Industrial Electronic Society. 2002. Pag. 1806-1811. ISBN: 0-7803-7474-6<br /> <br /> {{jalonso}}, {{jborrego}}: &#039;&#039;A Quasi-Metric for Machine Learning.&#039;&#039; 8th Ibero-American Conference on A.I. Ibero-American Conference on A.I. Num. 8. Sevilla. Springer, Berlín, Alemania. 2002. Pag. 193-203<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;A Theory About First-Order Terms in ACL2.&#039;&#039; Third International Workshop on the ACL2 Theorem Prover and Its Applications. Third International Workshop on the ACL2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 78-100<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Desarrollo Formal y Verificación de Sistemas Proposicionales.&#039;&#039; I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 1-12<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Progress Report: Term Dags Using Stobjs&#039;&#039;. Third International Workshop on the ACL2 Theorem Prover and Its Applications. Third International Workshop on the ACL2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 101-108<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}, M.A. Gutiérrez: &#039;&#039;Towards a Practical Argumentative Reasoning With Qsd.&#039;&#039; I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 111-120<br /> <br /> {{jalonso}}, {{jborrego}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: &#039;&#039;Una Introducción al Análisis Formal de Conceptos en PVS.&#039;&#039; I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 33-46<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Verificación Formal y Eficiencia: un Caso de Estudio Aplicado a la Unificación de Términos.&#039;&#039; I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 77-90<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers.&#039;&#039; Preproceedings of the International Workshop on Logic Based Program Development and Transformation. International Workshop on Logic Based Program Development and Transformation. Madrid, Spain. Facultad de Informática de la Universidad Politécnica de Madrid. 2002. Pag. 182-197<br /> <br /> I. Medina, F. Palomo, {{jalonso}}: &#039;&#039;A Certified Polynomial-Based Decision Procedure for Propositional Logic.&#039;&#039; International Conference on Theorem Proving in Higher Order Logics. International Conference on Theorem Proving in Higher Order Logics (14). Num. 14. Edimburgo (Escocia), Reino Unido. Division of Informatics of Edinburgh University. 2001. Pag. 297-312<br /> <br /> {{jalonso}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: &#039;&#039;Formalización del Razonamiento Ecuacional en una Lógica Computacional.&#039;&#039; Actas del I Encuentro de Matemáticos Andaluces. Encuentro de Matemáticos Andaluces. Num. 1. Sevilla, España. Universidad de Sevilla. Secretariado de Publicaciones. 2001. Pag. 41-50. ISBN: 84-472-0639-4<br /> <br /> {{jalonso}}, {{jborrego}}: &#039;&#039;Proximidad entre cláusulas en Programación Lógica Inductiva.&#039;&#039; Actas del I Encuentro de Matemáticos Andaluces. Encuentro de Matemáticos Andaluces. Num. 1. Sevilla, España. Universidad de Sevilla. Secretariado de Publicaciones. 2001. Pag. 33-40. ISBN: 84-472-0639-4<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Verifying an Applicative ATP Using Multiset Relations.&#039;&#039; Eurocast 2001 Conference. Eurocast 2001 Conference. Las Palmas de Gran Canaria. 0. 2001. Pag. 616-626<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;A Mechanical Proof of Knuth-Bendix Critical Pair Theorem (Using ACL2).&#039;&#039; Proceedings of the Third International Workshop on First-Order Theorem Proving. First-Order Theorem Proving (3). Num. 3. ST Andrews, Scotland. Fachberichte Informatik, Universitat Koblenz-Landau. 2000. Pag. 206-216<br /> <br /> M.A. Gutiérrez, {{jalonso}}, {{jborrego}}: &#039;&#039;A Topological Study of the Upward Refinement Operators on ILP.&#039;&#039; ILP 2000 - Work in Progress Reports. Inductive Logic Programming 10th International Conference, ILP 2000. Londres, Reino Unido. James Cussens - Alan Frisch (Eds.). 2000. Pag. 120-137<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Formalizing Rewriting in the ACL2 Theorem Prover.&#039;&#039; Artificial Intelligence and Symbolic Computation, Aisc 2000, Revised Papers. Int. Conference on Artificial Intelligence and Symbolic Computation (). Madrid, España. Springer-Verlag. 2000. Pag. 92-106<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Multiset Relations: a Tool for Proving Termination.&#039;&#039; Proceedings of the ACL2 Workshop 2000. Second ACL2 Workshop (2). Num. 2. Austin, Texas, EEUU. University of Texas At Austin. 2000. Pag. 82-91<br /> <br /> M.A. Gutiérrez, {{jalonso}}, {{jborrego}}: &#039;&#039;Una Quasi-Metrica Basada en Subsuncion.&#039;&#039; IV Jornadas Cientificas en Tecnologias de la Informacion. Jornadas Cientificas en Tecnologias de la Informacion. Num. 4. Cadiz, España. Servicio de Publicaciones de la Universidad de Cádiz. 2000. Pag. 260-267<br /> <br /> {{jruiz}}, {{fmartin}}, {{jalonso}}, {{mjoseh}}: &#039;&#039;Mechanical Verification of a Rule-Based Unification Algorithm in the Boyer-Moore Theorem Prover.&#039;&#039; Proc. of Joint Conference on Declarative Programming. Joint Conference on Declarative Programming. L&#039;aquila, Italia. 1999. Pag. 289-304<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Razonamiento Automático en Sistemas de Representación del Conocimiento (y su Relación con la Enseñanza de la Inteligencia Artificial).&#039;&#039; IV Jornades Sobre L&#039;ensenyament Universitari de la Infomàtica. IV Jornadas Sobre la Enseñanza Universitaria de la Informatica (Jenui&#039;98) (). Andorra. Enginyeria I Arquitectura la Salle. 1998. Pag. 289-296<br /> <br /> J.J. Arrabal, D. Balbontin, {{jalonso}}, F.F. Lara, {{fmartin}}, M.J. Perez, {{jruiz}}: &#039;&#039;GTI: una Herramienta de Edición de Cursos Adaptativos.&#039;&#039; Actas del XIII Congreso Nacional de Ingenieria de Proyectos. Journees Détudes Comparatives Franco- Hispano- Italiannes. Num. 1. Burdeos, Francia. 1997. Pag. 627-634<br /> <br /> R. Fernández, J.J. Arrabal, {{jalonso}}: &#039;&#039;Hacia una Enseñanza Permanente y Automatizada: WWW y Evaluación Automática con GTI.&#039;&#039; International Congress on Historical Information Systems. International Congress on Historical Information Systems (). Vitoria. 1997. Pag. 1-1<br /> <br /> D. Balbontin, M.L. de la Vega, {{jalonso}}, J.J. Arrabal: &#039;&#039;Aprende Matemáticas.&#039;&#039; Actas del Primer Encuentro de Informática Educativa: Edie. Primer Encuentro de Informática Educativa (Edie) (). Cees (Madrid). Asociacion para el Desarrollo de la Informatica Educativa. 1994. Pag. 20-25<br /> <br /> D. Balbontin, {{jalonso}}, J.J. Arrabal, F.J. Herrera: &#039;&#039;Especificación Formal de Bases de Datos con un Demostrador Automático de Teoremas.&#039;&#039; Actas del II Congreso Nacional de Programación Declarativa. Congreso Nacional de Programación Declarativa. Num. 2. Sin Editorial. 1993. Pag. 343-344<br /> <br /> D. Balbontin, J.J. Arrabal, {{jalonso}}, F.J. Herrera: &#039;&#039;Automated Proofs in Group Theory With OTTER.&#039;&#039; Proceedings of the Fith International Symposium on Knowledge Engineering. Fifth International Symposium on Knowledge Engineering (). Sevilla. Rank-Xerox. 1992. Pag. 326-331<br /> <br /> D. Balbontin, {{jalonso}}, J.J. Arrabal, F.J. Herrera: &#039;&#039;Razonamiento Automático en Lógica de Primer Orden.&#039;&#039; Actas del VIII Congreso de Lenguajes Naturales y Lenguajes Formales. VIII Congreso de Lenguajes Naturales y Lenguajes Formales (). Gerona (España). 1992. Pag. 165-172<br /> <br /> {{jalonso}}, E. Briales, A. Riscos: &#039;&#039;Preuve Automatique Dans Le Calcul Propositionnel et les Logiques Trivalentes.&#039;&#039; Computational Topology and Geometry and Computation in Teaching Mathematics. Computational Topology and Geometry and Computation in Teaching of Mathematics. Num. 1. Sevilla. Servicio de Publicaciones de la Universidad de Sevilla. 1990. Pag. 15-24. ISBN: 84-7405-639-X<br /> <br /> {{jalonso}}, E. Briales: &#039;&#039;Lógicas Polivalentes y Bases de Gröbner.&#039;&#039; V Congreso de Lenguajes Naturales y Lenguajes Formales. Congreso de Lenguajes Naturales y Lenguajes Formales (5). Num. 5. Barcelona, España. Universidad Barcelona. 1989. Pag. 307-315<br /> <br /> == Tesis dirigidas ==<br /> Director: {{jalonso}}, Doctorando: {{mjoseh}}: &#039;&#039;Teoría computacional (en PVS) de la programación lógica y del análisis formal de conceptos&#039;&#039;, 2004, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director: {{jalonso}}, Doctorando: I. Medina: &#039;&#039;Verificación formal en ACL2 del algoritmo de Buchberger&#039;&#039;, 2003, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director: {{jalonso}}, Doctorando: M.A. Gutiérrez: &#039;&#039;Operadores de generalizacion para el aprendizaje clausal&#039;&#039;, 2002, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director: {{jalonso}}, Doctorando: {{fmartin}}: &#039;&#039;Teoría computacional (en ACL2) sobre cálculos proposicionales,&#039;&#039; 2002, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director: {{jalonso}}, Doctorando: {{jruiz}}: &#039;&#039;Una teoría computacional acerca de la lógica ecuacional (Formalización en ACL2 y demostración automática de sus propiedades)&#039;&#039;, 2000, Ciencias de la Computacion e Inteligencia Artificial</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Publications&diff=25 2008-04-15T19:18:01Z

<p>WikiSysop: </p> <hr /> <div>== Libros ==<br /> {{jalonso}}, {{jborrego}}: &#039;&#039;Agentes Inteligentes: una Aproximación desde la Lógica Computacional&#039;&#039;. Sevilla, España. Editorial Kronos. 2002. 127. ISBN: 84-86273-59-5<br /> <br /> {{jalonso}}, {{jborrego}}: &#039;&#039;Deducción Automática&#039;&#039;. Sevilla. Editorial Kronos. 2002. 1004. ISBN: 84-86273-58-7<br /> <br /> {{jalonso}}, {{jruiz}}, {{jborrego}}: &#039;&#039;Curso Práctico de Teoría de Conjuntos&#039;&#039;. Sevilla. La Ñ. 1998. 344. ISBN: 84-89524-45-9<br /> <br /> == Capítulos en Libros ==<br /> {{jalonso}}, {{jborrego}}, {{tchavez}}: &#039;&#039;Logic Databases and Inconsistgency Handling. Encyclopedia of Databases Technologies and Applications&#039;&#039;. Hershey (Pennsylvania), Estados Unidos. Idea Group Reference. Vol. 1. 2006. Pag. 336-340. ISBN: 1-59140-560-2<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, Jose Luis Ruiz Reina: &#039;&#039;Formal Verification of Molecular Computational Models in ACL2: a Case Study&#039;&#039;. CAEPIA-TTIA 2003. San Sebastián. Universidad del País Vasco. Vol. 2. 2003. Pag. 235-244. ISBN: 84-8373-564-4<br /> <br /> {{jalonso}}, {{jborrego}}: &#039;&#039;Generalizing Logic Programs Via Subsumption&#039;&#039;. Eurocast 2003 - Cast and Tools for Complexity in Biological, Physical and Engineering Systems (Extended Abstracts). Las Palmas de Gran Canaria, España. Iuctc Universidad de las Palmas de Gran Canaria. Vol. 1. 2003. Pag. 185-188. ISBN: 84-688-0820-2<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Termination in ACL2 Using Multiset Relation.&#039;&#039; Thirty Five Years of Automating Mathematics. Dordrecht, Holanda. Kluwer Academic Publishers. 2003. Pag. 217-245. ISBN: 1-4020-1656-5<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}, J.D. Navarro: &#039;&#039;A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases.&#039;&#039; IECON 2002. Sevilla, España. IEEE Industrial Electronic Society. 2002. Pag. 1806-1811. ISBN: 0-7803-7475-4<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}: &#039;&#039;Deducción Automática en Anillos Ternarios: Algunos Métodos de Procesamiento del Conocimiento Matemático.&#039;&#039; Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 23-32. ISBN: 84-472-0290-9<br /> <br /> {{jalonso}}, {{mjoseh}}, {{jruiz}}, {{fmartin}}: &#039;&#039;Formalización del Razonamiento Ecuacional en una Lógica Computacional.&#039;&#039; Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 41-50. ISBN: 84-472-0290-9<br /> <br /> {{jalonso}}, {{jborrego}}: &#039;&#039;Proximidad Entre Cláusulas en Programación Lógica Inductiva.&#039;&#039; Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 33-40. ISBN: 84-472-0290-9<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}: &#039;&#039;Estrategias para la Demostración Automática de Teoremas.&#039;&#039; Libro de Actas Cinte&#039;00. Cadiz. Servicio de Publicaciones de la Universidad de Cádiz. 2000. Pag. 276-283<br /> <br /> {{jalonso}}, {{jborrego}}: &#039;&#039;Interpretación Reactiva de Sistemas Basados en Conocimiento.&#039;&#039; Actas del IV Congreso Isko España. Granada. 1999. Pag. 187-193. ISBN: 84-699-0289-X<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Razonamiento Automático en Sistemas de Representación del Conocimiento (y su Relación con la Enseñanza de la Inteligencia Artificial).&#039;&#039; IV Jornades Sobre L&#039;ensenyament Universitari de la Informatica (Jenui 98). Barcelona, España. Enginyeria I Arquitectura la Salle. 1998. Pag. 289-296. ISBN: 84-922538-3-5<br /> <br /> J.J. Arrabal, D. Balbontín, {{jalonso}}, F.F. Lara, {{fmartin}}, M.J. Pérez, {{jruiz}}: &#039;&#039;GTI: una Herramienta de Edición de Cursos Adaptativos.&#039;&#039; Actas del XIII Congreso Nacional de Ingeniería de Proyectos. Sevilla. Antonio F. Martin Navarro. 1997. Pag. 627-634. ISBN: 84-88783-30-2<br /> <br /> L. Laita, E. Roanes, {{jalonso}}, E. Briales: &#039;&#039;Verificación Algebraica de SBC Basada en la Lógica Trievaluada, Teoría e Implementación.&#039;&#039; I Jornadas Sobre Inteligencia Artificial, Control y Sistemas Expertos. Madrid, España. Servicio de Publicaciones de la Universidad de Alcala. 1996. Pag. 241-255. ISBN: 84-8138-147-0<br /> <br /> {{jalonso}}, A. Fernández, M.J. Pérez: &#039;&#039;Razonamiento Automático. Lógica Formal : Orígenes, Métodos y Aplicaciones.&#039;&#039; Sevilla. Kronos S.A. 1995. Pag. 189-211. ISBN: 84-88620-56-X<br /> <br /> J.J. Arrabal, {{jalonso}}, A. Fernández, M.J. Pérez: &#039;&#039;Automatización de la Aritmética. Lenguajes Naturales y Lenguajes Formales,&#039;&#039; X. Barcelona. Ppu: Promociones y Publicaciones Universitarias. 1994. Pag. 167-182. ISBN: 84-477-0396-7<br /> <br /> ================= Publicaciones en Revistas =================<br /> {{jalonso}}, {{jborrego}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: &#039;&#039;A Formally Verified Prover for the ALC Description Logic&#039;&#039;. Lecture Notes in Computer Science. Vol. 4732. 2007. Pag. 135-150<br /> <br /> {{jruiz}}, {{fmartin}}, {{jalonso}}, {{mjoseh}}: &#039;&#039;Formal Correctness of a Quadratic Unification Algorithm.&#039;&#039; Journal of Automated Reasoning. Vol. 37. Núm. 1-2. 2006. Pag. 67-92<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}, {{fmartin}}: &#039;&#039;Foundational Challenges in Automated Semantic Web Data and Ontology Cleaning.&#039;&#039; IEEE Intelligent Systems. Vol. 21. Núm. 1. 2006. Pag. 42-52<br /> <br /> {{fmartin}}, {{jruiz}}, {{jalonso}}, {{mjoseh}}: &#039;&#039;Proof Pearl: a Formal Proof of Higman S Lemma in ACL2.&#039;&#039; Lecture Notes in Computer Science. Vol. 3603. 2005. Pag. 358-372<br /> <br /> M. Palomo, {{jalonso}}, {{fmartin}}: &#039;&#039;Rete Algorithm Applied to Robotic Soccer.&#039;&#039; Lecture Notes in Computer Science. Vol. 3643. 2005. Pag. 571-576<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Formal Reasoning About Efficient Data Structures: a Case Study in ACL2.&#039;&#039; Lecture Notes in Computer Science. Vol. 3018. 2004. Pag. 75-91<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Formal Verification of a Generic Framework to Synthesize SAT-Provers.&#039;&#039; Journal of Automated Reasoning. Vol. 32. Núm. 4. 2004. Pag. 287-313<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Formal Verification of Molecular Computational Models in ACL2: a Case Study.&#039;&#039; Lecture Notes in Computer Science. Vol. 3040. 2004. Pag. 344-353<br /> <br /> {{tchavez}}, {{jborrego}}, {{jalonso}}: &#039;&#039;Ontology Cleaning By Mereotopological Reasoning.&#039;&#039; Proceedings. 2004. Pag. 132-137<br /> <br /> {{jalonso}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: &#039;&#039;Verification of the Formal Concept Analysis.&#039;&#039; RACSAM. Revista de la Real Academia de Ciencias. Serie a: Matemáticas. Vol. 98. 2004. Pag. 3-16<br /> <br /> I. Medina, F. Palomo, {{jalonso}}, {{jruiz}}: &#039;&#039;Verified Computer Algebra in ACL2 (Grobner Bases Computation).&#039;&#039; Lecture Notes in Computer Science. Vol. 3249. 2004. Pag. 171-184<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;A Formal Proof of Dickson&#039;s Lemma in ACL2.&#039;&#039; Lecture Notes in Computer Science. Vol. 2850. 2003. Pag. 49-58<br /> <br /> M.A. Gutiérrez, {{jalonso}}, {{jborrego}}: &#039;&#039;Generalizing Programs Via Subsumption.&#039;&#039; Lecture Notes in Computer Science. Vol. 2809. 2003. Pag. 115-126<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}, M.A. Gutiérrez, J.D. Navarro: &#039;&#039;Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases.&#039;&#039; Lecture Notes in Computer Science. Vol. 2718. 2003. Pag. 789-798<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers.&#039;&#039; Lecture Notes in Computer Science. Vol. 2664. 2003. Pag. 182-198<br /> <br /> M.A. Gutiérrez, {{jalonso}}, {{jborrego}}: &#039;&#039;A Quasi-Metric for Machine Learning.&#039;&#039; Lecture Notes in Computer Science. Vol. 2527. 2002. Pag. 193-203<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Formal Proofs About Rewriting Using ACL2.&#039;&#039; Annals of Mathematics and Artificial Intelligence . Vol. 36. Núm. 3. 2002. Pag. 239-262<br /> <br /> I. Medina, F. Palomo, {{jalonso}}: &#039;&#039;A Certified Polynomial-Based Decision Procedure for Propositional Logic.&#039;&#039; Lecture Notes in Computer Science. Núm. 2152. 2001. Pag. 297-312<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Formalizing Rewriting in the Acl2 Theorem Prover.&#039;&#039; Lecture Notes in Computer Science. Vol. 1930. 2001. Pag. 92-106<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Verifying an Applicative ATP Using Multiset Relations.&#039;&#039; Lecture Notes in Computer Science. Vol. 2178. 2001. Pag. 612-626<br /> <br /> J. Chazarain, A. Riscos, {{jalonso}}, E. Briales: &#039;&#039;Multivalued-Logic and Gröbner Bases With Applications to Modal Logic.&#039;&#039; Journal of Symbolic Computation . Vol. 11. 1991. Pag. 181-194<br /> <br /> == Libros de Actas ==<br /> {{jalonso}}, {{jruiz}}, {{jborrego}}, M. Ojeda: &#039;&#039;IDIA 2002: I Taller Iberoamericano Sobre Deducción Automática e Inteligencia Artificial.&#039;&#039; Sevilla, España. Sevilla, España. Departamento de Ciencias de la Computacion e Inteligencia Artificial. Universidad de Sevilla. 2002<br /> <br /> == Aportaciones a Congresos == <br /> {{jalonso}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: &#039;&#039;A Formally Verified Proof (in PVS) of the Strong Completeness Theorem Of Propositional SLD-Resolution.&#039;&#039; Cast and Tools for Robotics, Vehicular and Communication Systems. Computer Aided Systems Theory, Eurocast 2005 (10). Num. 10. Las Palmas de Gran Canaria, España. Actas del Congreso. 2005. Pag. 83-86<br /> <br /> {{fmartin}}, {{jruiz}}, {{jalonso}}, {{mjoseh}}: &#039;&#039;Proof Pearl: a Formal Proof of Higman&#039;s Lemma in ACL2.&#039;&#039; Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics (18). Num. 18. Oxford, Reino Unido. Springer-Verlag. 2005. Pag. 358-372. ISBN: 3-540-28372-2<br /> <br /> M. Palomo, {{fmartin}}, {{jalonso}}: &#039;&#039;Rete Algorithm Applied to Robotic Soccer.&#039;&#039; Cast and Tools for Robotics, Vehicular and Communication Systems. Computer Aided Systems Theory, Eurocast 2005 (10). Num. 10. Las Palmas de Gran Canaria, España. Actas del Congreso. 2005. Pag. 280-283<br /> <br /> {{jruiz}}, {{fmartin}}, {{jalonso}}, {{mjoseh}}: &#039;&#039;A Formally Verified Quadratic Unification Algorithm.&#039;&#039; Proceedings of the Fifth International Workshop on the Acl2 Theorem Prover and Its Applications (Acl2-2004). Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (Acl2-2004) (5). Num. 5. Austin, Texas, EEUU. Unicersity of Austin. 2004. Pag. 1-32<br /> <br /> {{jalonso}}, {{jborrego}}: &#039;&#039;Generalizing Logic Programs Via Subsumption.&#039;&#039; Computer Aided System Theory - Eurocast 2003: 9th International Workshop on Computer Aided Systems Theory [recurso Electrónico]. International Workshop on Computer Aided Systems Theory. Num. 9. Las Palmas de Gran Canaria. Springer-Verlag. 2004. Pag. 115-126. ISBN: 3-540-20221-8<br /> <br /> {{tchavez}}, {{jalonso}}, {{jborrego}}: &#039;&#039;Ontology Cleaning By Mereotopological Reasoning.&#039;&#039; Database and Expert Systems Applications. Webs 2004. International Workshop on Web Semantics. Webs 2004. (Dexa 2004) (3). Num. 3. Zaragoza, España. IEEE Press. 2004. Pag. 132-137<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}: &#039;&#039;Towards a Tool for Ontology Engineering.&#039;&#039; World Automation Congress: Advances in Robotics, Manufacturing, Automation, Control, Soft Computing, Multimedia, Biomedicine, Image Processing and Financial Engineering. Vol. IV. World Automation Congress (). Sevilla, Spain. Tsi Press. 2004. Pag. 1-100. ISBN: 1-889335-20-7<br /> <br /> I. Medina, F. Palomo, {{jalonso}}, {{jruiz}}: &#039;&#039;Verified Computer Algebra in ACL2 (Gröbner Basis Computation).&#039;&#039; Proceedings of the 7th Int. Conference on Artificial Intelligence and Symbolic Computation (Aisc 2004). 7th Int. Conference on Artificial Intelligence and Symbolic Computation, Aisc 2004 (). Linz, Austria. Springer-Verlag. 2004. Pag. 171-184<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;A Formal Proof of Dickson&#039;s Lemma in ACL2.&#039;&#039; Proceedings of the International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2003. International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (). Almaty, Kazakhstan. Springer-Verlag. 2003. Pag. 49-58<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Formal Reasoning About Efficient Data Structures: a Case Study in ACL2.&#039;&#039; LOPSTR 2003, Preproceedings of the International Symposium of Logic Based Program Synthesis and Transformation. International Workshop on Logic Based Program Synthesis and Transformation (). Uppsala, Suecia. Katholieke Universiteit Leuven, Dep. of Computer Science. 2003. Pag. 97-112<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Formal Verification of Molecular Computational Models in ACL2: a Case Study.&#039;&#039; CAEPIA-TTIA 2003. X Conferencia de la Asocicación Española para la Inteligenciia Artificial. Asociación Española para la Inteligencia Artificial. Conferencia. Num. 10. San Sebastián. Universidad del País Vasco, Servicio Editorial. 2003. Pag. 235-240. ISBN: 84-8373-564-4<br /> <br /> M.A. Gutiérrez, {{jalonso}}, {{jborrego}}: &#039;&#039;Generalizing Logic Programs Via Subsumption.&#039;&#039; Eurocast 2003: Cast and Tools for Complexity in Biological, Physical and Engineering Systems: Extended Abstracts. International Conference on Computer Aided Systems Theory. Num. 9. Las Palmas de Gran Canaria. Universidad de las Palmas de Gran Canaria. 2003. Pag. 185-188. ISBN: 84-688-0820-2<br /> <br /> {{tchavez}}, {{jborrego}}, {{jalonso}}: &#039;&#039;Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases&#039;&#039; (Iea/Aie 2003). Libro de Actas del 16th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (Iea/Aie 2003). Iea/Aie 2003 (). Loughborough, United Kingdom. Springer, Berlín, Alemania. 2003. Pag. 789-798<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;A Generic Instantiation Tool and a Case Study: a Generic Multiset Theory.&#039;&#039; Third International Workshop on the ACL2 Theorem Prover and Its Applications. Third International Workshop on the ACL2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 188-203<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}, J.D. Navarro: &#039;&#039;A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases.&#039;&#039; Proc. of the 28th Annual Conference of IEEE Industrial Electronics Society. The 28th Annual Conference of IEEE Industrial Electronics Society. Sevilla, España. IEEE Press. 2002. Pag. 1806-1811<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}, M.A. Gutiérrez, J.D. Navarro: &#039;&#039;A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases.&#039;&#039; Proceedings of the Iecon&#039;02. Iecon&#039;02 (). Sevilla, España. IEEE Industrial Electronic Society. 2002. Pag. 1806-1811. ISBN: 0-7803-7474-6<br /> <br /> {{jalonso}}, {{jborrego}}: &#039;&#039;A Quasi-Metric for Machine Learning.&#039;&#039; 8th Ibero-American Conference on A.I. Ibero-American Conference on A.I. Num. 8. Sevilla. Springer, Berlín, Alemania. 2002. Pag. 193-203<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;A Theory About First-Order Terms in ACL2.&#039;&#039; Third International Workshop on the ACL2 Theorem Prover and Its Applications. Third International Workshop on the ACL2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 78-100<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Desarrollo Formal y Verificación de Sistemas Proposicionales.&#039;&#039; I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 1-12<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Progress Report: Term Dags Using Stobjs&#039;&#039;. Third International Workshop on the ACL2 Theorem Prover and Its Applications. Third International Workshop on the ACL2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 101-108<br /> <br /> {{jalonso}}, {{jborrego}}, {{tchavez}}, M.A. Gutiérrez: &#039;&#039;Towards a Practical Argumentative Reasoning With Qsd.&#039;&#039; I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 111-120<br /> <br /> {{jalonso}}, {{jborrego}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: &#039;&#039;Una Introducción al Análisis Formal de Conceptos en PVS.&#039;&#039; I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 33-46<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Verificación Formal y Eficiencia: un Caso de Estudio Aplicado a la Unificación de Términos.&#039;&#039; I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 77-90<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers.&#039;&#039; Preproceedings of the International Workshop on Logic Based Program Development and Transformation. International Workshop on Logic Based Program Development and Transformation. Madrid, Spain. Facultad de Informática de la Universidad Politécnica de Madrid. 2002. Pag. 182-197<br /> <br /> I. Medina, F. Palomo, {{jalonso}}: &#039;&#039;A Certified Polynomial-Based Decision Procedure for Propositional Logic.&#039;&#039; International Conference on Theorem Proving in Higher Order Logics. International Conference on Theorem Proving in Higher Order Logics (14). Num. 14. Edimburgo (Escocia), Reino Unido. Division of Informatics of Edinburgh University. 2001. Pag. 297-312<br /> <br /> {{jalonso}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: &#039;&#039;Formalización del Razonamiento Ecuacional en una Lógica Computacional.&#039;&#039; Actas del I Encuentro de Matemáticos Andaluces. Encuentro de Matemáticos Andaluces. Num. 1. Sevilla, España. Universidad de Sevilla. Secretariado de Publicaciones. 2001. Pag. 41-50. ISBN: 84-472-0639-4<br /> <br /> {{jalonso}}, {{jborrego}}: &#039;&#039;Proximidad entre cláusulas en Programación Lógica Inductiva.&#039;&#039; Actas del I Encuentro de Matemáticos Andaluces. Encuentro de Matemáticos Andaluces. Num. 1. Sevilla, España. Universidad de Sevilla. Secretariado de Publicaciones. 2001. Pag. 33-40. ISBN: 84-472-0639-4<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Verifying an Applicative ATP Using Multiset Relations.&#039;&#039; Eurocast 2001 Conference. Eurocast 2001 Conference. Las Palmas de Gran Canaria. 0. 2001. Pag. 616-626<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;A Mechanical Proof of Knuth-Bendix Critical Pair Theorem (Using ACL2).&#039;&#039; Proceedings of the Third International Workshop on First-Order Theorem Proving. First-Order Theorem Proving (3). Num. 3. ST Andrews, Scotland. Fachberichte Informatik, Universitat Koblenz-Landau. 2000. Pag. 206-216<br /> <br /> M.A. Gutiérrez, {{jalonso}}, {{jborrego}}: &#039;&#039;A Topological Study of the Upward Refinement Operators on ILP.&#039;&#039; ILP 2000 - Work in Progress Reports. Inductive Logic Programming 10th International Conference, ILP 2000. Londres, Reino Unido. James Cussens - Alan Frisch (Eds.). 2000. Pag. 120-137<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Formalizing Rewriting in the ACL2 Theorem Prover.&#039;&#039; Artificial Intelligence and Symbolic Computation, Aisc 2000, Revised Papers. Int. Conference on Artificial Intelligence and Symbolic Computation (). Madrid, España. Springer-Verlag. 2000. Pag. 92-106<br /> <br /> {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: &#039;&#039;Multiset Relations: a Tool for Proving Termination.&#039;&#039; Proceedings of the ACL2 Workshop 2000. Second ACL2 Workshop (2). Num. 2. Austin, Texas, EEUU. University of Texas At Austin. 2000. Pag. 82-91<br /> <br /> M.A. Gutiérrez, {{jalonso}}, {{jborrego}}: &#039;&#039;Una Quasi-Metrica Basada en Subsuncion.&#039;&#039; IV Jornadas Cientificas en Tecnologias de la Informacion. Jornadas Cientificas en Tecnologias de la Informacion. Num. 4. Cadiz, España. Servicio de Publicaciones de la Universidad de Cádiz. 2000. Pag. 260-267<br /> <br /> {{jruiz}}, {{fmartin}}, {{jalonso}}, {{mjoseh}}: &#039;&#039;Mechanical Verification of a Rule-Based Unification Algorithm in the Boyer-Moore Theorem Prover.&#039;&#039; Proc. of Joint Conference on Declarative Programming. Joint Conference on Declarative Programming. L&#039;aquila, Italia. 1999. Pag. 289-304<br /> <br /> {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: &#039;&#039;Razonamiento Automático en Sistemas de Representación del Conocimiento (y su Relación con la Enseñanza de la Inteligencia Artificial).&#039;&#039; IV Jornades Sobre L&#039;ensenyament Universitari de la Infomàtica. IV Jornadas Sobre la Enseñanza Universitaria de la Informatica (Jenui&#039;98) (). Andorra. Enginyeria I Arquitectura la Salle. 1998. Pag. 289-296<br /> <br /> J.J. Arrabal, D. Balbontin, {{jalonso}}, F.F. Lara, {{fmartin}}, M.J. Perez, {{jruiz}}: &#039;&#039;GTI: una Herramienta de Edición de Cursos Adaptativos.&#039;&#039; Actas del XIII Congreso Nacional de Ingenieria de Proyectos. Journees Détudes Comparatives Franco- Hispano- Italiannes. Num. 1. Burdeos, Francia. 1997. Pag. 627-634<br /> <br /> R. Fernández, J.J. Arrabal, {{jalonso}}: &#039;&#039;Hacia una Enseñanza Permanente y Automatizada: WWW y Evaluación Automática con GTI.&#039;&#039; International Congress on Historical Information Systems. International Congress on Historical Information Systems (). Vitoria. 1997. Pag. 1-1<br /> <br /> D. Balbontin, M.L. de la Vega, {{jalonso}}, J.J. Arrabal: &#039;&#039;Aprende Matemáticas.&#039;&#039; Actas del Primer Encuentro de Informática Educativa: Edie. Primer Encuentro de Informática Educativa (Edie) (). Cees (Madrid). Asociacion para el Desarrollo de la Informatica Educativa. 1994. Pag. 20-25<br /> <br /> D. Balbontin, {{jalonso}}, J.J. Arrabal, F.J. Herrera: &#039;&#039;Especificación Formal de Bases de Datos con un Demostrador Automático de Teoremas.&#039;&#039; Actas del II Congreso Nacional de Programación Declarativa. Congreso Nacional de Programación Declarativa. Num. 2. Sin Editorial. 1993. Pag. 343-344<br /> <br /> D. Balbontin, J.J. Arrabal, {{jalonso}}, F.J. Herrera: &#039;&#039;Automated Proofs in Group Theory With OTTER.&#039;&#039; Proceedings of the Fith International Symposium on Knowledge Engineering. Fifth International Symposium on Knowledge Engineering (). Sevilla. Rank-Xerox. 1992. Pag. 326-331<br /> <br /> D. Balbontin, {{jalonso}}, J.J. Arrabal, F.J. Herrera: &#039;&#039;Razonamiento Automático en Lógica de Primer Orden.&#039;&#039; Actas del VIII Congreso de Lenguajes Naturales y Lenguajes Formales. VIII Congreso de Lenguajes Naturales y Lenguajes Formales (). Gerona (España). 1992. Pag. 165-172<br /> <br /> {{jalonso}}, E. Briales, A. Riscos: &#039;&#039;Preuve Automatique Dans Le Calcul Propositionnel et les Logiques Trivalentes.&#039;&#039; Computational Topology and Geometry and Computation in Teaching Mathematics. Computational Topology and Geometry and Computation in Teaching of Mathematics. Num. 1. Sevilla. Servicio de Publicaciones de la Universidad de Sevilla. 1990. Pag. 15-24. ISBN: 84-7405-639-X<br /> <br /> {{jalonso}}, E. Briales: &#039;&#039;Lógicas Polivalentes y Bases de Gröbner.&#039;&#039; V Congreso de Lenguajes Naturales y Lenguajes Formales. Congreso de Lenguajes Naturales y Lenguajes Formales (5). Num. 5. Barcelona, España. Universidad Barcelona. 1989. Pag. 307-315<br /> <br /> == Tesis dirigidas ==<br /> Director: {{jalonso}}, Doctorando: {{mjoseh}}: &#039;&#039;Teoría computacional (en PVS) de la programación lógica y del análisis formal de conceptos&#039;&#039;, 2004, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director: {{jalonso}}, Doctorando: I. Medina: &#039;&#039;Verificación formal en ACL2 del algoritmo de Buchberger&#039;&#039;, 2003, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director: {{jalonso}}, Doctorando: M.A. Gutiérrez: &#039;&#039;Operadores de generalizacion para el aprendizaje clausal&#039;&#039;, 2002, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director: {{jalonso}}, Doctorando: {{fmartin}}: &#039;&#039;Teoría computacional (en ACL2) sobre cálculos proposicionales,&#039;&#039; 2002, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director: {{jalonso}}, Doctorando: {{jruiz}}: &#039;&#039;Una teoría computacional acerca de la lógica ecuacional (Formalización en ACL2 y demostración automática de sus propiedades)&#039;&#039;, 2000, Ciencias de la Computacion e Inteligencia Artificial</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Plantilla:Jruiz&diff=24 2008-04-15T18:43:56Z

<p>WikiSysop: New page: [http://www.cs.us.es/~jruiz/ J.L. Ruiz]</p> <hr /> <div>[http://www.cs.us.es/~jruiz/ J.L. Ruiz]</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Plantilla:Fmartin&diff=23 2008-04-15T18:43:18Z

<p>WikiSysop: New page: [http://www.cs.us.es/~fmartin/ F.J. Martín]</p> <hr /> <div>[http://www.cs.us.es/~fmartin/ F.J. Martín]</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Plantilla:Mjoseh&diff=22 2008-04-15T18:42:33Z

<p>WikiSysop: New page: [http://www.cs.us.es/~mjoseh/ M.J. Hidalgo]</p> <hr /> <div>[http://www.cs.us.es/~mjoseh/ M.J. Hidalgo]</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Plantilla:Tchavez&diff=21 2008-04-15T18:41:54Z

<p>WikiSysop: New page: [http://www.cs.us.es/~tchavez/ A. Chávez]</p> <hr /> <div>[http://www.cs.us.es/~tchavez/ A. Chávez]</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Plantilla:Jborrego&diff=20 2008-04-15T18:41:04Z

<p>WikiSysop: New page: [http://www.cs.us.es/~joaquin/ J, Borrego]</p> <hr /> <div>[http://www.cs.us.es/~joaquin/ J, Borrego]</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Plantilla:Jalonso&diff=19 2008-04-15T18:40:01Z

<p>WikiSysop: </p> <hr /> <div>[http://www.cs.us.es/~jalonso J.A. Alonso]</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Publications&diff=18 2008-04-15T18:39:31Z

<p>WikiSysop: </p> <hr /> <div>== Libros ==<br /> {{jalonso}}, Joaquin Borrego Diaz: &#039;&#039;Agentes Inteligentes: una Aproximación desde la Lógica Computacional&#039;&#039;. Sevilla, España. Editorial Kronos. 2002. 127. ISBN: 84-86273-59-5<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz: &#039;&#039;Deducción Automática&#039;&#039;. Sevilla. Editorial Kronos. 2002. 1004. ISBN: 84-86273-58-7<br /> <br /> {{jalonso}}, Jose Luis Ruiz Reina, Joaquin Borrego Diaz: &#039;&#039;Curso Práctico de Teoría de Conjuntos&#039;&#039;. Sevilla. La Ñ. 1998. 344. ISBN: 84-89524-45-9<br /> <br /> == Capítulos en Libros ==<br /> {{jalonso}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez: &#039;&#039;Logic Databases and Inconsistgency Handling. Encyclopedia of Databases Technologies and Applications&#039;&#039;. Hershey (Pennsylvania), Estados Unidos. Idea Group Reference. Vol. 1. 2006. Pag. 336-340. ISBN: 1-59140-560-2<br /> <br /> Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina: &#039;&#039;Formal Verification of Molecular Computational Models in ACL2: a Case Study&#039;&#039;. CAEPIA-TTIA 2003. San Sebastián. Universidad del País Vasco. Vol. 2. 2003. Pag. 235-244. ISBN: 84-8373-564-4<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz: &#039;&#039;Generalizing Logic Programs Via Subsumption&#039;&#039;. Eurocast 2003 - Cast and Tools for Complexity in Biological, Physical and Engineering Systems (Extended Abstracts). Las Palmas de Gran Canaria, España. Iuctc Universidad de las Palmas de Gran Canaria. Vol. 1. 2003. Pag. 185-188. ISBN: 84-688-0820-2<br /> <br /> Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: &#039;&#039;Termination in ACL2 Using Multiset Relation.&#039;&#039; Thirty Five Years of Automating Mathematics. Dordrecht, Holanda. Kluwer Academic Publishers. 2003. Pag. 217-245. ISBN: 1-4020-1656-5<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Jorge D. Navarro Marín: &#039;&#039;A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases.&#039;&#039; IECON 2002. Sevilla, España. IEEE Industrial Electronic Society. 2002. Pag. 1806-1811. ISBN: 0-7803-7475-4<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez:<br /> Deduccion Automatica en Anillos Ternarios: Algunos Métodos de Procesamiento del Conocimiento Matemático. Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 23-32. ISBN: 84-472-0290-9<br /> <br /> {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos:<br /> Formalización del Razonamiento Ecuacional en una Lógica Computacional. Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 41-50. ISBN: 84-472-0290-9<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz:<br /> Proximidad Entre Clausulas en Programacion Logica Inductiva. Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 33-40. ISBN: 84-472-0290-9<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez: &#039;&#039;Estrategias para la Demostración Automática de Teoremas.&#039;&#039; Libro de Actas Cinte&#039;00. Cadiz. Servicio de Publicaciones de la Universidad de Cádiz. 2000. Pag. 276-283<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz: &#039;&#039;Interpretación Reactiva de Sistemas Basados en Conocimiento.&#039;&#039; Actas del IV Congreso Isko España. Granada. 1999. Pag. 187-193. ISBN: 84-699-0289-X<br /> <br /> Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina: &#039;&#039;Razonamiento Automático en Sistemas de Representación del Conocimiento (y su Relación con la Enseñanza de la Inteligencia Artificial).&#039;&#039; IV Jornades Sobre L&#039;ensenyament Universitari de la Informatica (Jenui 98). Barcelona, España. Enginyeria I Arquitectura la Salle. 1998. Pag. 289-296. ISBN: 84-922538-3-5<br /> <br /> Juan Jose Arrabal Parrilla, Delia Balbontin Noval, {{jalonso}}, Francisco Felix Lara Martin, Francisco Jesus Martin Mateos, Mario Jesus Perez Jimenez, Jose Luis Ruiz Reina: &#039;&#039;GTI: una Herramienta de Edición de Cursos Adaptativos.&#039;&#039; Actas del XIII Congreso Nacional de Ingeniería de Proyectos. Sevilla. Antonio F. Martin Navarro. 1997. Pag. 627-634. ISBN: 84-88783-30-2<br /> <br /> Luis Laita, Eugenio Roanes-Lozano, {{jalonso}}, Emilio Briales Morales: &#039;&#039;Verificación Algebraica de SBC Basada en la Lógica Trievaluada, Teoría e Implementación.&#039;&#039; I Jornadas Sobre Inteligencia Artificial, Control y Sistemas Expertos. Madrid, España. Servicio de Publicaciones de la Universidad de Alcala. 1996. Pag. 241-255. ISBN: 84-8138-147-0<br /> <br /> {{jalonso}}, Alejandro Fernandez Margarit, Mario Jesus Perez Jimenez: &#039;&#039;Razonamiento Automático. Lógica Formal : Orígenes, Métodos y Aplicaciones.&#039;&#039; Sevilla. Kronos S.A. 1995. Pag. 189-211. ISBN: 84-88620-56-X<br /> <br /> Juan Jose Arrabal Parrilla, {{jalonso}}, Alejandro Fernandez Margarit, Mario Jesus Perez Jimenez: &#039;&#039;Automatización de la Aritmética. Lenguajes Naturales y Lenguajes Formales,&#039;&#039; X. Barcelona. Ppu: Promociones y Publicaciones Universitarias. 1994. Pag. 167-182. ISBN: 84-477-0396-7<br /> <br /> == Publicaciones en Revistas ==<br /> {{jalonso}}, Joaquin Borrego Diaz, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina: &#039;&#039;A Formally Verified Prover for the ALC Description Logic&#039;&#039;. Lecture Notes in Computer Science. Vol. 4732. 2007. Pag. 135-150<br /> <br /> Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado: &#039;&#039;Formal Correctness of a Quadratic Unification Algorithm.&#039;&#039; Journal of Automated Reasoning. Vol. 37. Núm. 1-2. 2006. Pag. 67-92<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Francisco Jesus Martin Mateos: &#039;&#039;Foundational Challenges in Automated Semantic Web Data and Ontology Cleaning.&#039;&#039; IEEE Intelligent Systems. Vol. 21. Núm. 1. 2006. Pag. 42-52<br /> <br /> Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado: &#039;&#039;Proof Pearl: a Formal Proof of Higman S Lemma in ACL2.&#039;&#039; Lecture Notes in Computer Science. Vol. 3603. 2005. Pag. 358-372<br /> <br /> Manuel Palomo Duarte, {{jalonso}}, Francisco Jesus Martin Mateos: &#039;&#039;Rete Algorithm Applied to Robotic Soccer.&#039;&#039; Lecture Notes in Computer Science. Vol. 3643. 2005. Pag. 571-576<br /> <br /> Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: &#039;&#039;Formal Reasoning About Efficient Data Structures: a Case Study in ACL2.&#039;&#039; Lecture Notes in Computer Science. Vol. 3018. 2004. Pag. 75-91<br /> <br /> Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina: &#039;&#039;Formal Verification of a Generic Framework to Synthesize SAT-Provers.&#039;&#039; Journal of Automated Reasoning. Vol. 32. Núm. 4. 2004. Pag. 287-313<br /> <br /> Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Formal Verification of Molecular Computational Models in Acl2: a Case Study. Lecture Notes in Computer Science. Vol. 3040. 2004. Pag. 344-353<br /> <br /> Antonia Mª Chavez Gonzalez, Joaquin Borrego Diaz, {{jalonso}}:<br /> Ontology Cleaning By Mereotopological Reasoning. Proceedings. 2004. Pag. 132-137<br /> <br /> {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> Verification of the Formal Concept Analysis. RACSAM. Revista de la Real Academia de Ciencias. Serie a: Matemáticas. Vol. 98. 2004. Pag. 3-16<br /> <br /> Inmaculada Medina Bulo, Francisco Palomo Lozano, {{jalonso}}, Jose Luis Ruiz Reina:<br /> Verified Computer Algebra in Acl2 (Grobner Bases Computation). Lecture Notes in Computer Science. Vol. 3249. 2004. Pag. 171-184<br /> <br /> Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> A Formal Proof of Dickson&#039;s Lemma in Acl2. Lecture Notes in Computer Science. Vol. 2850. 2003. Pag. 49-58<br /> <br /> Miguel Angel Gutierrez Naranjo, {{jalonso}}, Joaquin Borrego Diaz:<br /> Generalizing Programs Via Subsumption. Lecture Notes in Computer Science. Vol. 2809. 2003. Pag. 115-126<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo, Jorge D. Navarro Marín:<br /> Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases. Lecture Notes in Computer Science. Vol. 2718. 2003. Pag. 789-798<br /> <br /> Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Verification in Acl2 of a Generic Framework to Synthesize SAT-Provers. Lecture Notes in Computer Science. Vol. 2664. 2003. Pag. 182-198<br /> <br /> Miguel Angel Gutierrez Naranjo, {{jalonso}}, Joaquin Borrego Diaz:<br /> A Quasi-Metric for Machine Learning. Lecture Notes in Computer Science. Vol. 2527. 2002. Pag. 193-203<br /> <br /> Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formal Proofs About Rewriting Using Acl2. Annals of Mathematics and Artificial Intelligence . Vol. 36. Núm. 3. 2002. Pag. 239-262<br /> <br /> Inmaculada Medina Bulo, Francisco Palomo Lozano, {{jalonso}}:<br /> A Certified Polynomial-Based Decision Procedure for Propositional Logic. Lecture Notes in Computer Science. Núm. 2152. 2001. Pag. 297-312<br /> <br /> Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formalizing Rewriting in the Acl2 Theorem Prover. Lecture Notes in Computer Science. Vol. 1930. 2001. Pag. 92-106<br /> <br /> Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Verifying an Applicative ATP Using Multiset Relations. Lecture Notes in Computer Science. Vol. 2178. 2001. Pag. 612-626<br /> <br /> J. Chazarain, Agustin Riscos, {{jalonso}}, Emilio Briales Morales:<br /> Multivalued-Logic and Gröbner Bases With Applications to Modal Logic. Journal of Symbolic Computation . Vol. 11. 1991. Pag. 181-194<br /> <br /> Libros de Actas<br /> {{jalonso}}, Jose Luis Ruiz Reina, Joaquin Borrego Diaz, Manuel Ojeda Aciego:<br /> Ideia 2002: I Taller Iberoamericano Sobre Deducción Automática e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Sevilla, España. Departamento de Ciencias de la Computacion e Inteligencia Artificial. Universidad de Sevilla. 2002<br /> <br /> Aportaciones a Congresos<br /> {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> A Formally Verified Proof (in PVS) of the Strong Completeness Theorem Of Propositional Sld-Resolution. Cast and Tools for Robotics, Vehicular and Communication Systems. Computer Aided Systems Theory, Eurocast 2005 (10). Num. 10. Las Palmas de Gran Canaria, España. Actas del Congreso. 2005. Pag. 83-86<br /> <br /> Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado:<br /> Proof Pearl: a Formal Proof of Higman&#039;s Lemma in Acl2. Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics (18). Num. 18. Oxford, Reino Unido. Springer-Verlag. 2005. Pag. 358-372. ISBN: 3-540-28372-2<br /> <br /> Manuel Palomo Duarte, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez:<br /> Rete Algorithm Applied to Robotic Soccer. Cast and Tools for Robotics, Vehicular and Communication Systems. Computer Aided Systems Theory, Eurocast 2005 (10). Num. 10. Las Palmas de Gran Canaria, España. Actas del Congreso. 2005. Pag. 280-283<br /> <br /> Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado:<br /> A Formally Verified Quadratic Unification Algorithm. Proceedings of the Fifth International Workshop on the Acl2 Theorem Prover and Its Applications (Acl2-2004). Fifth International Workshop on the Acl2 Theorem Prover and Its Applications (Acl2-2004) (5). Num. 5. Austin, Texas, EEUU. Unicersity of Austin. 2004. Pag. 1-32<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz:<br /> Generalizing Logic Programs Via Subsumption. Computer Aided System Theory - Eurocast 2003: 9th International Workshop on Computer Aided Systems Theory [recurso Electrónico]. International Workshop on Computer Aided Systems Theory. Num. 9. Las Palmas de Gran Canaria. Springer-Verlag. 2004. Pag. 115-126. ISBN: 3-540-20221-8<br /> <br /> Antonia Mª Chavez Gonzalez, {{jalonso}}, Joaquin Borrego Diaz:<br /> Ontology Cleaning By Mereotopological Reasoning. Database and Expert Systems Applications. Webs 2004. International Workshop on Web Semantics. Webs 2004. (Dexa 2004) (3). Num. 3. Zaragoza, España. IEEE Press. 2004. Pag. 132-137<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez:<br /> Towards a Tool for Ontology Engineering. World Automation Congress: Advances in Robotics, Manufacturing, Automation, Control, Soft Computing, Multimedia, Biomedicine, Image Processing and Financial Engineering. Vol. IV. World Automation Congress (). Sevilla, Spain. Tsi Press. 2004. Pag. 1-100. ISBN: 1-889335-20-7<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz:<br /> Towards a Tool for Ontology Engineering. Advances in Roboticas. Vol 4. Wac 2004. Wac (World Automation Congress) (). Sevilla, España. Tsi Press. 2004. Pag. 1-300<br /> <br /> Inmaculada Medina Bulo, Francisco Palomo Lozano, {{jalonso}}, Jose Luis Ruiz Reina:<br /> Verified Computer Algebra in Acl2 (Gröbner Basis Computation). Proceedings of the 7th Int. Conference on Artificial Intelligence and Symbolic Computation (Aisc 2004). 7th Int. Conference on Artificial Intelligence and Symbolic Computation, Aisc 2004 (). Linz, Austria. Springer-Verlag. 2004. Pag. 171-184<br /> <br /> Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> A Formal Proof of Dickson&#039;s Lemma in Acl2. Proceedings of the International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2003. International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (). Almaty, Kazakhstan. Springer-Verlag. 2003. Pag. 49-58<br /> <br /> Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formal Reasoning About Efficient Data Structures: a Case Study in Acl2. LOPSTR 2003, Preproceedings of the International Symposium of Logic Based Program Synthesis and Transformation. International Workshop on Logic Based Program Synthesis and Transformation (). Uppsala, Suecia. Katholieke Universiteit Leuven, Dep. of Computer Science. 2003. Pag. 97-112<br /> <br /> Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Formal Verification of Molecular Computational Models in Acl2: a Case Study. CAEPIA-TTIA 2003. X Conferencia de la Asocicación Española para la Inteligenciia Artificial. Asociación Española para la Inteligencia Artificial. Conferencia. Num. 10. San Sebastián. Universidad del País Vasco, Servicio Editorial. 2003. Pag. 235-240. ISBN: 84-8373-564-4<br /> <br /> Miguel Angel Gutierrez Naranjo, {{jalonso}}, Joaquin Borrego Diaz:<br /> Generalizing Logic Programs Via Subsumption. Eurocast 2003: Cast and Tools for Complexity in Biological, Physical and Engineering Systems: Extended Abstracts. International Conference on Computer Aided Systems Theory. Num. 9. Las Palmas de Gran Canaria. Universidad de las Palmas de Gran Canaria. 2003. Pag. 185-188. ISBN: 84-688-0820-2<br /> <br /> Antonia Mª Chavez Gonzalez, Joaquin Borrego Diaz, {{jalonso}}:<br /> Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases (Iea/Aie 2003). Libro de Actas del 16th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (Iea/Aie 2003). Iea/Aie 2003 (). Loughborough, United Kingdom. Springer, Berlín, Alemania. 2003. Pag. 789-798<br /> <br /> Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> A Generic Instantiation Tool and a Case Study: a Generic Multiset Theory. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 188-203<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Jorge D. Navarro Marín:<br /> A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases. Proc. of the 28th Annual Conference of IEEE Industrial Electronics Society. The 28th Annual Conference of IEEE Industrial Electronics Society. Sevilla, España. IEEE Press. 2002. Pag. 1806-1811<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo, Jorge D. Navarro Marín:<br /> A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases. Proceedings of the Iecon&#039;02. Iecon&#039;02 (). Sevilla, España. IEEE Industrial Electronic Society. 2002. Pag. 1806-1811. ISBN: 0-7803-7474-6<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz:<br /> A Quasi-Metric for Machine Learning. 8th Ibero-American Conference on A.I. Ibero-American Conference on A.I. Num. 8. Sevilla. Springer, Berlín, Alemania. 2002. Pag. 193-203<br /> <br /> Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> A Theory About First-Order Terms in Acl2. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 78-100<br /> <br /> Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Desarrollo Formal y Verificación de Sistemas Proposicionales. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 1-12<br /> <br /> Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Progress Report: Term Dags Using Stobjs. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 101-108<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo:<br /> Towards a Practical Argumentative Reasoning With Qsd. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 111-120<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> Una Introducción al Análisis Formal de Conceptos en PVS. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 33-46<br /> <br /> Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Verificación Formal y Eficiencia: un Caso de Estudio Aplicado a la Unificación de Términos. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 77-90<br /> <br /> Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Verification in Acl2 of a Generic Framework to Synthesize SAT-Provers. Preproceedings of the International Workshop on Logic Based Program Development and Transformation. International Workshop on Logic Based Program Development and Transformation. Madrid, Spain. Facultad de Informática de la Universidad Politécnica de Madrid. 2002. Pag. 182-197<br /> <br /> Inmaculada Medina Bulo, Francisco Palomo Lozano, {{jalonso}}:<br /> A Certified Polynomial-Based Decision Procedure for Propositional Logic. International Conference on Theorem Proving in Higher Order Logics. International Conference on Theorem Proving in Higher Order Logics (14). Num. 14. Edimburgo (Escocia), Reino Unido. Division of Informatics of Edinburgh University. 2001. Pag. 297-312<br /> <br /> {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> Formalización del Razonamiento Ecuacional en una Lógica Computacional. Actas del I Encuentro de Matemáticos Andaluces. Encuentro de Matemáticos Andaluces. Num. 1. Sevilla, España. Universidad de Sevilla. Secretariado de Publicaciones. 2001. Pag. 41-50. ISBN: 84-472-0639-4<br /> <br /> {{jalonso}}, Joaquin Borrego Diaz:<br /> Proximidad Entre Clausulas en Programacion Logica Inductiva. Actas del I Encuentro de Matemáticos Andaluces. Encuentro de Matemáticos Andaluces. Num. 1. Sevilla, España. Universidad de Sevilla. Secretariado de Publicaciones. 2001. Pag. 33-40. ISBN: 84-472-0639-4<br /> <br /> Miguel Angel Gutierrez Naranjo, {{jalonso}}, Joaquin Borrego Diaz:<br /> Proximidad Entre Cláusulas en Programación Lógica Inductiva. Actas del Encuentro de Matemáticos Andaluces: Comunicaciones. Encuentro de Matemáticos Andaluces (). Sevilla, España. Servicio de Publicaciones de la Universidad de Sevilla. 2001. Pag. 33-40. ISBN: 84-472-0290-9<br /> <br /> Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Verifying an Applicative ATP Using Multiset Relations. Eurocast 2001 Conference. Eurocast 2001 Conference. Las Palmas de Gran Canaria. 0. 2001. Pag. 616-626<br /> <br /> Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> A Mechanical Proof of Knuth-Bendix Critical Pair Theorem (Using Acl2). Proceedings of the Third International Workshop on First-Order Theorem Proving. First-Order Theorem Proving (3). Num. 3. ST Andrews, Scotland. Fachberichte Informatik, Universitat Koblenz-Landau. 2000. Pag. 206-216<br /> <br /> Miguel Angel Gutierrez Naranjo, {{jalonso}}, Joaquin Borrego Diaz:<br /> A Topological Study of the Upward Refinement Operators on ILP. ILP 2000 - Work in Progress Reports. Inductive Logic Programming 10th International Conference, ILP 2000. Londres, Reino Unido. James Cussens - Alan Frisch (Eds.). 2000. Pag. 120-137<br /> <br /> Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formalizing Rewriting in the Acl2 Theorem Prover. Artificial Intelligence and Symbolic Computation, Aisc 2000, Revised Papers. Int. Conference on Artificial Intelligence and Symbolic Computation (). Madrid, España. Springer-Verlag. 2000. Pag. 92-106<br /> <br /> Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Multiset Relations: a Tool for Proving Termination. Proceedings of the Acl2 Workshop 2000. Second Acl2 Workshop (2). Num. 2. Austin, Texas, EEUU. University of Texas At Austin. 2000. Pag. 82-91<br /> <br /> Miguel Angel Gutierrez Naranjo, {{jalonso}}, Joaquin Borrego Diaz:<br /> Una Quasi-Metrica Basada en Subsuncion. IV Jornadas Cientificas en Tecnologias de la Informacion. Jornadas Cientificas en Tecnologias de la Informacion. Num. 4. Cadiz, España. Servicio de Publicaciones de la Universidad de Cádiz. 2000. Pag. 260-267<br /> <br /> Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado:<br /> Mechanical Verification of a Rule-Based Unification Algorithm in the Boyer-Moore Theorem Prover. Proc. of Joint Conference on Declarative Programming. Joint Conference on Declarative Programming. L&#039;aquila, Italia. 1999. Pag. 289-304<br /> <br /> Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Razonamiento Automático en Sistemas de Representación del Conocimiento (y su Relación con la Enseñanza de la Inteligencia Artificial). IV Jornades Sobre L&#039;ensenyament Universitari de la Infomàtica. IV Jornadas Sobre la Enseñanza Universitaria de la Informatica (Jenui&#039;98) (). Andorra. Enginyeria I Arquitectura la Salle. 1998. Pag. 289-296<br /> <br /> Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Verificación Automática de Sistemas de Razonamiento (Aplicación a la Enseñanza de la Inteligencia Artificial). IV Jornades Sobre L&#039;ensenyament Universitari de la Infomàtica. IV Jornadas Sobre la Enseñanza Universitaria de la Informatica (Jenui&#039;98) (). Andorra. Enginyeria I Arquitectura la Salle. 1998. Pag. 297-304<br /> <br /> Juan Jose Arrabal Parrilla, Delia Balbontin Noval, {{jalonso}}, Francisco Felix Lara Martin, Francisco Jesus Martin Mateos, Mario Jesus Perez Jimenez, Jose Luis Ruiz Reina:<br /> Gti: una Herramienta de Edición de Cursos Adaptativos. Actas del XIII Congreso Nacional de Ingenieria de Proyectos. Journees Détudes Comparatives Franco- Hispano- Italiannes. Num. 1. Burdeos, Francia. 1997. Pag. 627-634<br /> <br /> Rodrigo Fernandez Carrion, Juan Jose Arrabal Parrilla, Jose Antonio Alonso Jimenez:<br /> Hacia una Enseñanza Permanente y Automatizada: Www y Evaluación Automática con Gti. International Congress on Historical Information Systems. International Congress on Historical Information Systems (). Vitoria. 1997. Pag. 1-1<br /> <br /> Delia Balbontin Noval, Mª Luisa de la Vega Royo, {{jalonso}}, Juan Jose Arrabal Parrilla:<br /> Aprende Matemáticas. Actas del Primer Encuentro de Informática Educativa: Edie. Primer Encuentro de Informática Educativa (Edie) (). Cees (Madrid). Asociacion para el Desarrollo de la Informatica Educativa. 1994. Pag. 20-25<br /> <br /> Delia Balbontin Noval, {{jalonso}}, Juan Jose Arrabal Parrilla, Francisco Javier Herrera Govantes:<br /> Especificación Formal de Bases de Datos con un Demostrador Automático de Teoremas. Actas del II Congreso Nacional de Programación Declarativa. Congreso Nacional de Programación Declarativa. Num. 2. Sin Editorial. 1993. Pag. 343-344<br /> <br /> Delia Balbontin Noval, Juan Jose Arrabal Parrilla, {{jalonso}}, Francisco Javier Herrera Govantes:<br /> Automated Proofs in Group Theory With Otter. Proceedings of the Fith International Symposium on Knowledge Engineering. Fifth International Symposium on Knowledge Engineering (). Sevilla. Rank-Xerox. 1992. Pag. 326-331<br /> <br /> Delia Balbontin Noval, {{jalonso}}, Juan Jose Arrabal Parrilla, Francisco Javier Herrera Govantes:<br /> Razonamiento Automático en Lógica de Primer Orden. Actas del VIII Congreso de Lenguajes Naturales y Lenguajes Formales. VIII Congreso de Lenguajes Naturales y Lenguajes Formales (). Gerona (España). 1992. Pag. 165-172<br /> <br /> {{jalonso}}, Emilio Briales Morales, Agustin Riscos:<br /> Preuve Automatique Dans Le Calcul Propositionnel Et Les Logiques Trivalentes. Computational Topology and Geometry and Computation in Teaching Mathematics. Computational Topology and Geometry and Computation in Teaching of Mathematics. Num. 1. Sevilla. Servicio de Publicaciones de la Universidad de Sevilla. 1990. Pag. 15-24. ISBN: 84-7405-639-X<br /> <br /> {{jalonso}}, Emilio Briales Morales:<br /> Lógicas Polivalentes y Bases de Gröbner. V Congreso de Lenguajes Naturales y Lenguajes Formales. Congreso de Lenguajes Naturales y Lenguajes Formales (5). Num. 5. Barcelona, España. Universidad Barcelona. 1989. Pag. 307-315<br /> <br /> Tesis dirigidas:<br /> Director/a: {{jalonso}}, Doctorando: Maria Jose Hidalgo Doblado:<br /> Teoría Computacional (en PVS) de la Programación Lógica y del Análisis Formal de Conceptos., 2004, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director/a: {{jalonso}}, Doctorando: Inmaculada Medina Bulo:<br /> Verificación Formal en Acl2 del Algoritmo de Buchberger, 2003, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director/a: {{jalonso}}, Doctorando: Miguel Angel Gutierrez Naranjo:<br /> Operadores de Generalizacion para el Aprendizaje Clausal, 2002, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director/a: {{jalonso}}, Doctorando: Francisco Jesus Martin Mateos:<br /> Teoría Computacional (en Acl2) Sobre Cálculos Proposicionales, 2001, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director/a: {{jalonso}}, Doctorando: Jose Luis Ruiz Reina:<br /> Una Teoría Computacional Acerca de la Lógica Ecuacional (Formalización en Acl2 y Demostración Automática de Sus Propiedades), 2000, Ciencias de la Computacion e Inteligencia Artificial</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Publications&diff=17 2008-04-15T18:38:02Z

<p>WikiSysop: /* Libros */</p> <hr /> <div>== Libros ==<br /> {{jalonso}}, Joaquin Borrego Diaz: &#039;&#039;Agentes Inteligentes: una Aproximación desde la Lógica Computacional&#039;&#039;. Sevilla, España. Editorial Kronos. 2002. 127. ISBN: 84-86273-59-5<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz: &#039;&#039;Deducción Automática&#039;&#039;. Sevilla. Editorial Kronos. 2002. 1004. ISBN: 84-86273-58-7<br /> <br /> Jose Antonio Alonso Jimenez, Jose Luis Ruiz Reina, Joaquin Borrego Diaz: &#039;&#039;Curso Práctico de Teoría de Conjuntos&#039;&#039;. Sevilla. La Ñ. 1998. 344. ISBN: 84-89524-45-9<br /> <br /> == Capítulos en Libros ==<br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez: &#039;&#039;Logic Databases and Inconsistgency Handling. Encyclopedia of Databases Technologies and Applications&#039;&#039;. Hershey (Pennsylvania), Estados Unidos. Idea Group Reference. Vol. 1. 2006. Pag. 336-340. ISBN: 1-59140-560-2<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina: &#039;&#039;Formal Verification of Molecular Computational Models in ACL2: a Case Study&#039;&#039;. CAEPIA-TTIA 2003. San Sebastián. Universidad del País Vasco. Vol. 2. 2003. Pag. 235-244. ISBN: 84-8373-564-4<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz: &#039;&#039;Generalizing Logic Programs Via Subsumption&#039;&#039;. Eurocast 2003 - Cast and Tools for Complexity in Biological, Physical and Engineering Systems (Extended Abstracts). Las Palmas de Gran Canaria, España. Iuctc Universidad de las Palmas de Gran Canaria. Vol. 1. 2003. Pag. 185-188. ISBN: 84-688-0820-2<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: &#039;&#039;Termination in ACL2 Using Multiset Relation.&#039;&#039; Thirty Five Years of Automating Mathematics. Dordrecht, Holanda. Kluwer Academic Publishers. 2003. Pag. 217-245. ISBN: 1-4020-1656-5<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Jorge D. Navarro Marín: &#039;&#039;A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases.&#039;&#039; IECON 2002. Sevilla, España. IEEE Industrial Electronic Society. 2002. Pag. 1806-1811. ISBN: 0-7803-7475-4<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez:<br /> Deduccion Automatica en Anillos Ternarios: Algunos Métodos de Procesamiento del Conocimiento Matemático. Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 23-32. ISBN: 84-472-0290-9<br /> <br /> Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos:<br /> Formalización del Razonamiento Ecuacional en una Lógica Computacional. Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 41-50. ISBN: 84-472-0290-9<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Proximidad Entre Clausulas en Programacion Logica Inductiva. Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 33-40. ISBN: 84-472-0290-9<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez: &#039;&#039;Estrategias para la Demostración Automática de Teoremas.&#039;&#039; Libro de Actas Cinte&#039;00. Cadiz. Servicio de Publicaciones de la Universidad de Cádiz. 2000. Pag. 276-283<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz: &#039;&#039;Interpretación Reactiva de Sistemas Basados en Conocimiento.&#039;&#039; Actas del IV Congreso Isko España. Granada. 1999. Pag. 187-193. ISBN: 84-699-0289-X<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina: &#039;&#039;Razonamiento Automático en Sistemas de Representación del Conocimiento (y su Relación con la Enseñanza de la Inteligencia Artificial).&#039;&#039; IV Jornades Sobre L&#039;ensenyament Universitari de la Informatica (Jenui 98). Barcelona, España. Enginyeria I Arquitectura la Salle. 1998. Pag. 289-296. ISBN: 84-922538-3-5<br /> <br /> Juan Jose Arrabal Parrilla, Delia Balbontin Noval, Jose Antonio Alonso Jimenez, Francisco Felix Lara Martin, Francisco Jesus Martin Mateos, Mario Jesus Perez Jimenez, Jose Luis Ruiz Reina: &#039;&#039;GTI: una Herramienta de Edición de Cursos Adaptativos.&#039;&#039; Actas del XIII Congreso Nacional de Ingeniería de Proyectos. Sevilla. Antonio F. Martin Navarro. 1997. Pag. 627-634. ISBN: 84-88783-30-2<br /> <br /> Luis Laita, Eugenio Roanes-Lozano, Jose Antonio Alonso Jimenez, Emilio Briales Morales: &#039;&#039;Verificación Algebraica de SBC Basada en la Lógica Trievaluada, Teoría e Implementación.&#039;&#039; I Jornadas Sobre Inteligencia Artificial, Control y Sistemas Expertos. Madrid, España. Servicio de Publicaciones de la Universidad de Alcala. 1996. Pag. 241-255. ISBN: 84-8138-147-0<br /> <br /> Jose Antonio Alonso Jimenez, Alejandro Fernandez Margarit, Mario Jesus Perez Jimenez: &#039;&#039;Razonamiento Automático. Lógica Formal : Orígenes, Métodos y Aplicaciones.&#039;&#039; Sevilla. Kronos S.A. 1995. Pag. 189-211. ISBN: 84-88620-56-X<br /> <br /> Juan Jose Arrabal Parrilla, Jose Antonio Alonso Jimenez, Alejandro Fernandez Margarit, Mario Jesus Perez Jimenez: &#039;&#039;Automatización de la Aritmética. Lenguajes Naturales y Lenguajes Formales,&#039;&#039; X. Barcelona. Ppu: Promociones y Publicaciones Universitarias. 1994. Pag. 167-182. ISBN: 84-477-0396-7<br /> <br /> == Publicaciones en Revistas ==<br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina: &#039;&#039;A Formally Verified Prover for the ALC Description Logic&#039;&#039;. Lecture Notes in Computer Science. Vol. 4732. 2007. Pag. 135-150<br /> <br /> Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado: &#039;&#039;Formal Correctness of a Quadratic Unification Algorithm.&#039;&#039; Journal of Automated Reasoning. Vol. 37. Núm. 1-2. 2006. Pag. 67-92<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Francisco Jesus Martin Mateos: &#039;&#039;Foundational Challenges in Automated Semantic Web Data and Ontology Cleaning.&#039;&#039; IEEE Intelligent Systems. Vol. 21. Núm. 1. 2006. Pag. 42-52<br /> <br /> Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado: &#039;&#039;Proof Pearl: a Formal Proof of Higman S Lemma in ACL2.&#039;&#039; Lecture Notes in Computer Science. Vol. 3603. 2005. Pag. 358-372<br /> <br /> Manuel Palomo Duarte, Jose Antonio Alonso Jimenez, Francisco Jesus Martin Mateos: &#039;&#039;Rete Algorithm Applied to Robotic Soccer.&#039;&#039; Lecture Notes in Computer Science. Vol. 3643. 2005. Pag. 571-576<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: &#039;&#039;Formal Reasoning About Efficient Data Structures: a Case Study in ACL2.&#039;&#039; Lecture Notes in Computer Science. Vol. 3018. 2004. Pag. 75-91<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina: &#039;&#039;Formal Verification of a Generic Framework to Synthesize SAT-Provers.&#039;&#039; Journal of Automated Reasoning. Vol. 32. Núm. 4. 2004. Pag. 287-313<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Formal Verification of Molecular Computational Models in Acl2: a Case Study. Lecture Notes in Computer Science. Vol. 3040. 2004. Pag. 344-353<br /> <br /> Antonia Mª Chavez Gonzalez, Joaquin Borrego Diaz, Jose Antonio Alonso Jimenez:<br /> Ontology Cleaning By Mereotopological Reasoning. Proceedings. 2004. Pag. 132-137<br /> <br /> Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> Verification of the Formal Concept Analysis. RACSAM. Revista de la Real Academia de Ciencias. Serie a: Matemáticas. Vol. 98. 2004. Pag. 3-16<br /> <br /> Inmaculada Medina Bulo, Francisco Palomo Lozano, Jose Antonio Alonso Jimenez, Jose Luis Ruiz Reina:<br /> Verified Computer Algebra in Acl2 (Grobner Bases Computation). Lecture Notes in Computer Science. Vol. 3249. 2004. Pag. 171-184<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> A Formal Proof of Dickson&#039;s Lemma in Acl2. Lecture Notes in Computer Science. Vol. 2850. 2003. Pag. 49-58<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Generalizing Programs Via Subsumption. Lecture Notes in Computer Science. Vol. 2809. 2003. Pag. 115-126<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo, Jorge D. Navarro Marín:<br /> Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases. Lecture Notes in Computer Science. Vol. 2718. 2003. Pag. 789-798<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Verification in Acl2 of a Generic Framework to Synthesize SAT-Provers. Lecture Notes in Computer Science. Vol. 2664. 2003. Pag. 182-198<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> A Quasi-Metric for Machine Learning. Lecture Notes in Computer Science. Vol. 2527. 2002. Pag. 193-203<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formal Proofs About Rewriting Using Acl2. Annals of Mathematics and Artificial Intelligence . Vol. 36. Núm. 3. 2002. Pag. 239-262<br /> <br /> Inmaculada Medina Bulo, Francisco Palomo Lozano, Jose Antonio Alonso Jimenez:<br /> A Certified Polynomial-Based Decision Procedure for Propositional Logic. Lecture Notes in Computer Science. Núm. 2152. 2001. Pag. 297-312<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formalizing Rewriting in the Acl2 Theorem Prover. Lecture Notes in Computer Science. Vol. 1930. 2001. Pag. 92-106<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Verifying an Applicative ATP Using Multiset Relations. Lecture Notes in Computer Science. Vol. 2178. 2001. Pag. 612-626<br /> <br /> J. Chazarain, Agustin Riscos, Jose Antonio Alonso Jimenez, Emilio Briales Morales:<br /> Multivalued-Logic and Gröbner Bases With Applications to Modal Logic. Journal of Symbolic Computation . Vol. 11. 1991. Pag. 181-194<br /> <br /> Libros de Actas<br /> Jose Antonio Alonso Jimenez, Jose Luis Ruiz Reina, Joaquin Borrego Diaz, Manuel Ojeda Aciego:<br /> Ideia 2002: I Taller Iberoamericano Sobre Deducción Automática e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Sevilla, España. Departamento de Ciencias de la Computacion e Inteligencia Artificial. Universidad de Sevilla. 2002<br /> <br /> Aportaciones a Congresos<br /> Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> A Formally Verified Proof (in PVS) of the Strong Completeness Theorem Of Propositional Sld-Resolution. Cast and Tools for Robotics, Vehicular and Communication Systems. Computer Aided Systems Theory, Eurocast 2005 (10). Num. 10. Las Palmas de Gran Canaria, España. Actas del Congreso. 2005. Pag. 83-86<br /> <br /> Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado:<br /> Proof Pearl: a Formal Proof of Higman&#039;s Lemma in Acl2. Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics (18). Num. 18. Oxford, Reino Unido. Springer-Verlag. 2005. Pag. 358-372. ISBN: 3-540-28372-2<br /> <br /> Manuel Palomo Duarte, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez:<br /> Rete Algorithm Applied to Robotic Soccer. Cast and Tools for Robotics, Vehicular and Communication Systems. Computer Aided Systems Theory, Eurocast 2005 (10). Num. 10. Las Palmas de Gran Canaria, España. Actas del Congreso. 2005. Pag. 280-283<br /> <br /> Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado:<br /> A Formally Verified Quadratic Unification Algorithm. Proceedings of the Fifth International Workshop on the Acl2 Theorem Prover and Its Applications (Acl2-2004). Fifth International Workshop on the Acl2 Theorem Prover and Its Applications (Acl2-2004) (5). Num. 5. Austin, Texas, EEUU. Unicersity of Austin. 2004. Pag. 1-32<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Generalizing Logic Programs Via Subsumption. Computer Aided System Theory - Eurocast 2003: 9th International Workshop on Computer Aided Systems Theory [recurso Electrónico]. International Workshop on Computer Aided Systems Theory. Num. 9. Las Palmas de Gran Canaria. Springer-Verlag. 2004. Pag. 115-126. ISBN: 3-540-20221-8<br /> <br /> Antonia Mª Chavez Gonzalez, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Ontology Cleaning By Mereotopological Reasoning. Database and Expert Systems Applications. Webs 2004. International Workshop on Web Semantics. Webs 2004. (Dexa 2004) (3). Num. 3. Zaragoza, España. IEEE Press. 2004. Pag. 132-137<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez:<br /> Towards a Tool for Ontology Engineering. World Automation Congress: Advances in Robotics, Manufacturing, Automation, Control, Soft Computing, Multimedia, Biomedicine, Image Processing and Financial Engineering. Vol. IV. World Automation Congress (). Sevilla, Spain. Tsi Press. 2004. Pag. 1-100. ISBN: 1-889335-20-7<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Towards a Tool for Ontology Engineering. Advances in Roboticas. Vol 4. Wac 2004. Wac (World Automation Congress) (). Sevilla, España. Tsi Press. 2004. Pag. 1-300<br /> <br /> Inmaculada Medina Bulo, Francisco Palomo Lozano, Jose Antonio Alonso Jimenez, Jose Luis Ruiz Reina:<br /> Verified Computer Algebra in Acl2 (Gröbner Basis Computation). Proceedings of the 7th Int. Conference on Artificial Intelligence and Symbolic Computation (Aisc 2004). 7th Int. Conference on Artificial Intelligence and Symbolic Computation, Aisc 2004 (). Linz, Austria. Springer-Verlag. 2004. Pag. 171-184<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> A Formal Proof of Dickson&#039;s Lemma in Acl2. Proceedings of the International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2003. International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (). Almaty, Kazakhstan. Springer-Verlag. 2003. Pag. 49-58<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formal Reasoning About Efficient Data Structures: a Case Study in Acl2. LOPSTR 2003, Preproceedings of the International Symposium of Logic Based Program Synthesis and Transformation. International Workshop on Logic Based Program Synthesis and Transformation (). Uppsala, Suecia. Katholieke Universiteit Leuven, Dep. of Computer Science. 2003. Pag. 97-112<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Formal Verification of Molecular Computational Models in Acl2: a Case Study. CAEPIA-TTIA 2003. X Conferencia de la Asocicación Española para la Inteligenciia Artificial. Asociación Española para la Inteligencia Artificial. Conferencia. Num. 10. San Sebastián. Universidad del País Vasco, Servicio Editorial. 2003. Pag. 235-240. ISBN: 84-8373-564-4<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Generalizing Logic Programs Via Subsumption. Eurocast 2003: Cast and Tools for Complexity in Biological, Physical and Engineering Systems: Extended Abstracts. International Conference on Computer Aided Systems Theory. Num. 9. Las Palmas de Gran Canaria. Universidad de las Palmas de Gran Canaria. 2003. Pag. 185-188. ISBN: 84-688-0820-2<br /> <br /> Antonia Mª Chavez Gonzalez, Joaquin Borrego Diaz, Jose Antonio Alonso Jimenez:<br /> Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases (Iea/Aie 2003). Libro de Actas del 16th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (Iea/Aie 2003). Iea/Aie 2003 (). Loughborough, United Kingdom. Springer, Berlín, Alemania. 2003. Pag. 789-798<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> A Generic Instantiation Tool and a Case Study: a Generic Multiset Theory. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 188-203<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Jorge D. Navarro Marín:<br /> A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases. Proc. of the 28th Annual Conference of IEEE Industrial Electronics Society. The 28th Annual Conference of IEEE Industrial Electronics Society. Sevilla, España. IEEE Press. 2002. Pag. 1806-1811<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo, Jorge D. Navarro Marín:<br /> A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases. Proceedings of the Iecon&#039;02. Iecon&#039;02 (). Sevilla, España. IEEE Industrial Electronic Society. 2002. Pag. 1806-1811. ISBN: 0-7803-7474-6<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> A Quasi-Metric for Machine Learning. 8th Ibero-American Conference on A.I. Ibero-American Conference on A.I. Num. 8. Sevilla. Springer, Berlín, Alemania. 2002. Pag. 193-203<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> A Theory About First-Order Terms in Acl2. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 78-100<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Desarrollo Formal y Verificación de Sistemas Proposicionales. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 1-12<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Progress Report: Term Dags Using Stobjs. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 101-108<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo:<br /> Towards a Practical Argumentative Reasoning With Qsd. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 111-120<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> Una Introducción al Análisis Formal de Conceptos en PVS. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 33-46<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Verificación Formal y Eficiencia: un Caso de Estudio Aplicado a la Unificación de Términos. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 77-90<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Verification in Acl2 of a Generic Framework to Synthesize SAT-Provers. Preproceedings of the International Workshop on Logic Based Program Development and Transformation. International Workshop on Logic Based Program Development and Transformation. Madrid, Spain. Facultad de Informática de la Universidad Politécnica de Madrid. 2002. Pag. 182-197<br /> <br /> Inmaculada Medina Bulo, Francisco Palomo Lozano, Jose Antonio Alonso Jimenez:<br /> A Certified Polynomial-Based Decision Procedure for Propositional Logic. International Conference on Theorem Proving in Higher Order Logics. International Conference on Theorem Proving in Higher Order Logics (14). Num. 14. Edimburgo (Escocia), Reino Unido. Division of Informatics of Edinburgh University. 2001. Pag. 297-312<br /> <br /> Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> Formalización del Razonamiento Ecuacional en una Lógica Computacional. Actas del I Encuentro de Matemáticos Andaluces. Encuentro de Matemáticos Andaluces. Num. 1. Sevilla, España. Universidad de Sevilla. Secretariado de Publicaciones. 2001. Pag. 41-50. ISBN: 84-472-0639-4<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Proximidad Entre Clausulas en Programacion Logica Inductiva. Actas del I Encuentro de Matemáticos Andaluces. Encuentro de Matemáticos Andaluces. Num. 1. Sevilla, España. Universidad de Sevilla. Secretariado de Publicaciones. 2001. Pag. 33-40. ISBN: 84-472-0639-4<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Proximidad Entre Cláusulas en Programación Lógica Inductiva. Actas del Encuentro de Matemáticos Andaluces: Comunicaciones. Encuentro de Matemáticos Andaluces (). Sevilla, España. Servicio de Publicaciones de la Universidad de Sevilla. 2001. Pag. 33-40. ISBN: 84-472-0290-9<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Verifying an Applicative ATP Using Multiset Relations. Eurocast 2001 Conference. Eurocast 2001 Conference. Las Palmas de Gran Canaria. 0. 2001. Pag. 616-626<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> A Mechanical Proof of Knuth-Bendix Critical Pair Theorem (Using Acl2). Proceedings of the Third International Workshop on First-Order Theorem Proving. First-Order Theorem Proving (3). Num. 3. ST Andrews, Scotland. Fachberichte Informatik, Universitat Koblenz-Landau. 2000. Pag. 206-216<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> A Topological Study of the Upward Refinement Operators on ILP. ILP 2000 - Work in Progress Reports. Inductive Logic Programming 10th International Conference, ILP 2000. Londres, Reino Unido. James Cussens - Alan Frisch (Eds.). 2000. Pag. 120-137<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formalizing Rewriting in the Acl2 Theorem Prover. Artificial Intelligence and Symbolic Computation, Aisc 2000, Revised Papers. Int. Conference on Artificial Intelligence and Symbolic Computation (). Madrid, España. Springer-Verlag. 2000. Pag. 92-106<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Multiset Relations: a Tool for Proving Termination. Proceedings of the Acl2 Workshop 2000. Second Acl2 Workshop (2). Num. 2. Austin, Texas, EEUU. University of Texas At Austin. 2000. Pag. 82-91<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Una Quasi-Metrica Basada en Subsuncion. IV Jornadas Cientificas en Tecnologias de la Informacion. Jornadas Cientificas en Tecnologias de la Informacion. Num. 4. Cadiz, España. Servicio de Publicaciones de la Universidad de Cádiz. 2000. Pag. 260-267<br /> <br /> Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado:<br /> Mechanical Verification of a Rule-Based Unification Algorithm in the Boyer-Moore Theorem Prover. Proc. of Joint Conference on Declarative Programming. Joint Conference on Declarative Programming. L&#039;aquila, Italia. 1999. Pag. 289-304<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Razonamiento Automático en Sistemas de Representación del Conocimiento (y su Relación con la Enseñanza de la Inteligencia Artificial). IV Jornades Sobre L&#039;ensenyament Universitari de la Infomàtica. IV Jornadas Sobre la Enseñanza Universitaria de la Informatica (Jenui&#039;98) (). Andorra. Enginyeria I Arquitectura la Salle. 1998. Pag. 289-296<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Verificación Automática de Sistemas de Razonamiento (Aplicación a la Enseñanza de la Inteligencia Artificial). IV Jornades Sobre L&#039;ensenyament Universitari de la Infomàtica. IV Jornadas Sobre la Enseñanza Universitaria de la Informatica (Jenui&#039;98) (). Andorra. Enginyeria I Arquitectura la Salle. 1998. Pag. 297-304<br /> <br /> Juan Jose Arrabal Parrilla, Delia Balbontin Noval, Jose Antonio Alonso Jimenez, Francisco Felix Lara Martin, Francisco Jesus Martin Mateos, Mario Jesus Perez Jimenez, Jose Luis Ruiz Reina:<br /> Gti: una Herramienta de Edición de Cursos Adaptativos. Actas del XIII Congreso Nacional de Ingenieria de Proyectos. Journees Détudes Comparatives Franco- Hispano- Italiannes. Num. 1. Burdeos, Francia. 1997. Pag. 627-634<br /> <br /> Rodrigo Fernandez Carrion, Juan Jose Arrabal Parrilla, Jose Antonio Alonso Jimenez:<br /> Hacia una Enseñanza Permanente y Automatizada: Www y Evaluación Automática con Gti. International Congress on Historical Information Systems. International Congress on Historical Information Systems (). Vitoria. 1997. Pag. 1-1<br /> <br /> Delia Balbontin Noval, Mª Luisa de la Vega Royo, Jose Antonio Alonso Jimenez, Juan Jose Arrabal Parrilla:<br /> Aprende Matemáticas. Actas del Primer Encuentro de Informática Educativa: Edie. Primer Encuentro de Informática Educativa (Edie) (). Cees (Madrid). Asociacion para el Desarrollo de la Informatica Educativa. 1994. Pag. 20-25<br /> <br /> Delia Balbontin Noval, Jose Antonio Alonso Jimenez, Juan Jose Arrabal Parrilla, Francisco Javier Herrera Govantes:<br /> Especificación Formal de Bases de Datos con un Demostrador Automático de Teoremas. Actas del II Congreso Nacional de Programación Declarativa. Congreso Nacional de Programación Declarativa. Num. 2. Sin Editorial. 1993. Pag. 343-344<br /> <br /> Delia Balbontin Noval, Juan Jose Arrabal Parrilla, Jose Antonio Alonso Jimenez, Francisco Javier Herrera Govantes:<br /> Automated Proofs in Group Theory With Otter. Proceedings of the Fith International Symposium on Knowledge Engineering. Fifth International Symposium on Knowledge Engineering (). Sevilla. Rank-Xerox. 1992. Pag. 326-331<br /> <br /> Delia Balbontin Noval, Jose Antonio Alonso Jimenez, Juan Jose Arrabal Parrilla, Francisco Javier Herrera Govantes:<br /> Razonamiento Automático en Lógica de Primer Orden. Actas del VIII Congreso de Lenguajes Naturales y Lenguajes Formales. VIII Congreso de Lenguajes Naturales y Lenguajes Formales (). Gerona (España). 1992. Pag. 165-172<br /> <br /> Jose Antonio Alonso Jimenez, Emilio Briales Morales, Agustin Riscos:<br /> Preuve Automatique Dans Le Calcul Propositionnel Et Les Logiques Trivalentes. Computational Topology and Geometry and Computation in Teaching Mathematics. Computational Topology and Geometry and Computation in Teaching of Mathematics. Num. 1. Sevilla. Servicio de Publicaciones de la Universidad de Sevilla. 1990. Pag. 15-24. ISBN: 84-7405-639-X<br /> <br /> Jose Antonio Alonso Jimenez, Emilio Briales Morales:<br /> Lógicas Polivalentes y Bases de Gröbner. V Congreso de Lenguajes Naturales y Lenguajes Formales. Congreso de Lenguajes Naturales y Lenguajes Formales (5). Num. 5. Barcelona, España. Universidad Barcelona. 1989. Pag. 307-315<br /> <br /> Tesis dirigidas:<br /> Director/a: Jose Antonio Alonso Jimenez, Doctorando: Maria Jose Hidalgo Doblado:<br /> Teoría Computacional (en PVS) de la Programación Lógica y del Análisis Formal de Conceptos., 2004, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director/a: Jose Antonio Alonso Jimenez, Doctorando: Inmaculada Medina Bulo:<br /> Verificación Formal en Acl2 del Algoritmo de Buchberger, 2003, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director/a: Jose Antonio Alonso Jimenez, Doctorando: Miguel Angel Gutierrez Naranjo:<br /> Operadores de Generalizacion para el Aprendizaje Clausal, 2002, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director/a: Jose Antonio Alonso Jimenez, Doctorando: Francisco Jesus Martin Mateos:<br /> Teoría Computacional (en Acl2) Sobre Cálculos Proposicionales, 2001, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director/a: Jose Antonio Alonso Jimenez, Doctorando: Jose Luis Ruiz Reina:<br /> Una Teoría Computacional Acerca de la Lógica Ecuacional (Formalización en Acl2 y Demostración Automática de Sus Propiedades), 2000, Ciencias de la Computacion e Inteligencia Artificial</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Plantilla:Jalonso&diff=16 2008-04-15T18:32:50Z

<p>WikiSysop: New page: [http://www.cs.us.es/~jalonso José A. Alonso]</p> <hr /> <div>[http://www.cs.us.es/~jalonso José A. Alonso]</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Publications&diff=15 2008-04-15T18:29:51Z

<p>WikiSysop: /* Libros */</p> <hr /> <div>== Libros ==<br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz: &#039;&#039;Agentes Inteligentes: una Aproximación desde la Lógica Computacional&#039;&#039;. Sevilla, España. Editorial Kronos. 2002. 127. ISBN: 84-86273-59-5<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz: &#039;&#039;Deducción Automática&#039;&#039;. Sevilla. Editorial Kronos. 2002. 1004. ISBN: 84-86273-58-7<br /> <br /> Jose Antonio Alonso Jimenez, Jose Luis Ruiz Reina, Joaquin Borrego Diaz: &#039;&#039;Curso Práctico de Teoría de Conjuntos&#039;&#039;. Sevilla. La Ñ. 1998. 344. ISBN: 84-89524-45-9<br /> <br /> == Capítulos en Libros ==<br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez: &#039;&#039;Logic Databases and Inconsistgency Handling. Encyclopedia of Databases Technologies and Applications&#039;&#039;. Hershey (Pennsylvania), Estados Unidos. Idea Group Reference. Vol. 1. 2006. Pag. 336-340. ISBN: 1-59140-560-2<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina: &#039;&#039;Formal Verification of Molecular Computational Models in ACL2: a Case Study&#039;&#039;. CAEPIA-TTIA 2003. San Sebastián. Universidad del País Vasco. Vol. 2. 2003. Pag. 235-244. ISBN: 84-8373-564-4<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz: &#039;&#039;Generalizing Logic Programs Via Subsumption&#039;&#039;. Eurocast 2003 - Cast and Tools for Complexity in Biological, Physical and Engineering Systems (Extended Abstracts). Las Palmas de Gran Canaria, España. Iuctc Universidad de las Palmas de Gran Canaria. Vol. 1. 2003. Pag. 185-188. ISBN: 84-688-0820-2<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: &#039;&#039;Termination in ACL2 Using Multiset Relation.&#039;&#039; Thirty Five Years of Automating Mathematics. Dordrecht, Holanda. Kluwer Academic Publishers. 2003. Pag. 217-245. ISBN: 1-4020-1656-5<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Jorge D. Navarro Marín: &#039;&#039;A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases.&#039;&#039; IECON 2002. Sevilla, España. IEEE Industrial Electronic Society. 2002. Pag. 1806-1811. ISBN: 0-7803-7475-4<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez:<br /> Deduccion Automatica en Anillos Ternarios: Algunos Métodos de Procesamiento del Conocimiento Matemático. Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 23-32. ISBN: 84-472-0290-9<br /> <br /> Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos:<br /> Formalización del Razonamiento Ecuacional en una Lógica Computacional. Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 41-50. ISBN: 84-472-0290-9<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Proximidad Entre Clausulas en Programacion Logica Inductiva. Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 33-40. ISBN: 84-472-0290-9<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez: &#039;&#039;Estrategias para la Demostración Automática de Teoremas.&#039;&#039; Libro de Actas Cinte&#039;00. Cadiz. Servicio de Publicaciones de la Universidad de Cádiz. 2000. Pag. 276-283<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz: &#039;&#039;Interpretación Reactiva de Sistemas Basados en Conocimiento.&#039;&#039; Actas del IV Congreso Isko España. Granada. 1999. Pag. 187-193. ISBN: 84-699-0289-X<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina: &#039;&#039;Razonamiento Automático en Sistemas de Representación del Conocimiento (y su Relación con la Enseñanza de la Inteligencia Artificial).&#039;&#039; IV Jornades Sobre L&#039;ensenyament Universitari de la Informatica (Jenui 98). Barcelona, España. Enginyeria I Arquitectura la Salle. 1998. Pag. 289-296. ISBN: 84-922538-3-5<br /> <br /> Juan Jose Arrabal Parrilla, Delia Balbontin Noval, Jose Antonio Alonso Jimenez, Francisco Felix Lara Martin, Francisco Jesus Martin Mateos, Mario Jesus Perez Jimenez, Jose Luis Ruiz Reina: &#039;&#039;GTI: una Herramienta de Edición de Cursos Adaptativos.&#039;&#039; Actas del XIII Congreso Nacional de Ingeniería de Proyectos. Sevilla. Antonio F. Martin Navarro. 1997. Pag. 627-634. ISBN: 84-88783-30-2<br /> <br /> Luis Laita, Eugenio Roanes-Lozano, Jose Antonio Alonso Jimenez, Emilio Briales Morales: &#039;&#039;Verificación Algebraica de SBC Basada en la Lógica Trievaluada, Teoría e Implementación.&#039;&#039; I Jornadas Sobre Inteligencia Artificial, Control y Sistemas Expertos. Madrid, España. Servicio de Publicaciones de la Universidad de Alcala. 1996. Pag. 241-255. ISBN: 84-8138-147-0<br /> <br /> Jose Antonio Alonso Jimenez, Alejandro Fernandez Margarit, Mario Jesus Perez Jimenez: &#039;&#039;Razonamiento Automático. Lógica Formal : Orígenes, Métodos y Aplicaciones.&#039;&#039; Sevilla. Kronos S.A. 1995. Pag. 189-211. ISBN: 84-88620-56-X<br /> <br /> Juan Jose Arrabal Parrilla, Jose Antonio Alonso Jimenez, Alejandro Fernandez Margarit, Mario Jesus Perez Jimenez: &#039;&#039;Automatización de la Aritmética. Lenguajes Naturales y Lenguajes Formales,&#039;&#039; X. Barcelona. Ppu: Promociones y Publicaciones Universitarias. 1994. Pag. 167-182. ISBN: 84-477-0396-7<br /> <br /> == Publicaciones en Revistas ==<br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina: &#039;&#039;A Formally Verified Prover for the ALC Description Logic&#039;&#039;. Lecture Notes in Computer Science. Vol. 4732. 2007. Pag. 135-150<br /> <br /> Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado: &#039;&#039;Formal Correctness of a Quadratic Unification Algorithm.&#039;&#039; Journal of Automated Reasoning. Vol. 37. Núm. 1-2. 2006. Pag. 67-92<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Francisco Jesus Martin Mateos: &#039;&#039;Foundational Challenges in Automated Semantic Web Data and Ontology Cleaning.&#039;&#039; IEEE Intelligent Systems. Vol. 21. Núm. 1. 2006. Pag. 42-52<br /> <br /> Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado: &#039;&#039;Proof Pearl: a Formal Proof of Higman S Lemma in ACL2.&#039;&#039; Lecture Notes in Computer Science. Vol. 3603. 2005. Pag. 358-372<br /> <br /> Manuel Palomo Duarte, Jose Antonio Alonso Jimenez, Francisco Jesus Martin Mateos: &#039;&#039;Rete Algorithm Applied to Robotic Soccer.&#039;&#039; Lecture Notes in Computer Science. Vol. 3643. 2005. Pag. 571-576<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: &#039;&#039;Formal Reasoning About Efficient Data Structures: a Case Study in ACL2.&#039;&#039; Lecture Notes in Computer Science. Vol. 3018. 2004. Pag. 75-91<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina: &#039;&#039;Formal Verification of a Generic Framework to Synthesize SAT-Provers.&#039;&#039; Journal of Automated Reasoning. Vol. 32. Núm. 4. 2004. Pag. 287-313<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Formal Verification of Molecular Computational Models in Acl2: a Case Study. Lecture Notes in Computer Science. Vol. 3040. 2004. Pag. 344-353<br /> <br /> Antonia Mª Chavez Gonzalez, Joaquin Borrego Diaz, Jose Antonio Alonso Jimenez:<br /> Ontology Cleaning By Mereotopological Reasoning. Proceedings. 2004. Pag. 132-137<br /> <br /> Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> Verification of the Formal Concept Analysis. RACSAM. Revista de la Real Academia de Ciencias. Serie a: Matemáticas. Vol. 98. 2004. Pag. 3-16<br /> <br /> Inmaculada Medina Bulo, Francisco Palomo Lozano, Jose Antonio Alonso Jimenez, Jose Luis Ruiz Reina:<br /> Verified Computer Algebra in Acl2 (Grobner Bases Computation). Lecture Notes in Computer Science. Vol. 3249. 2004. Pag. 171-184<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> A Formal Proof of Dickson&#039;s Lemma in Acl2. Lecture Notes in Computer Science. Vol. 2850. 2003. Pag. 49-58<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Generalizing Programs Via Subsumption. Lecture Notes in Computer Science. Vol. 2809. 2003. Pag. 115-126<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo, Jorge D. Navarro Marín:<br /> Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases. Lecture Notes in Computer Science. Vol. 2718. 2003. Pag. 789-798<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Verification in Acl2 of a Generic Framework to Synthesize SAT-Provers. Lecture Notes in Computer Science. Vol. 2664. 2003. Pag. 182-198<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> A Quasi-Metric for Machine Learning. Lecture Notes in Computer Science. Vol. 2527. 2002. Pag. 193-203<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formal Proofs About Rewriting Using Acl2. Annals of Mathematics and Artificial Intelligence . Vol. 36. Núm. 3. 2002. Pag. 239-262<br /> <br /> Inmaculada Medina Bulo, Francisco Palomo Lozano, Jose Antonio Alonso Jimenez:<br /> A Certified Polynomial-Based Decision Procedure for Propositional Logic. Lecture Notes in Computer Science. Núm. 2152. 2001. Pag. 297-312<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formalizing Rewriting in the Acl2 Theorem Prover. Lecture Notes in Computer Science. Vol. 1930. 2001. Pag. 92-106<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Verifying an Applicative ATP Using Multiset Relations. Lecture Notes in Computer Science. Vol. 2178. 2001. Pag. 612-626<br /> <br /> J. Chazarain, Agustin Riscos, Jose Antonio Alonso Jimenez, Emilio Briales Morales:<br /> Multivalued-Logic and Gröbner Bases With Applications to Modal Logic. Journal of Symbolic Computation . Vol. 11. 1991. Pag. 181-194<br /> <br /> Libros de Actas<br /> Jose Antonio Alonso Jimenez, Jose Luis Ruiz Reina, Joaquin Borrego Diaz, Manuel Ojeda Aciego:<br /> Ideia 2002: I Taller Iberoamericano Sobre Deducción Automática e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Sevilla, España. Departamento de Ciencias de la Computacion e Inteligencia Artificial. Universidad de Sevilla. 2002<br /> <br /> Aportaciones a Congresos<br /> Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> A Formally Verified Proof (in PVS) of the Strong Completeness Theorem Of Propositional Sld-Resolution. Cast and Tools for Robotics, Vehicular and Communication Systems. Computer Aided Systems Theory, Eurocast 2005 (10). Num. 10. Las Palmas de Gran Canaria, España. Actas del Congreso. 2005. Pag. 83-86<br /> <br /> Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado:<br /> Proof Pearl: a Formal Proof of Higman&#039;s Lemma in Acl2. Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics (18). Num. 18. Oxford, Reino Unido. Springer-Verlag. 2005. Pag. 358-372. ISBN: 3-540-28372-2<br /> <br /> Manuel Palomo Duarte, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez:<br /> Rete Algorithm Applied to Robotic Soccer. Cast and Tools for Robotics, Vehicular and Communication Systems. Computer Aided Systems Theory, Eurocast 2005 (10). Num. 10. Las Palmas de Gran Canaria, España. Actas del Congreso. 2005. Pag. 280-283<br /> <br /> Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado:<br /> A Formally Verified Quadratic Unification Algorithm. Proceedings of the Fifth International Workshop on the Acl2 Theorem Prover and Its Applications (Acl2-2004). Fifth International Workshop on the Acl2 Theorem Prover and Its Applications (Acl2-2004) (5). Num. 5. Austin, Texas, EEUU. Unicersity of Austin. 2004. Pag. 1-32<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Generalizing Logic Programs Via Subsumption. Computer Aided System Theory - Eurocast 2003: 9th International Workshop on Computer Aided Systems Theory [recurso Electrónico]. International Workshop on Computer Aided Systems Theory. Num. 9. Las Palmas de Gran Canaria. Springer-Verlag. 2004. Pag. 115-126. ISBN: 3-540-20221-8<br /> <br /> Antonia Mª Chavez Gonzalez, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Ontology Cleaning By Mereotopological Reasoning. Database and Expert Systems Applications. Webs 2004. International Workshop on Web Semantics. Webs 2004. (Dexa 2004) (3). Num. 3. Zaragoza, España. IEEE Press. 2004. Pag. 132-137<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez:<br /> Towards a Tool for Ontology Engineering. World Automation Congress: Advances in Robotics, Manufacturing, Automation, Control, Soft Computing, Multimedia, Biomedicine, Image Processing and Financial Engineering. Vol. IV. World Automation Congress (). Sevilla, Spain. Tsi Press. 2004. Pag. 1-100. ISBN: 1-889335-20-7<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Towards a Tool for Ontology Engineering. Advances in Roboticas. Vol 4. Wac 2004. Wac (World Automation Congress) (). Sevilla, España. Tsi Press. 2004. Pag. 1-300<br /> <br /> Inmaculada Medina Bulo, Francisco Palomo Lozano, Jose Antonio Alonso Jimenez, Jose Luis Ruiz Reina:<br /> Verified Computer Algebra in Acl2 (Gröbner Basis Computation). Proceedings of the 7th Int. Conference on Artificial Intelligence and Symbolic Computation (Aisc 2004). 7th Int. Conference on Artificial Intelligence and Symbolic Computation, Aisc 2004 (). Linz, Austria. Springer-Verlag. 2004. Pag. 171-184<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> A Formal Proof of Dickson&#039;s Lemma in Acl2. Proceedings of the International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2003. International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (). Almaty, Kazakhstan. Springer-Verlag. 2003. Pag. 49-58<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formal Reasoning About Efficient Data Structures: a Case Study in Acl2. LOPSTR 2003, Preproceedings of the International Symposium of Logic Based Program Synthesis and Transformation. International Workshop on Logic Based Program Synthesis and Transformation (). Uppsala, Suecia. Katholieke Universiteit Leuven, Dep. of Computer Science. 2003. Pag. 97-112<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Formal Verification of Molecular Computational Models in Acl2: a Case Study. CAEPIA-TTIA 2003. X Conferencia de la Asocicación Española para la Inteligenciia Artificial. Asociación Española para la Inteligencia Artificial. Conferencia. Num. 10. San Sebastián. Universidad del País Vasco, Servicio Editorial. 2003. Pag. 235-240. ISBN: 84-8373-564-4<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Generalizing Logic Programs Via Subsumption. Eurocast 2003: Cast and Tools for Complexity in Biological, Physical and Engineering Systems: Extended Abstracts. International Conference on Computer Aided Systems Theory. Num. 9. Las Palmas de Gran Canaria. Universidad de las Palmas de Gran Canaria. 2003. Pag. 185-188. ISBN: 84-688-0820-2<br /> <br /> Antonia Mª Chavez Gonzalez, Joaquin Borrego Diaz, Jose Antonio Alonso Jimenez:<br /> Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases (Iea/Aie 2003). Libro de Actas del 16th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (Iea/Aie 2003). Iea/Aie 2003 (). Loughborough, United Kingdom. Springer, Berlín, Alemania. 2003. Pag. 789-798<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> A Generic Instantiation Tool and a Case Study: a Generic Multiset Theory. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 188-203<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Jorge D. Navarro Marín:<br /> A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases. Proc. of the 28th Annual Conference of IEEE Industrial Electronics Society. The 28th Annual Conference of IEEE Industrial Electronics Society. Sevilla, España. IEEE Press. 2002. Pag. 1806-1811<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo, Jorge D. Navarro Marín:<br /> A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases. Proceedings of the Iecon&#039;02. Iecon&#039;02 (). Sevilla, España. IEEE Industrial Electronic Society. 2002. Pag. 1806-1811. ISBN: 0-7803-7474-6<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> A Quasi-Metric for Machine Learning. 8th Ibero-American Conference on A.I. Ibero-American Conference on A.I. Num. 8. Sevilla. Springer, Berlín, Alemania. 2002. Pag. 193-203<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> A Theory About First-Order Terms in Acl2. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 78-100<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Desarrollo Formal y Verificación de Sistemas Proposicionales. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 1-12<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Progress Report: Term Dags Using Stobjs. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 101-108<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo:<br /> Towards a Practical Argumentative Reasoning With Qsd. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 111-120<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> Una Introducción al Análisis Formal de Conceptos en PVS. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 33-46<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Verificación Formal y Eficiencia: un Caso de Estudio Aplicado a la Unificación de Términos. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 77-90<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Verification in Acl2 of a Generic Framework to Synthesize SAT-Provers. Preproceedings of the International Workshop on Logic Based Program Development and Transformation. International Workshop on Logic Based Program Development and Transformation. Madrid, Spain. Facultad de Informática de la Universidad Politécnica de Madrid. 2002. Pag. 182-197<br /> <br /> Inmaculada Medina Bulo, Francisco Palomo Lozano, Jose Antonio Alonso Jimenez:<br /> A Certified Polynomial-Based Decision Procedure for Propositional Logic. International Conference on Theorem Proving in Higher Order Logics. International Conference on Theorem Proving in Higher Order Logics (14). Num. 14. Edimburgo (Escocia), Reino Unido. Division of Informatics of Edinburgh University. 2001. Pag. 297-312<br /> <br /> Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> Formalización del Razonamiento Ecuacional en una Lógica Computacional. Actas del I Encuentro de Matemáticos Andaluces. Encuentro de Matemáticos Andaluces. Num. 1. Sevilla, España. Universidad de Sevilla. Secretariado de Publicaciones. 2001. Pag. 41-50. ISBN: 84-472-0639-4<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Proximidad Entre Clausulas en Programacion Logica Inductiva. Actas del I Encuentro de Matemáticos Andaluces. Encuentro de Matemáticos Andaluces. Num. 1. Sevilla, España. Universidad de Sevilla. Secretariado de Publicaciones. 2001. Pag. 33-40. ISBN: 84-472-0639-4<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Proximidad Entre Cláusulas en Programación Lógica Inductiva. Actas del Encuentro de Matemáticos Andaluces: Comunicaciones. Encuentro de Matemáticos Andaluces (). Sevilla, España. Servicio de Publicaciones de la Universidad de Sevilla. 2001. Pag. 33-40. ISBN: 84-472-0290-9<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Verifying an Applicative ATP Using Multiset Relations. Eurocast 2001 Conference. Eurocast 2001 Conference. Las Palmas de Gran Canaria. 0. 2001. Pag. 616-626<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> A Mechanical Proof of Knuth-Bendix Critical Pair Theorem (Using Acl2). Proceedings of the Third International Workshop on First-Order Theorem Proving. First-Order Theorem Proving (3). Num. 3. ST Andrews, Scotland. Fachberichte Informatik, Universitat Koblenz-Landau. 2000. Pag. 206-216<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> A Topological Study of the Upward Refinement Operators on ILP. ILP 2000 - Work in Progress Reports. Inductive Logic Programming 10th International Conference, ILP 2000. Londres, Reino Unido. James Cussens - Alan Frisch (Eds.). 2000. Pag. 120-137<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formalizing Rewriting in the Acl2 Theorem Prover. Artificial Intelligence and Symbolic Computation, Aisc 2000, Revised Papers. Int. Conference on Artificial Intelligence and Symbolic Computation (). Madrid, España. Springer-Verlag. 2000. Pag. 92-106<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Multiset Relations: a Tool for Proving Termination. Proceedings of the Acl2 Workshop 2000. Second Acl2 Workshop (2). Num. 2. Austin, Texas, EEUU. University of Texas At Austin. 2000. Pag. 82-91<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Una Quasi-Metrica Basada en Subsuncion. IV Jornadas Cientificas en Tecnologias de la Informacion. Jornadas Cientificas en Tecnologias de la Informacion. Num. 4. Cadiz, España. Servicio de Publicaciones de la Universidad de Cádiz. 2000. Pag. 260-267<br /> <br /> Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado:<br /> Mechanical Verification of a Rule-Based Unification Algorithm in the Boyer-Moore Theorem Prover. Proc. of Joint Conference on Declarative Programming. Joint Conference on Declarative Programming. L&#039;aquila, Italia. 1999. Pag. 289-304<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Razonamiento Automático en Sistemas de Representación del Conocimiento (y su Relación con la Enseñanza de la Inteligencia Artificial). IV Jornades Sobre L&#039;ensenyament Universitari de la Infomàtica. IV Jornadas Sobre la Enseñanza Universitaria de la Informatica (Jenui&#039;98) (). Andorra. Enginyeria I Arquitectura la Salle. 1998. Pag. 289-296<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Verificación Automática de Sistemas de Razonamiento (Aplicación a la Enseñanza de la Inteligencia Artificial). IV Jornades Sobre L&#039;ensenyament Universitari de la Infomàtica. IV Jornadas Sobre la Enseñanza Universitaria de la Informatica (Jenui&#039;98) (). Andorra. Enginyeria I Arquitectura la Salle. 1998. Pag. 297-304<br /> <br /> Juan Jose Arrabal Parrilla, Delia Balbontin Noval, Jose Antonio Alonso Jimenez, Francisco Felix Lara Martin, Francisco Jesus Martin Mateos, Mario Jesus Perez Jimenez, Jose Luis Ruiz Reina:<br /> Gti: una Herramienta de Edición de Cursos Adaptativos. Actas del XIII Congreso Nacional de Ingenieria de Proyectos. Journees Détudes Comparatives Franco- Hispano- Italiannes. Num. 1. Burdeos, Francia. 1997. Pag. 627-634<br /> <br /> Rodrigo Fernandez Carrion, Juan Jose Arrabal Parrilla, Jose Antonio Alonso Jimenez:<br /> Hacia una Enseñanza Permanente y Automatizada: Www y Evaluación Automática con Gti. International Congress on Historical Information Systems. International Congress on Historical Information Systems (). Vitoria. 1997. Pag. 1-1<br /> <br /> Delia Balbontin Noval, Mª Luisa de la Vega Royo, Jose Antonio Alonso Jimenez, Juan Jose Arrabal Parrilla:<br /> Aprende Matemáticas. Actas del Primer Encuentro de Informática Educativa: Edie. Primer Encuentro de Informática Educativa (Edie) (). Cees (Madrid). Asociacion para el Desarrollo de la Informatica Educativa. 1994. Pag. 20-25<br /> <br /> Delia Balbontin Noval, Jose Antonio Alonso Jimenez, Juan Jose Arrabal Parrilla, Francisco Javier Herrera Govantes:<br /> Especificación Formal de Bases de Datos con un Demostrador Automático de Teoremas. Actas del II Congreso Nacional de Programación Declarativa. Congreso Nacional de Programación Declarativa. Num. 2. Sin Editorial. 1993. Pag. 343-344<br /> <br /> Delia Balbontin Noval, Juan Jose Arrabal Parrilla, Jose Antonio Alonso Jimenez, Francisco Javier Herrera Govantes:<br /> Automated Proofs in Group Theory With Otter. Proceedings of the Fith International Symposium on Knowledge Engineering. Fifth International Symposium on Knowledge Engineering (). Sevilla. Rank-Xerox. 1992. Pag. 326-331<br /> <br /> Delia Balbontin Noval, Jose Antonio Alonso Jimenez, Juan Jose Arrabal Parrilla, Francisco Javier Herrera Govantes:<br /> Razonamiento Automático en Lógica de Primer Orden. Actas del VIII Congreso de Lenguajes Naturales y Lenguajes Formales. VIII Congreso de Lenguajes Naturales y Lenguajes Formales (). Gerona (España). 1992. Pag. 165-172<br /> <br /> Jose Antonio Alonso Jimenez, Emilio Briales Morales, Agustin Riscos:<br /> Preuve Automatique Dans Le Calcul Propositionnel Et Les Logiques Trivalentes. Computational Topology and Geometry and Computation in Teaching Mathematics. Computational Topology and Geometry and Computation in Teaching of Mathematics. Num. 1. Sevilla. Servicio de Publicaciones de la Universidad de Sevilla. 1990. Pag. 15-24. ISBN: 84-7405-639-X<br /> <br /> Jose Antonio Alonso Jimenez, Emilio Briales Morales:<br /> Lógicas Polivalentes y Bases de Gröbner. V Congreso de Lenguajes Naturales y Lenguajes Formales. Congreso de Lenguajes Naturales y Lenguajes Formales (5). Num. 5. Barcelona, España. Universidad Barcelona. 1989. Pag. 307-315<br /> <br /> Tesis dirigidas:<br /> Director/a: Jose Antonio Alonso Jimenez, Doctorando: Maria Jose Hidalgo Doblado:<br /> Teoría Computacional (en PVS) de la Programación Lógica y del Análisis Formal de Conceptos., 2004, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director/a: Jose Antonio Alonso Jimenez, Doctorando: Inmaculada Medina Bulo:<br /> Verificación Formal en Acl2 del Algoritmo de Buchberger, 2003, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director/a: Jose Antonio Alonso Jimenez, Doctorando: Miguel Angel Gutierrez Naranjo:<br /> Operadores de Generalizacion para el Aprendizaje Clausal, 2002, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director/a: Jose Antonio Alonso Jimenez, Doctorando: Francisco Jesus Martin Mateos:<br /> Teoría Computacional (en Acl2) Sobre Cálculos Proposicionales, 2001, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director/a: Jose Antonio Alonso Jimenez, Doctorando: Jose Luis Ruiz Reina:<br /> Una Teoría Computacional Acerca de la Lógica Ecuacional (Formalización en Acl2 y Demostración Automática de Sus Propiedades), 2000, Ciencias de la Computacion e Inteligencia Artificial</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Publications&diff=14 2008-04-15T18:21:46Z

<p>WikiSysop: New page: == Libros == Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz: &#039;&#039;Agentes Inteligentes: una Aproximación desde la Lógica Computacional&#039;&#039;. Sevilla, España. Editorial Kronos. 2002. 127. I...</p> <hr /> <div>== Libros ==<br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz: &#039;&#039;Agentes Inteligentes: una Aproximación desde la Lógica Computacional&#039;&#039;. Sevilla, España. Editorial Kronos. 2002. 127. ISBN 84-86273-59-5<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz: &#039;&#039;Deducción Automática&#039;&#039;. Sevilla. Editorial Kronos. 2002. 1004. ISBN 84-86273-58-7<br /> <br /> Jose Antonio Alonso Jimenez, Jose Luis Ruiz Reina, Joaquin Borrego Diaz: &#039;&#039;Curso Práctico de Teoría de Conjuntos&#039;&#039;. Sevilla. La Ñ. 1998. 344. ISBN 84-89524-45-9<br /> <br /> Jose Luis Ruiz Reina, Joaquin Borrego Diaz, Jose Antonio Alonso Jimenez, Mario Jesus Perez Jimenez:<br /> Curso Práctico de Teoría de Conjuntos. Sevilla. La Ñ. 1998. 344. ISBN: 84-89524-45-9<br /> <br /> Capítulos en Libros<br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez:<br /> Logic Databases and Inconsistgency Handling. Encyclopedia of Databases Technologies and Applications. Hershey (Pennsylvania), Estados Unidos. Idea Group Reference. Vol. 1. 2006. Pag. 336-340. ISBN: 1-59140-560-2<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Formal Verification of Molecular Computational Models in Acl2: a Case Study. CAEPIA-TTIA 2003. San Sebastián. Universidad del País Vasco. Vol. 2. 2003. Pag. 235-244. ISBN: 84-8373-564-4<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Generalizing Logic Programs Via Subsumption. Eurocast 2003 - Cast and Tools for Complexity in Biological, Physical and Engineering Systems (Extended Abstracts). Las Palmas de Gran Canaria, España. Iuctc Universidad de las Palmas de Gran Canaria. Vol. 1. 2003. Pag. 185-188. ISBN: 84-688-0820-2<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Termination in Acl2 Using Multiset Relation. Thirty Five Years of Automating Mathematics. Dordrecht, Holanda. Kluwer Academic Publishers. 2003. Pag. 217-245. ISBN: 1-4020-1656-5<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Jorge D. Navarro Marín:<br /> A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases. IECON 2002. Sevilla, España. IEEE Industrial Electronic Society. 2002. Pag. 1806-1811. ISBN: 0-7803-7475-4<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez:<br /> Deduccion Automatica en Anillos Ternarios: Algunos Métodos de Procesamiento del Conocimiento Matemático. Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 23-32. ISBN: 84-472-0290-9<br /> <br /> Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos:<br /> Formalización del Razonamiento Ecuacional en una Lógica Computacional. Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 41-50. ISBN: 84-472-0290-9<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Proximidad Entre Clausulas en Programacion Logica Inductiva. Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 33-40. ISBN: 84-472-0290-9<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez:<br /> Estrategias para la Demostración Automática de Teoremas. Libro de Actas Cinte&#039;00. Cadiz. Servicio de Publicaciones de la Universidad de Cádiz. 2000. Pag. 276-283<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Interpretación Reactiva de Sistemas Basados en Conocimiento. Actas del IV Congreso Isko España. Granada. 1999. Pag. 187-193. ISBN: 84-699-0289-X<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Razonamiento Automático en Sistemas de Representación del Conocimiento (y su Relación con la Enseñanza de la Inteligencia Artificial). IV Jornades Sobre L&#039;ensenyament Universitari de la Informatica (Jenui 98). Barcelona, España. Enginyeria I Arquitectura la Salle. 1998. Pag. 289-296. ISBN: 84-922538-3-5<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Verificación Automática de Sistemas de Razonamiento (Aplicación a la Enseñanza de la Inteligencia Artificial). IV Jornades Sobre L&#039;ensenyament Universitari de la Informatica (Jenui 98). Barcelona, España. Enginyeria I Arquitectura la Salle. 1998. Pag. 297-304. ISBN: 84-922538-3-5<br /> <br /> Juan Jose Arrabal Parrilla, Delia Balbontin Noval, Jose Antonio Alonso Jimenez, Francisco Felix Lara Martin, Francisco Jesus Martin Mateos, Mario Jesus Perez Jimenez, Jose Luis Ruiz Reina:<br /> Gti: una Herramienta de Edición de Cursos Adaptativos. Actas del XIII Congreso Nacional de Ingeniería de Proyectos. Sevilla. Antonio F. Martin Navarro. 1997. Pag. 627-634. ISBN: 84-88783-30-2<br /> <br /> Juan Jose Arrabal Parrilla, Delia Balbontin Noval, Jose Antonio Alonso Jimenez, Francisco Felix Lara Martin:<br /> Gti: una Herramienta de Edición de Cursos Adaptativos. Actas del XIII Congreso Nacional de Ingeniería de Proyectos. Sevilla. Antonio F. Martin Navarro. 1997. Pag. 627-634. ISBN: 84-88783-30-2<br /> <br /> Luis Laita, Eugenio Roanes-Lozano, Jose Antonio Alonso Jimenez, Emilio Briales Morales:<br /> Verificación Algebraica de Sbc Basada en la Lógica Trievaluada, Teoría e Implementación. I Jornadas Sobre Inteligencia Artificial, Control y Sistemas Expertos. Madrid, España. Servicio de Publicaciones de la Universidad de Alcala. 1996. Pag. 241-255. ISBN: 84-8138-147-0<br /> <br /> Jose Antonio Alonso Jimenez, Alejandro Fernandez Margarit, Mario Jesus Perez Jimenez:<br /> Razonamiento Automático. Lógica Formal : Orígenes, Métodos y Aplicaciones. Sevilla. Kronos S.A. 1995. Pag. 189-211. ISBN: 84-88620-56-X<br /> <br /> Juan Jose Arrabal Parrilla, Jose Antonio Alonso Jimenez, Alejandro Fernandez Margarit, Mario Jesus Perez Jimenez:<br /> Automatización de la Aritmética. Lenguajes Naturales y Lenguajes Formales, X. Barcelona. Ppu: Promociones y Publicaciones Universitarias. 1994. Pag. 167-182. ISBN: 84-477-0396-7<br /> <br /> Publicaciones en Revistas<br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> A Formally Verified Prover for the Alc Description Logic. Lecture Notes in Computer Science. Vol. 4732. 2007. Pag. 135-150<br /> <br /> Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado:<br /> Formal Correctness of a Quadratic Unification Algorithm. Journal of Automated Reasoning. Vol. 37. Núm. 1-2. 2006. Pag. 67-92<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Francisco Jesus Martin Mateos:<br /> Foundational Challenges in Automated Semantic Web Data and Ontology Cleaning. IEEE Intelligent Systems. Vol. 21. Núm. 1. 2006. Pag. 42-52<br /> <br /> Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado:<br /> Proof Pearl: a Formal Proof of Higman S Lemma in Acl2. Lecture Notes in Computer Science. Vol. 3603. 2005. Pag. 358-372<br /> <br /> Manuel Palomo Duarte, Jose Antonio Alonso Jimenez, Francisco Jesus Martin Mateos:<br /> Rete Algorithm Applied to Robotic Soccer. Lecture Notes in Computer Science. Vol. 3643. 2005. Pag. 571-576<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formal Reasoning About Efficient Data Structures: a Case Study in Acl2. Lecture Notes in Computer Science. Vol. 3018. 2004. Pag. 75-91<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Formal Verification of a Generic Framework to Synthesize SAT-Provers. Journal of Automated Reasoning. Vol. 32. Núm. 4. 2004. Pag. 287-313<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Formal Verification of Molecular Computational Models in Acl2: a Case Study. Lecture Notes in Computer Science. Vol. 3040. 2004. Pag. 344-353<br /> <br /> Antonia Mª Chavez Gonzalez, Joaquin Borrego Diaz, Jose Antonio Alonso Jimenez:<br /> Ontology Cleaning By Mereotopological Reasoning. Proceedings. 2004. Pag. 132-137<br /> <br /> Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> Verification of the Formal Concept Analysis. RACSAM. Revista de la Real Academia de Ciencias. Serie a: Matemáticas. Vol. 98. 2004. Pag. 3-16<br /> <br /> Inmaculada Medina Bulo, Francisco Palomo Lozano, Jose Antonio Alonso Jimenez, Jose Luis Ruiz Reina:<br /> Verified Computer Algebra in Acl2 (Grobner Bases Computation). Lecture Notes in Computer Science. Vol. 3249. 2004. Pag. 171-184<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> A Formal Proof of Dickson&#039;s Lemma in Acl2. Lecture Notes in Computer Science. Vol. 2850. 2003. Pag. 49-58<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Generalizing Programs Via Subsumption. Lecture Notes in Computer Science. Vol. 2809. 2003. Pag. 115-126<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo, Jorge D. Navarro Marín:<br /> Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases. Lecture Notes in Computer Science. Vol. 2718. 2003. Pag. 789-798<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Verification in Acl2 of a Generic Framework to Synthesize SAT-Provers. Lecture Notes in Computer Science. Vol. 2664. 2003. Pag. 182-198<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> A Quasi-Metric for Machine Learning. Lecture Notes in Computer Science. Vol. 2527. 2002. Pag. 193-203<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formal Proofs About Rewriting Using Acl2. Annals of Mathematics and Artificial Intelligence . Vol. 36. Núm. 3. 2002. Pag. 239-262<br /> <br /> Inmaculada Medina Bulo, Francisco Palomo Lozano, Jose Antonio Alonso Jimenez:<br /> A Certified Polynomial-Based Decision Procedure for Propositional Logic. Lecture Notes in Computer Science. Núm. 2152. 2001. Pag. 297-312<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formalizing Rewriting in the Acl2 Theorem Prover. Lecture Notes in Computer Science. Vol. 1930. 2001. Pag. 92-106<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Verifying an Applicative ATP Using Multiset Relations. Lecture Notes in Computer Science. Vol. 2178. 2001. Pag. 612-626<br /> <br /> J. Chazarain, Agustin Riscos, Jose Antonio Alonso Jimenez, Emilio Briales Morales:<br /> Multivalued-Logic and Gröbner Bases With Applications to Modal Logic. Journal of Symbolic Computation . Vol. 11. 1991. Pag. 181-194<br /> <br /> Libros de Actas<br /> Jose Antonio Alonso Jimenez, Jose Luis Ruiz Reina, Joaquin Borrego Diaz, Manuel Ojeda Aciego:<br /> Ideia 2002: I Taller Iberoamericano Sobre Deducción Automática e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Sevilla, España. Departamento de Ciencias de la Computacion e Inteligencia Artificial. Universidad de Sevilla. 2002<br /> <br /> Aportaciones a Congresos<br /> Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> A Formally Verified Proof (in PVS) of the Strong Completeness Theorem Of Propositional Sld-Resolution. Cast and Tools for Robotics, Vehicular and Communication Systems. Computer Aided Systems Theory, Eurocast 2005 (10). Num. 10. Las Palmas de Gran Canaria, España. Actas del Congreso. 2005. Pag. 83-86<br /> <br /> Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado:<br /> Proof Pearl: a Formal Proof of Higman&#039;s Lemma in Acl2. Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics (18). Num. 18. Oxford, Reino Unido. Springer-Verlag. 2005. Pag. 358-372. ISBN: 3-540-28372-2<br /> <br /> Manuel Palomo Duarte, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez:<br /> Rete Algorithm Applied to Robotic Soccer. Cast and Tools for Robotics, Vehicular and Communication Systems. Computer Aided Systems Theory, Eurocast 2005 (10). Num. 10. Las Palmas de Gran Canaria, España. Actas del Congreso. 2005. Pag. 280-283<br /> <br /> Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado:<br /> A Formally Verified Quadratic Unification Algorithm. Proceedings of the Fifth International Workshop on the Acl2 Theorem Prover and Its Applications (Acl2-2004). Fifth International Workshop on the Acl2 Theorem Prover and Its Applications (Acl2-2004) (5). Num. 5. Austin, Texas, EEUU. Unicersity of Austin. 2004. Pag. 1-32<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Generalizing Logic Programs Via Subsumption. Computer Aided System Theory - Eurocast 2003: 9th International Workshop on Computer Aided Systems Theory [recurso Electrónico]. International Workshop on Computer Aided Systems Theory. Num. 9. Las Palmas de Gran Canaria. Springer-Verlag. 2004. Pag. 115-126. ISBN: 3-540-20221-8<br /> <br /> Antonia Mª Chavez Gonzalez, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Ontology Cleaning By Mereotopological Reasoning. Database and Expert Systems Applications. Webs 2004. International Workshop on Web Semantics. Webs 2004. (Dexa 2004) (3). Num. 3. Zaragoza, España. IEEE Press. 2004. Pag. 132-137<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez:<br /> Towards a Tool for Ontology Engineering. World Automation Congress: Advances in Robotics, Manufacturing, Automation, Control, Soft Computing, Multimedia, Biomedicine, Image Processing and Financial Engineering. Vol. IV. World Automation Congress (). Sevilla, Spain. Tsi Press. 2004. Pag. 1-100. ISBN: 1-889335-20-7<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Towards a Tool for Ontology Engineering. Advances in Roboticas. Vol 4. Wac 2004. Wac (World Automation Congress) (). Sevilla, España. Tsi Press. 2004. Pag. 1-300<br /> <br /> Inmaculada Medina Bulo, Francisco Palomo Lozano, Jose Antonio Alonso Jimenez, Jose Luis Ruiz Reina:<br /> Verified Computer Algebra in Acl2 (Gröbner Basis Computation). Proceedings of the 7th Int. Conference on Artificial Intelligence and Symbolic Computation (Aisc 2004). 7th Int. Conference on Artificial Intelligence and Symbolic Computation, Aisc 2004 (). Linz, Austria. Springer-Verlag. 2004. Pag. 171-184<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> A Formal Proof of Dickson&#039;s Lemma in Acl2. Proceedings of the International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2003. International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (). Almaty, Kazakhstan. Springer-Verlag. 2003. Pag. 49-58<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formal Reasoning About Efficient Data Structures: a Case Study in Acl2. LOPSTR 2003, Preproceedings of the International Symposium of Logic Based Program Synthesis and Transformation. International Workshop on Logic Based Program Synthesis and Transformation (). Uppsala, Suecia. Katholieke Universiteit Leuven, Dep. of Computer Science. 2003. Pag. 97-112<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Formal Verification of Molecular Computational Models in Acl2: a Case Study. CAEPIA-TTIA 2003. X Conferencia de la Asocicación Española para la Inteligenciia Artificial. Asociación Española para la Inteligencia Artificial. Conferencia. Num. 10. San Sebastián. Universidad del País Vasco, Servicio Editorial. 2003. Pag. 235-240. ISBN: 84-8373-564-4<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Generalizing Logic Programs Via Subsumption. Eurocast 2003: Cast and Tools for Complexity in Biological, Physical and Engineering Systems: Extended Abstracts. International Conference on Computer Aided Systems Theory. Num. 9. Las Palmas de Gran Canaria. Universidad de las Palmas de Gran Canaria. 2003. Pag. 185-188. ISBN: 84-688-0820-2<br /> <br /> Antonia Mª Chavez Gonzalez, Joaquin Borrego Diaz, Jose Antonio Alonso Jimenez:<br /> Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases (Iea/Aie 2003). Libro de Actas del 16th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (Iea/Aie 2003). Iea/Aie 2003 (). Loughborough, United Kingdom. Springer, Berlín, Alemania. 2003. Pag. 789-798<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> A Generic Instantiation Tool and a Case Study: a Generic Multiset Theory. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 188-203<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Jorge D. Navarro Marín:<br /> A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases. Proc. of the 28th Annual Conference of IEEE Industrial Electronics Society. The 28th Annual Conference of IEEE Industrial Electronics Society. Sevilla, España. IEEE Press. 2002. Pag. 1806-1811<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo, Jorge D. Navarro Marín:<br /> A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases. Proceedings of the Iecon&#039;02. Iecon&#039;02 (). Sevilla, España. IEEE Industrial Electronic Society. 2002. Pag. 1806-1811. ISBN: 0-7803-7474-6<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> A Quasi-Metric for Machine Learning. 8th Ibero-American Conference on A.I. Ibero-American Conference on A.I. Num. 8. Sevilla. Springer, Berlín, Alemania. 2002. Pag. 193-203<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> A Theory About First-Order Terms in Acl2. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 78-100<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Desarrollo Formal y Verificación de Sistemas Proposicionales. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 1-12<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Progress Report: Term Dags Using Stobjs. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Third International Workshop on the Acl2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 101-108<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo:<br /> Towards a Practical Argumentative Reasoning With Qsd. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 111-120<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> Una Introducción al Análisis Formal de Conceptos en PVS. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 33-46<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Verificación Formal y Eficiencia: un Caso de Estudio Aplicado a la Unificación de Términos. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 77-90<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Verification in Acl2 of a Generic Framework to Synthesize SAT-Provers. Preproceedings of the International Workshop on Logic Based Program Development and Transformation. International Workshop on Logic Based Program Development and Transformation. Madrid, Spain. Facultad de Informática de la Universidad Politécnica de Madrid. 2002. Pag. 182-197<br /> <br /> Inmaculada Medina Bulo, Francisco Palomo Lozano, Jose Antonio Alonso Jimenez:<br /> A Certified Polynomial-Based Decision Procedure for Propositional Logic. International Conference on Theorem Proving in Higher Order Logics. International Conference on Theorem Proving in Higher Order Logics (14). Num. 14. Edimburgo (Escocia), Reino Unido. Division of Informatics of Edinburgh University. 2001. Pag. 297-312<br /> <br /> Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina:<br /> Formalización del Razonamiento Ecuacional en una Lógica Computacional. Actas del I Encuentro de Matemáticos Andaluces. Encuentro de Matemáticos Andaluces. Num. 1. Sevilla, España. Universidad de Sevilla. Secretariado de Publicaciones. 2001. Pag. 41-50. ISBN: 84-472-0639-4<br /> <br /> Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Proximidad Entre Clausulas en Programacion Logica Inductiva. Actas del I Encuentro de Matemáticos Andaluces. Encuentro de Matemáticos Andaluces. Num. 1. Sevilla, España. Universidad de Sevilla. Secretariado de Publicaciones. 2001. Pag. 33-40. ISBN: 84-472-0639-4<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Proximidad Entre Cláusulas en Programación Lógica Inductiva. Actas del Encuentro de Matemáticos Andaluces: Comunicaciones. Encuentro de Matemáticos Andaluces (). Sevilla, España. Servicio de Publicaciones de la Universidad de Sevilla. 2001. Pag. 33-40. ISBN: 84-472-0290-9<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Verifying an Applicative ATP Using Multiset Relations. Eurocast 2001 Conference. Eurocast 2001 Conference. Las Palmas de Gran Canaria. 0. 2001. Pag. 616-626<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> A Mechanical Proof of Knuth-Bendix Critical Pair Theorem (Using Acl2). Proceedings of the Third International Workshop on First-Order Theorem Proving. First-Order Theorem Proving (3). Num. 3. ST Andrews, Scotland. Fachberichte Informatik, Universitat Koblenz-Landau. 2000. Pag. 206-216<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> A Topological Study of the Upward Refinement Operators on ILP. ILP 2000 - Work in Progress Reports. Inductive Logic Programming 10th International Conference, ILP 2000. Londres, Reino Unido. James Cussens - Alan Frisch (Eds.). 2000. Pag. 120-137<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Formalizing Rewriting in the Acl2 Theorem Prover. Artificial Intelligence and Symbolic Computation, Aisc 2000, Revised Papers. Int. Conference on Artificial Intelligence and Symbolic Computation (). Madrid, España. Springer-Verlag. 2000. Pag. 92-106<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Multiset Relations: a Tool for Proving Termination. Proceedings of the Acl2 Workshop 2000. Second Acl2 Workshop (2). Num. 2. Austin, Texas, EEUU. University of Texas At Austin. 2000. Pag. 82-91<br /> <br /> Miguel Angel Gutierrez Naranjo, Jose Antonio Alonso Jimenez, Joaquin Borrego Diaz:<br /> Una Quasi-Metrica Basada en Subsuncion. IV Jornadas Cientificas en Tecnologias de la Informacion. Jornadas Cientificas en Tecnologias de la Informacion. Num. 4. Cadiz, España. Servicio de Publicaciones de la Universidad de Cádiz. 2000. Pag. 260-267<br /> <br /> Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado:<br /> Mechanical Verification of a Rule-Based Unification Algorithm in the Boyer-Moore Theorem Prover. Proc. of Joint Conference on Declarative Programming. Joint Conference on Declarative Programming. L&#039;aquila, Italia. 1999. Pag. 289-304<br /> <br /> Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina:<br /> Razonamiento Automático en Sistemas de Representación del Conocimiento (y su Relación con la Enseñanza de la Inteligencia Artificial). IV Jornades Sobre L&#039;ensenyament Universitari de la Infomàtica. IV Jornadas Sobre la Enseñanza Universitaria de la Informatica (Jenui&#039;98) (). Andorra. Enginyeria I Arquitectura la Salle. 1998. Pag. 289-296<br /> <br /> Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos:<br /> Verificación Automática de Sistemas de Razonamiento (Aplicación a la Enseñanza de la Inteligencia Artificial). IV Jornades Sobre L&#039;ensenyament Universitari de la Infomàtica. IV Jornadas Sobre la Enseñanza Universitaria de la Informatica (Jenui&#039;98) (). Andorra. Enginyeria I Arquitectura la Salle. 1998. Pag. 297-304<br /> <br /> Juan Jose Arrabal Parrilla, Delia Balbontin Noval, Jose Antonio Alonso Jimenez, Francisco Felix Lara Martin, Francisco Jesus Martin Mateos, Mario Jesus Perez Jimenez, Jose Luis Ruiz Reina:<br /> Gti: una Herramienta de Edición de Cursos Adaptativos. Actas del XIII Congreso Nacional de Ingenieria de Proyectos. Journees Détudes Comparatives Franco- Hispano- Italiannes. Num. 1. Burdeos, Francia. 1997. Pag. 627-634<br /> <br /> Rodrigo Fernandez Carrion, Juan Jose Arrabal Parrilla, Jose Antonio Alonso Jimenez:<br /> Hacia una Enseñanza Permanente y Automatizada: Www y Evaluación Automática con Gti. International Congress on Historical Information Systems. International Congress on Historical Information Systems (). Vitoria. 1997. Pag. 1-1<br /> <br /> Delia Balbontin Noval, Mª Luisa de la Vega Royo, Jose Antonio Alonso Jimenez, Juan Jose Arrabal Parrilla:<br /> Aprende Matemáticas. Actas del Primer Encuentro de Informática Educativa: Edie. Primer Encuentro de Informática Educativa (Edie) (). Cees (Madrid). Asociacion para el Desarrollo de la Informatica Educativa. 1994. Pag. 20-25<br /> <br /> Delia Balbontin Noval, Jose Antonio Alonso Jimenez, Juan Jose Arrabal Parrilla, Francisco Javier Herrera Govantes:<br /> Especificación Formal de Bases de Datos con un Demostrador Automático de Teoremas. Actas del II Congreso Nacional de Programación Declarativa. Congreso Nacional de Programación Declarativa. Num. 2. Sin Editorial. 1993. Pag. 343-344<br /> <br /> Delia Balbontin Noval, Juan Jose Arrabal Parrilla, Jose Antonio Alonso Jimenez, Francisco Javier Herrera Govantes:<br /> Automated Proofs in Group Theory With Otter. Proceedings of the Fith International Symposium on Knowledge Engineering. Fifth International Symposium on Knowledge Engineering (). Sevilla. Rank-Xerox. 1992. Pag. 326-331<br /> <br /> Delia Balbontin Noval, Jose Antonio Alonso Jimenez, Juan Jose Arrabal Parrilla, Francisco Javier Herrera Govantes:<br /> Razonamiento Automático en Lógica de Primer Orden. Actas del VIII Congreso de Lenguajes Naturales y Lenguajes Formales. VIII Congreso de Lenguajes Naturales y Lenguajes Formales (). Gerona (España). 1992. Pag. 165-172<br /> <br /> Jose Antonio Alonso Jimenez, Emilio Briales Morales, Agustin Riscos:<br /> Preuve Automatique Dans Le Calcul Propositionnel Et Les Logiques Trivalentes. Computational Topology and Geometry and Computation in Teaching Mathematics. Computational Topology and Geometry and Computation in Teaching of Mathematics. Num. 1. Sevilla. Servicio de Publicaciones de la Universidad de Sevilla. 1990. Pag. 15-24. ISBN: 84-7405-639-X<br /> <br /> Jose Antonio Alonso Jimenez, Emilio Briales Morales:<br /> Lógicas Polivalentes y Bases de Gröbner. V Congreso de Lenguajes Naturales y Lenguajes Formales. Congreso de Lenguajes Naturales y Lenguajes Formales (5). Num. 5. Barcelona, España. Universidad Barcelona. 1989. Pag. 307-315<br /> <br /> Tesis dirigidas:<br /> Director/a: Jose Antonio Alonso Jimenez, Doctorando: Maria Jose Hidalgo Doblado:<br /> Teoría Computacional (en PVS) de la Programación Lógica y del Análisis Formal de Conceptos., 2004, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director/a: Jose Antonio Alonso Jimenez, Doctorando: Inmaculada Medina Bulo:<br /> Verificación Formal en Acl2 del Algoritmo de Buchberger, 2003, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director/a: Jose Antonio Alonso Jimenez, Doctorando: Miguel Angel Gutierrez Naranjo:<br /> Operadores de Generalizacion para el Aprendizaje Clausal, 2002, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director/a: Jose Antonio Alonso Jimenez, Doctorando: Francisco Jesus Martin Mateos:<br /> Teoría Computacional (en Acl2) Sobre Cálculos Proposicionales, 2001, Ciencias de la Computacion e Inteligencia Artificial<br /> <br /> Director/a: Jose Antonio Alonso Jimenez, Doctorando: Jose Luis Ruiz Reina:<br /> Una Teoría Computacional Acerca de la Lógica Ecuacional (Formalización en Acl2 y Demostración Automática de Sus Propiedades), 2000, Ciencias de la Computacion e Inteligencia Artificial</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Projects&diff=13 2008-04-15T18:08:22Z

<p>WikiSysop: </p> <hr /> <div>* 2004-08 Sistemas verificados para el razonamiento en la web semántica. (MEC TIN2004-038844).<br /> *: Directed by José A. Alonso Jiménez.<br /> <br /> * 2003-06 Development and verification of Intelligent Systems with logic and algebraic technics. Evolution of information systems. Theory and interdisciplinary applications (en tramitación)<br /> *: Directed by Luis M. Laita de la Rica.<br /> <br /> * 2000-03 Development and formal verification of reasoning systems (DGI TIC2000-1368-C03-02)<br /> *: Directed by José A. Alonso Jiménez.<br /> <br /> * 2000-03 Development and verification of Expert Systems with logic and algebraic technics. Theory and interdisciplinary applications (DGI TIC2000-1368-C03)<br /> *: Directed by Luis M. Laita de la Rica.<br /> <br /> * 1997-00 Verification of knowledge bases and reasoning systems (DGES PB96-0098-C04-04)<br /> *: Directed by José A. Alonso Jiménez.<br /> <br /> * 1997-00 Verification and automatic extraction of conclusions in knowledge and information systems. Theoretical foundations and implementation (DGES PB96-0098-C04)<br /> *: Directed by Luis M. Laita de la Rica.<br /> <br /> * 1997-00 Classification of the computable functions by means of arithmetic specifications: methodology and design (DGES PB96-1345)<br /> *: Directed by Alejandro Fernández Margarit.<br /> <br /> * 1995-96 Verification of expert systems: formal models and implementation (DGICYT PB 94-0424)<br /> *: Directed by Luis M. Laita de la Rica.<br /> <br /> * 1992-93 Verification of knowledge bases in expert systems II (CICYT TIC 92-1191)<br /> *: Directed by Luis M. Laita de la Rica.<br /> <br /> * 1992-93 A model for verification of expert systems (CICYT TIC 92-0069)<br /> *: Directed by Luis M. Laita de la Rica.<br /> <br /> * 1990-91 Verification of knowledge bases in expert systems II (PRONTIC 90-2738)<br /> *: Directed by Luis M. Laita de la Rica.</div>

WikiSysop https://www.glc.us.es/web/index.php?title=Projects&diff=12 2008-04-15T18:07:58Z

<p>WikiSysop: New page: * 2004-08 Sistemas verificados para el razonamiento en la web semántica. (MEC TIN2004-038844). *: Directed by José A. Alonso Jiménez. * 2003-06 Development and verification of Intelli...</p> <hr /> <div>* 2004-08 Sistemas verificados para el razonamiento en la web semántica. (MEC TIN2004-038844).<br /> *: Directed by José A. Alonso Jiménez.<br /> <br /> * 2003-06 Development and verification of Intelligent Systems with logic and algebraic technics. Evolution of information systems. Theory and interdisciplinary applications (en tramitación)<br /> *: Directed by Luis M. Laita de la Rica.<br /> <br /> * 2000-03 Development and formal verification of reasoning systems (DGI TIC2000-1368-C03-02)<br /> *: Directed by José A. Alonso Jiménez.<br /> <br /> * 2000-03 Development and verification of Expert Systems with logic and algebraic technics. Theory and interdisciplinary applications (DGI TIC2000-1368-C03)<br /> *: Directed by Luis M. Laita de la Rica.<br /> <br /> * 1997-00 Verification of knowledge bases and reasoning systems (DGES PB96-0098-C04-04)<br /> *: Directed by José A. Alonso Jiménez.<br /> <br /> * 1997-00 Verification and automatic extraction of conclusions in knowledge and information systems. Theoretical foundations and implementation (DGES PB96-0098-C04)<br /> *: Directed by Luis M. Laita de la Rica.<br /> <br /> * 1997-00 Classification of the computable functions by means of arithmetic specifications: methodology and design (DGES PB96-1345)<br /> *: Directed by Alejandro Fernández Margarit.<br /> <br /> * 1995-96 Verification of expert systems: formal models and implementation (DGICYT PB 94-0424)<br /> *: Directed by Luis M. Laita de la Rica.<br /> <br /> * 1992-93 Verification of knowledge bases in expert systems II (CICYT TIC 92-1191)<br /> *: Directed by Luis M. Laita de la Rica.<br /> <br /> * 1992-93 A model for verification of expert systems (CICYT TIC 92-0069)<br /> *: Directed by Luis M. Laita de la Rica.<br /> <br /> * 1990-91 Verification of knowledge bases in expert systems II (PRONTIC 90-2738)<br /> Directed by Luis M. Laita de la Rica.</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=11 2008-04-15T18:03:17Z

<p>WikiSysop: </p> <hr /> <div>* navigation<br /> ** mainpage|mainpage<br /> ** Projects|Projects<br /> ** Group members|Members<br /> ** Publications|Publications<br /> ** Theories|Theories<br /> ** Related courses|Teaching<br /> ** recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=10 2008-04-15T18:01:02Z

<p>WikiSysop: </p> <hr /> <div>* navigation<br /> ** mainpage|mainpage<br /> ** Group members|Members<br /> ** recentchanges-url|recentchanges</div>

WikiSysop https://www.glc.us.es/web/index.php?title=MediaWiki:Sidebar&diff=9 2008-04-15T18:00:08Z

<p>WikiSysop: New page: * navigation ** mainpage|mainpage ** recentchanges-url|recentchanges</p> <hr /> <div>* navigation<br /> ** mainpage|mainpage<br /> ** recentchanges-url|recentchanges</div>

WikiSysop