Reseña: A hierarchy of mathematical structures in ACL2

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

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

Reseña: Formalized algebraic numbers: construction and first-order theory

Se ha publicado una tesis de razonamiento formalizado en Coq sobre los números algebraicos titulada Formalized algebraic numbers: construction and first-order theory.

Su autor es Cyril Cohen dirigido por Assia Mahboubi y Benjamin Werner (de la Escuela Politécnica de París)

Su resumen es

This thesis presents a formalization of algebraic numbers and their theory. It brings two new important contributions to the formalization of mathematical results in proof assistants, Coq in our case: the intuitionistic construction of real algebraic numbers together with the proof they form a real closed field, and the programming and certification of quantifier elimination procedures for the theories of algebraically closed fields and real closed fields. In order to reach those results, we brought multiple contributions to the toolboxes and formalization and proof methodologies in Coq. More particularly, we provide in Coq/SSReflect a framework to work with quotient types. We provide a complete library about ordered and normed number algebraic structures. We wrote a short implementation of Cauchy reals together with tactics to deal easily with reasoning using assertions of the form “let n be a big enough number”, commonly used in mathematical paper proofs. We also developed a short library of real polynomial analysis. A big part of our contributions is useful for the formalization of the proof of Odd Order Theorem and they also aim at helping to prove and certify more efficient quantifier elimination procedures on reals.

La correspondientes teorías en Coq se encuentran en aquí.

Reseña: Verifying a plaftorm for digital imaging: a multi-tool strategy

Se ha publicado un trabajo de verificación formal con Why/Krakatoa, Coq y ACL2 titulado Verifying a platform for digital imaging: a multi-tool strategy.

Sus autores son Jónathan Heras, Gadea Mata, Ana Romero, Julio Rubio y Rubén Sáenz (de la Universidad de la Rioja).

Su resumen es

Fiji is a Java platform widely used by biologists and other experimental scientists to process digital images. In particular, in our research – made together with a biologists team; we use Fiji in some pre-processing steps before undertaking a homological digital processing of images. In a previous work, we have formalised the correctness of the programs which use homological techniques to analyse digital images. However, the verification of Fiji’s pre-processing step was missed. In this paper, we present a multi-tool approach filling this gap, based on the combination of Why/Krakatoa, Coq and ACL2.

Los códigos correpondientes al trabajo se encuentran aquí.

Reseña: Formal reasoning about finite-state discrete-time Markov chains in HOL

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre procesos de Markov titulado Formal reasoning about finite-state discrete-time Markov chains in HOL.

Sus autores son Liya Liu, Osman Hasan y Sofiène Tahar (de la Univ. de Concordia, Canadá).

Su resumen es

Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyzing Markovian models, for example, Markov Chain Monte Carlo based simulation, Markov Analyzer, and more recently probabilistic model-checking. However, these techniques either do not guarantee accurate analysis or are not scalable. Higher-order-logic theorem proving is a formal method that has the ability to overcome the above mentioned limitations. However, it is not mature enough to handle all sorts of Markovian models. In this paper, we propose a formalization of Discrete-Time Markov Chain (DTMC) that facilitates formal reasoning about time-homogeneous finite-state discrete-time Markov chain. In particular, we provide a formal verification on some of its important properties, such as joint probabilities, Chapman-Kolmogorov equation, reversibility property, using higher-order logic. To demonstrate the usefulness of our work, we analyze two applications: a simplified binary communication channel and the Automatic Mail Quality Measurement protocol.

La revista en donde que ha publicado el artículo es el Journal of Computer Science and Technology.