Se presenta una manera de usar el programa de matemática dinámica GeoGebra, como medio para estimular la elaboración de conjeturas enla enseñanza y el aprendizaje de las matemáticas. Se usa la expresión general de la función cuadrática y se examina en la Vista Gráfica del GeoGebra la variación de sus parámetros para elaborar conjeturas que se demuestran algebraicamente. En el artículo, se hace uso del enfoque de los registros de representación semiótica de Duval.

Doctor en Ingeniería Eléctrica / Esta tesis presenta un método que permite que usuarios no expertos enseñen agentes a ejecutar tareas complejas durante tiempo de ejecución, con el principal propósito de acelerar la convergencia del aprendizaje y mejorar el desempeño final de las políticas aprendidas. En este sentido, se propone COrrective Advice Communicated by Humans (COACH), un framework interactivo para entrenar políticas con vagas correcciones respecto a las acciones ejecutadas, las cuales son cambios relativos de la magnitud de las acciones que están siendo ejecutadas. Así, los usuarios sugieren correcciones como: incrementar la fuerza, reducir la velocidad, ir más hacia la izquierda, etc. Inicialmente, se propone un esquema de aprendizaje que permite a humanos enseñar políticas de acciones continuas por medio de correcciones correctivas, para problemas de acciones de una dimensión. Se incluye en el framework de aprendizaje un módulo que representa las intenciones del profesor, el cual se basa en la historia pasada de las correcciones. Luego, el framework se extiende a problemas de acciones de más de una dimensión, incluso para casos en los que las correcciones del usuario no están en el mismo espacio de la política. Adicionalmente, el COACH propuesto es combinado con aprendizaje reforzado Policy Search con el fin de obtener la ventajas de ambas fuentes de información (correcciones humanas y funciones de recompensa) en el proceso de aprendizaje. Se proponen dos enfoques híbridos que combinan los dos enfoques, uno secuencial y uno simultáneo. Los resultados muestran que estos esquemas se benefician de las ventajas de cada uno de sus componentes, es decir se obtiene i) rápido progreso al principio del proceso de aprendizaje, y ii) aprendizaje robusto a errores humanos, junto con optimalidad local. Además, este enfoque híbrido es extendido para entrenar primitivas de movimiento. Así, las ventajas previamente mencionadas son extendidas para aprender también políticas representadas como Dynamic Movement Primitives (DMP) y Probabilistic Movement Primitives (ProMP), las cuales son convenientes para aprender trayectorias. El uso del enfoque propuesto es validado en muchos problemas tanto simulados como reales, con variadas características, recorriendo problemas de equilibrio, navegación con robots bípedos en el contexto del fútbol robótico, y también habilidades motoras con brazos robóticos en tareas como escritura de símbolos y el conocido juego "emboque". Los resultados muestran que el conocimiento de los usuarios no expertos puede apalancar procesos de aprendizaje de máquina, guiando hacia desempeños más altos con respecto a otros enfoques de aprendizaje de máquina interactivo y de aprendizaje reforzado, e incluso superando las capacidades de usuarios aprendiendo a tele-operar los agentes. Adicionalmente, los métodos presentados obtienen convergencias las cuales varían desde 3 hasta más de 40 veces más rápido que otras técnicas, dependiendo del problema.

