Reseña: A hierarchy of mathematical structures in ACL2

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en ACL2 titulado A hierarchy of mathematical structures in ACL2.

Sus autores son Jónathan Heras, Francisco J. Martín y Vico Pascual.

Su resumen es

In this paper, we present a methodology which allows one to deal with mathematical structures in the ACL2 theorem prover. Namely, we cope with the representation of mathematical structures, the certification that an object fulfills the axioms characterizing an algebraic structure and the generation of generic theories about concrete structures. As a by-product, an ACL2 algebraic hierarchy has been obtained. Our framework has been tested with the definition of homology groups, an example coming from Homological Algebra which involves several notions related to Universal Algebra. The method presented here, when compared to a from-scratch approach, is preferred when working with complex mathematical structures; for instance, the ones coming from Algebraic Topology. The final aim of this work is the verification of Computer Algebra systems, a field where our hierarchy fits better than the ones developed in other systems.

El códico correspondiente a este trabajo se encuentra aquí.

LMF2013: Sintaxis y semántica de la lógica de primer orden

PorJosé A. Alonso

En la clase de hoy del curso Lógica matemática y fundamentos se presentado la sintaxis y la semántica de la lógica de primer orden como respuestas a las siguientes preguntas:

  • ¿cómo se puede representar el conocimiento con la lógica de primer orden?,
  • ¿qué es una fórmula de primer orden?,
  • ¿qué significa que una fórmula verdadera? y
  • ¿qué significa que un argumento sea correcto?

Como ejemplos de representación hemos visto cómo representar conocimiento geográfico, del mundo de los bloques y conocimiento astronómico. En los distintos ejemplos hemos resaltado los tipos de símbolos lógicos utilizados.

A partir de los ejemplos de representación del conocimiento, se han definido los símbolos lógicos (variables, conectivas, cuantificadores e igualdad) y los símbolos no lógicos (constantes, predicados y funciones) que forman el alfabeto del lenguaje de la lógica de primer orden.

A partir del alfabeto, se definen los términos, las fórmulas atómicas y las fórmulas del lenguaje.

Como medio del reconocimiento de fórmulas, se introducen los árboles de análisis. Con ello, respondemos a la segunda de las preguntas iniciales.

En el estudio sintáctico, definimos el conjunto de las subfórmulas, el conjunto de las variables de un término, las ocurrencias libres y ligadas, el conjunto de las variables libres y ligadas y las fórmulas cerradas y abiertas. Algunas de las definiciones anteriores se realizan por recursión sobre fórmulas o sobre términos.

En segundo lugar hemos estudiado la semántica, comenzando con distintas cuestiones sobre qué significa que una fórmula sea verdadera para resaltar su dependencia del universo, la interpretación de los símbolos no lógico y de las asignaciones a las variables libres.

Se han definido las estructuras de un lenguaje, las asignaciones a las variables y las interpretaciones de un lenguaje.

Se ha definido el valor de un término o de una fórmula en una interpretación. Con ello, respondemos a la tercera de las preguntas iniciales.

Finalmente, se han definido los conceptos de consistencia, consecuencia lógica y equivalencia y se ha explicado la metodología de búsqueda semántica de modelos y contramodelos.

Las transparencias de esta clase son las del tema 7.

I1M2012: Resolución de problemas matemáticos con Haskell

PorJosé A. Alonso

En las clases de ayer y de hoy de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los ejercicios de la 12ª relación en la que se plantea la resolución de distintos problemas
matemáticos. En concreto,

  • el problema de Ullman sobre la existencia de subconjunto del tamaño dado y con su suma acotada,
  • las descomposiciones de un número como suma de dos cuadrados,
  • el problema 145 del proyecto Euler,
  • el grafo de una función sobre los elementos que cumplen una propiedad,
  • los números semiperfectos,
  • el carácter funcional de una relación y
  • la identidad de Bezout.

Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2012: Resolución de problemas matemáticos con Haskell”

Reseña: Knowledge representation, reasoning, and the design of intelligent agents

