LI2013-14: La lógica de Prolog

En la clase de hoy del curso Lógica Informática se ha realizado una introducción a la programación lógica con Prolog como aplicación de la resolución en la lógica de primer orden.

Se ha presentado el sistema deductivo de Prolog en tres fases: proposicional, relacional y funcional. En cada una se ha comentado cómo representar el conocimiento, cómo realizar consultas y cómo es el razonamiento de Prolog para calcular las respuestas.

En los siguiente vídeos se presenta el uso de Prolog y uso de SldRaw.

La clase se basa en los apuntes de Introducción a la programación lógica con Prolog.

Las transparencias de esta clase son las página 1 a 18 del tema 12
Read More “LI2013-14: La lógica de Prolog”

Reseña: “Proofs you can believe in – Proving equivalences between Prolog semantics in Coq”

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Proofs you can believe in (Proving equivalences between Prolog semantics in Coq).

Sus autores son

El trabajo se presentará en septiembre en el PPDP 2013 (15th International Symposium on Principles and Practice of Declarative Programming ).

Su resumen es

Basing program analyses on formal semantics has a long and successful tradition in the logic programming paradigm. These analyses rely on results about the relative correctness of mathematically sophisticated semantics, and authors of such analyses often invest considerable effort into establishing these results. The development of interactive theorem provers such as Coq and their recent successes both in the field of program verification as well as in mathematics, poses the question whether these tools can be usefully deployed in logic programming. This paper presents formalisations in Coq of several general results about the correctness of semantics in different styles; forward and backward, top-down and bottom-up. The results chosen are paradigmatic of the kind of correctness theorems that semantic analyses rely on and are therefore well-suited to explore the possibilities afforded by the application of interactive theorem provers to this task, as well as the difficulties likely to be encountered in the endeavour. It turns out that the advantages offered by moving to a functional setting, including the possibility to apply higher-order abstract syntax, are considerable.

El código de las correspondientes teorías en Coq se encuentra aquí.

LMF2013: Soluciones lógicas de problemas lógicos

En la clase de hoy del curso Lógica matemática y fundamentos se ha presentado una colección de problemas para mostrar cómo pueden resolverse elementalmente con Prolog.

Los problemas son

  1. Rompecabeza lógico.
  2. La banda de músicos.
  3. Mini sudoku.
  4. Criptoaritmética.
  5. Cuadrados mágicos.
  6. La sucesión de Langford.
  7. Coloraciones de un mapa.
  8. El mono y el plátano.

A continuación se muestran los problemas y sus soluciones
Read More “LMF2013: Soluciones lógicas de problemas lógicos”

LMF2013: Introducción a la programación lógica con Prolog

En la clase de hoy del curso Lógica matemática y fundamentos se ha realizado una introducción a la programación lógica con Prolog como aplicación de la resolución en la lógica de primer orden.

Se ha presentado el sistema deductivo de Prolog en tres fases: proposicional, relacional y funcional. En cada una se ha comentado cómo representar el conocimiento, cómo realizar consultas y cómo es el razonamiento de Prolog para calcular las respuestas.

Los apuntes de esta clase son Introducción a la programación lógica con Prolog (páginas 1-26).

Las transparencias de esta clase son las páginas 1 a 18 del tema 13
Read More “LMF2013: Introducción a la programación lógica con Prolog”

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

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