Esta tesis tiene como objeto el estudio de dos temas principales: en primer lugar nos abocamos al estudio de una clase de cálculos de Gentzen, los hipersecuentes; y en segundo lugar, abordamos el estudio de ciertas lógicas a las que dan lugar las álgebras tetravalentes modales. Ambos temas quedarán relacionados, como veremos en el Capítulo III. Los hipersecuentes son una generalización natural de los secuentes ordinarios que resultan ser una herramienta muy adecuada para presentar formulaciones estilo Gentzen de diversas l´ogicas con la muy deseable propiedad de eliminación de corte (cut-elimination property). En los años recientes, el desarrollo de métodos para combinar lógicas ha recibido mucha atención, y las motivaciones para que esto suceda provienen de áreas tan disímiles como la Filosofía y las Ciencias de la Computación (ver, por ejemplo, [13] y [15]). El fibring categorial (tambi´en conocido como fibring algebraico) introducido en [55], ha demostrado ser una herramienta amplia y poderosa para combinar lógicas. Por otro lado, la clase TMA de las álgebras tetravalentes modales fue considerada por primera vez por Antonio Monteiro, y fueron estudiadas principalmente por I. Loureiro, A.V. Figallo, A. Ziliani y P. Landini. Posteriormente, J.M. Font y M. Rius en [31] se interesaron en las lógicas a las que dan lugar los aspectos reticulares de estas ´ágebras.Estos mismos autores introdujeron un cálculo de secuentes para una de estas lógicas, a saber, T ML. En el Capítulo II, presentamos un modo alternativo de formular cálculos de hipersecuentes mediante la introducción de metavariables para fórmulas, secuentes e hipersecuentes respectivamente, en el lenguaje objeto. Se introduce una categoría adecuada de cálculos de hipersecuentes y se definen ambos tipos de fibring: restringido y no restringido. Los morfismos introducidos resultar´an ser una novedosa noción de traducción entre lógicas la cual preserva meta-propiedades en un sentido fuerte. Finalmente, exploraremos algunas características de preservación, en particular mostraremos un resultado sobre la preservación por fibring de la propiedad de interpolación de Craig (CIP). En el Capítulo III, retomamos la cuestion de investigar diferentes aspectos lógicos de las TMAs. Considerando la implicación contrapositiva introducida por A. Figallo y P. Landini en [28], introducimos tres cálculos de Hilbert distintos para la lógica T ML, como así tambien, un sistema de tableau correcto y completo para la semántica de las TMAs. Los aspectos paraconsistentes de T ML tambi´en son analizados desde el punto de vista de las Logicas de la Inconsistencia Formal, introducidas por W. Carnielli y J. Marcos en [18], y posteriormente estudiadas en [17]. La lógica tetravalente modal normal T MLN es luego estudiada. Finalmente, probamos que ambas lógicas son sublógicas propias del cálculo proposicional clásico que no son maximales. En el Capitulo IV, mostramos que el cálculo de secuentes presentado por Font y Rius en [31] para T ML no tiene la propiedad de eliminación de corte. Formulamos, entonces, un cálculo de hipersecuentes correcto y completo con respecto a T ML que si tiene esta tan deseable propiedad. Finalmente, en el Capítulo V, motivados por el problema de enriquecer a T ML con una implicación deductiva, probamos que las álgebras tetravalentes modales de A. Monteiro enriquecidas con un complemento booleano coinciden con las álgebras de De Morgan enriquecidas con un complemento booleano, o equivalentemente, con las álgebras de Boole enriquecidas con una negación de De Morgan. Estas últimas son denominadas álgebras de Boole involutivas (o simétricas) (IBAs), introducidas por Gr. Moisil y principalmente estudiadas por A. Monteiro. Probamos que las IBAs son la contrapartida algebraica de la lógica modal S5 que satisface ecuaciones adicionales. De esta manera, la lógica que puede asociarse naturalmente a las IBAs es una extensión modal propia de S5. Presentamos un cálculo de Hilbert correcto y completo para esta extensión de S5 en el lenguaje de las IBAs, esto es, sin modalidades. / The aim of this thesis is the study of two main topics. In the first place we focus on the study of a particular class of Gentzen systems, the so called hypersequents; and in the second place, we address the study of certain logics which are given raised by tetravalent modal algebras. Both topics will be relate as we will see in Chapter III. Hypersequents are a natural generalization od ordinary sequents and turned out to be a very suitable tool for presenting Gentzen style formulations of diverse logics with the very desirable cut-elimination property. In recent years, methods for combining logics have gained a lot of attention, and motivations come from different areas such as Philosophy and Computer Science (see for instance [13] y [15]). Categorical fibring (also known as algebraic fibring) introduced in [55], has shown to be a very wide and powerful tool for combining logics. On the other hand, the class TMA of tetravalent modal algebras was first considered by Antonio Monteiro, and were studied mainly by I. Loureiro, A.V. Figallo, A. Ziliani and P. Landini. Later, J.M. Font and M. Rius en [31] were interested in the logics that can be defined taking into account the lattice–theoretical aspects of these algebras. These same authors introduced a sequent calculus for one of these logics, namely, T ML. In Chapter II, we present an alternative way to formulate hypersequent calculi introducing meta–variables for formulas, sequents and hypersequents, respectively, in the language. A suitable category of hypersequent calculi and both kind of fibring: constrained and unconstrained. The introduced morphisms turned out to bea novel notion of translation between logics which preserve meta–properties in a strong sense. Finally, we explore some preservation features,in particular we show a preservation result by fibring of the Craig interpolation property (CIP). In Chapter III, we retake the study of different logical aspects of TMAs. Considering the contrapositive implication introduced by A. Figallo and P. Landini in [28], we introduce three different Hilbert calculus for the logic T ML, as well as, a tableau system sound and complete with respect to the semantics of TMAs. The paraconsistent aspects of T ML also are analyzed under the point of view of Logics of Formal Inconsistency, introduced by W. Carnielli and J. Marcos in [18], and later studied in [17]. Normal modal tetravalent logic T MLN is also studied. Finally, we prove that both logics are proper sublogics of classical propositional calculus that are not maximal. In Chapter IV, we show that the sequent calculus presented by Font and Rius en [31] for T ML does not admit the cut–elimination property. So, we formulate a hypersequent calculus sound and complete with respect to T ML which does admit the so longed property. Finally, in Chapter V, motivated by the question of enrich T ML with a deductive implication, we prove that Monteiro’s tetravalent modal algebras enriched with a boolean complement coincide with De Morgan enriched with a boolean complement, or equivaxiv lently, they coincide with Boolean algebras enriched with a De Morgan negation. The latter are called involutive Boolean algebras (or symetric Boolean algebras) (IBAs), introduced by Gr. Moisil and mainly studied by A. Monteiro. We prove that IBAs are an algebraic counterpart to yhe modal logic S5 that satisfies some additional equations. So, the logic that naturally can be associated to IBAs is a proper modal extension of S5. We present a Hilbert calculus sound and complete with respect to this extension of S5 in the language of IBAs, i.e., without modalities.