PorJosé A. Alonso

Se ha publicado un libro sobre representación del conocimiento y razonamiento titulado Knowledge representation, reasoning, and the design of intelligent agents.

Sus autores son Michael Gelfond y Yulia Kahl.

Su resumen es

This is a book about knowledge representation and reasoning (KRR) – a comparatively new branch of science which serves as the foundation of Artificial Intelligence, Declarative Programming, and the design of knowledge – intensive software systems. Our main goal is to show how a a software system can be given knowledge about the world and itself, and how this knowledge can be used to solve non-trivial computational problems. There are several approaches to KRR which both compete and complement each other. The approaches differ primarily by the languages used to represent the knowledge and by corresponding computational methods. This book is based on a knowledge representation language called Answer Set Prolog (ASP) and the answer set programming paradigm – a comparatively recent branch of KRR with a well-developed theory, efficient reasoning systems, methodology of use, and a growing number of applications.

The text can be used for classes in Knowledge Representation, Declarative Programming, and Artificial Intelligence for advanced undergraduate or graduate students in computer science and related disciplines including software engineering, logic, cognitive science, etc. It will also be useful to serious researchers in these fields who would like to learn more about the answer sets programming paradigm and its use in KRR. Finally, we hope it will be of interest to anyone with a sense of wonder about the amazing ability of humans to derive volumes of knowledge from a collection of basic facts. Knowledge representation and reasoning, located at the intersection of mathematics, science and the humanities, provides us with mathematical and computational models of human thought and gives some clues to the understanding of this ability. The reader is not required to know logic or to have previous experience with computational systems. However, some understanding of mathematical method of thinking will be of substantial help.

We have attempted to maintain a proper balance between mathematical analysis of the subject and practical design of intelligent agents — software systems capable of using knowledge about their environment to perform intelligent tasks. Beginning with simple question-answering agents, we progress to more and more complex ones and explain how common problems of knowledge representation and reasoning such as commonsense (default) reasoning, planning, diagnostics and probabilistic reasoning are solved with ASP and its extensions. The precise mathematical definitions of basic concepts are always accompanied by informal discussions and by examples of their use for modeling various computational tasks performed by humans. Readers are encouraged to run programs to test their agent’s ability to perform these tasks using available, state-of-the-art ASP reasoning systems.

Of course the worth of a particular KRR theory is tested by the ability of software agents built on the basis of this theory to behave intelligently. If, given a certain amount of knowledge, the agent exhibits behavior that we believe reasonable for a human with exactly the same knowledge, we deem the theory to be a step in the right direction.

We hope that serious readers will learn to appreciate the interplay between mathematical modeling of a phenomenon and system design and better understand the view of programming as refinement of specifications. Even though the book does not contain large practical projects, we believe that the skills learned will be of substantial use in the marketplace.

We meant for this book to be a foundation for those interested in KRR. Our desire to limit the material to one semester forced us to skip many topics closely related to our approach. This includes various constraint and abductive logic programming languages and algorithms, descriptions of important ASP reasoning methods, the methodology of transforming ASP programs to improve their efficiency, and a large body of useful mathematical knowledge. The book does not cover other important KR topics such as descriptive logics and their use for the Semantic Web and other applications, natural language processing, etc. To help those interested in building on the foundation presented and learning more about these other topics, we have included a section on references and further reading in each chapter.”

LMF2013: Ejercicios de deducción natural en lógica proposicional con Isabelle/HOL

PorJosé A. Alonso

En las clases del miércoles y de hoy del curso Lógica matemática y fundamentos se han comentado soluciones de los ejercicios de deducción natural en lógica proposicional con Isabelle/HOL.

Para cada uno de los ejercicios se ha presentado distintas demostraciones: desde la detallada (que sea parecida a la mostrada en las transparencias) hasta la automática.

La teoría con la relación de ejercicios es
Read More “LMF2013: Ejercicios de deducción natural en lógica proposicional con Isabelle/HOL”