El trabajo incluido en la presente tesis se enmarca dentro del campo de la demostración automática de teoremas y consiste en la estudio, definición y desarrollo de un paradigma de resolución lineal, denominado Resolución SL*. La razón para utilizar la denominación de paradigma reside en el hecho de que en sí misma resolución SL* no es un procedimiento, sino que se puede entender como una forma de razonamiento con ciertos parámetros cuya instanciación da lugar a diferentes procedimientos que son adecuados para el tratamiento de distintos tipos de problemas. Por otro lado, se le ha dado el nombre de resolución SL* porque, como posteriormente se explicará, está muy cercano a Eliminación de Modelos y a resolución SL (de ahí la primera parte del nombre). El asterisco final quiere denotar su parametrización, de forma que los procedimientos instancias de resolución SL* serán denominados con una letra más en vez del asterisco, como posteriormente se verá. La tesis ha sido dividida en cuatro capítulos que se describen brevemente a continuación. En el primero se realiza una breve introducción histórica a la demostración automática, que va desde los orígenes de la lógica con el uso de las primeras notaciones matemáticas formales en el siglo XVI hasta la aparición de los resultados más importantes de la lógica descubiertos por Herbrand, Gödel, Church, etc. Se hace un especial hincapié en este capítulo en la demostración automática realizando un recorrido desde sus orígenes a finales del siglo XVIII hasta el momento actual, en el cual es posible ver cuál ha sido la evolución de este campo y qué descubrimientos y resultados se pueden presentar como los principales puntos de inflexión. En el segundo capítulo se presentan la resolución lineal y algunos de sus principales refinamientos, ya que resolución SL* es un variación de resolución SL y por tanto de resolución lineal. Para ello se introduce el principio de resolución, viendo los problemas de su mecanización, y posteriormente se ven dos refinamientos de resolución: resolución semántica y resolución lineal. Para concluir se estudian los principales refinamientos de resolución lineal: resolución de entrada, resolución lineal con fusión, resolución lineal con subsumción, resolución lineal ordenada, resolución MTOSS y TOSS, Eliminación de Modelos, resolución SL y el sistema MESON. En el tercer capítulo se presentan y estudian con profundidad las principales aportaciones al campo de la demostración automática que se han producido en los últimos años y que están cercanas a la aproximación del presente trabajo. Se han incluido los siguientes trabajos: el demostrador PTTP de Stickel, el sistema MESON basado en secuencias de Plaisted, el demostrador SATCHMO de Manthey y Bry, los procedimientos Near-Horn Prolog de Loveland y otros autores y, por último, el demostrador SETHEO de Bibel y otros autores. Obviamente no se han incluido todos los demostradores y procedimientos, pero sí aquellos que se han considerado como los más interesantes y cercanos a resolución SL* de manera que sea posible realizar comparaciones, de forma que queden patentes las aportaciones realizadas. En el cuarto capítulo se presenta resolución SL*. Se da la definición formal de la misma y se introduce el concepto fundamental de elección de ancestros. La elección de ancestros es el mecanismo que permite controlar la aplicación de la resolución de ancestro haciendo posible una reducción del coste de su aplicación y una adecuación de resolución SL* al tipo de problema a tratar. Posteriormente se ven las principales instancias de resolución SL*, los procedimientos SLT y SLP. En este capítulo se hace un especial hincapié en la elección de ancestros, ya que es la principal aportación de resolución SL*, analizando tanto las ventajas que aporta asociadas al incremento de la eficiencia como el hecho de dotar a resolución SL* la capacidad de adaptarse a los problemas que trata. También en este capítulo se presenta una implementación de resolución SL*, en particular del procedimiento SLT, y se incluyen resultados sobre un conjunto extenso de problemas del campo de la demostración automática. En la última sección de este capítulo se realiza una comparación de resolución SL* con los demostradores y sistemas más cercanos, tanto a nivel de características como de resultados. / Casamayor Rodenas, JC. (1996). Resolución SL*: Un paradigma basado en resolución lineal para la demostración automática [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/6023