Reseña: Representations of finite groups

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra titulado Representations of finite groups.

Su autor es Jeremy Sylvestre (de la Univ. de Alberta en Canadá).

Su resumen es

We provide a formal framework for the theory of representations of finite groups, as modules over the group ring. Along the way, we develop the general theory of groups (relying on the group_add class for the basics), modules, and vector spaces, to the extent required for theory of group representations. We then provide formal proofs of several important introductory theorems in the subject, including Maschke’s theorem, Schur’s lemma, and Frobenius reciprocity. We also prove that every irreducible representation is isomorphic to a submodule of the group ring, leading to the fact that for a finite group there are only finitely many isomorphism classes of irreducible representations. In all of this, no restriction is made on the characteristic of the ring or field of scalars until the definition of a group representation, and then the only restriction made is that the characteristic must not divide the order of the group.

El trabajo se ha publicado el 12 de agosto en AFP (The Archive of Formal Proofs).

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.

Reseña: A symbolic approach to abstract algebra in HOL Light

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL Light sobre álgebra titulado A symbolic approach to abstract algebra in HOL Light.

Su autor es Marco Maggesi (de la Univ. de Florencia en Italia).

Su resumen es

Formalising algebraic structures (groups, rings, fields, vector spaces, lattices, …) is known to be challenging task which is often undertaken by exploiting various kind of extra-logical mechanisms (axiomatic classes, modules, locales, coercions, …) provided by most modern theorem provers.

We want to explore an alternative strategy, where algebraic structures are implemented via a deep embedding of mathematical formulas and are managed as first class objects in the HOL theory. Along the way, we provide a mechanism of generalised conversions, which extends Paulson’s conversions by allowing to compute with equivalence relations. We developed generalised conversions to support rewriting in our system, but they can be used independently and may have an interest in its own.

El trabajo se ha presentado en CICM 2015 (the 8th Conference on Intelligent Computer Mathematics).

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

Reseña: Using automated theorem provers to teach knowledge representation in first-order logic

PorJosé A. Alonso

Se ha publicado un artículo de aplicación del razonamiento automático a la enseñanza, usando Prover9, titulado Using automated theorem provers to teach knowledge representation in first-order logic.

Sus autores son Angelo Kyrilov y David Noelle (de la University of California, Merced).

Su resumen es

Undergraduate students of artificial intelligence often struggle with representing knowledge as logical sentences. This is a skill that seems to require extensive practice to obtain, suggesting a teaching strategy that involves the assignment of numerous exercises involving the formulation of some bit of knowledge, communicated using a natural language such as English, as a sentence in some logic. The number of such exercises needed to master this skill is far too large to allow typical artificial intelligence course teaching teams to provide prompt feedback on student efforts. Thus, an automated assessment system for such exercises is needed to ensure that students receive an adequate amount of practice, with the rapid delivery of feedback allowing students to identify errors in their understanding and correct them. This paper describes an automated grading system for knowledge representation exercises using first-order logic. A resolution theorem prover, Prover9, is used to check if a student-submitted formula is logically equivalent to a solution provided by the instructor. This system has been used by students enrolled in undergraduate artificial intelligence classes for several years. Use of this teaching tool resulted in a statistically significant improvement on first-order logic knowledge representation questions appearing on the course final examination. This article explains how this system works, provides an analysis of changes in student learning outcomes, and explores potential enhancements of this system, including the possibility of providing rich formative feedback by replacing the resolution theorem prover with a tableaux-based method.

El trabajo se ha presentado en el TTL2015 (Fourth International Conference on Tools for Teaching Logic)

El sistema y la metodología presentada en el artículo es análoga a la expuesta en el trabajo KRRT: Knowledge Representation and Reasoning Tutor System.

Reseña: Formal verification of programs computing the floating-point average

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre la aritmética titulado Formal verification of programs computing the floating-point average.

Sus autora es Silvie Boldo (del grupo Toccata (Formally Verified Programs, Certified Tools and Numerical Computations) en el LRI (Laboratoire de Recherche en Informatique) de la Universidad Paris-Sur).

Su resumen es

The most well-known feature of floating-point arithmetic is the limited precision, which creates round-off errors and inaccuracies. Another important issue is the limited range, which creates underflow and overflow, even if this topic is dismissed most of the time. This article shows a very simple example: the average of two floating-point numbers. As we want to take exceptional behaviors into account, we cannot use the naive formula (x+y)/2. Based on hints given by Sterbenz, we first write an accurate program and formally prove its properties. An interesting fact is that Sterbenz did not give this program, but only specified it. We prove this specification and include a new property: a precise certified error bound. We also present and formally prove a new algorithm that computes the correct rounding of the average of two floating-point numbers. It is more accurate than the previous one and is correct whatever the inputs.

El trabajo se presentará en el ICFEM 2015 (The 17th International Conference on Formal Engineering Methods).

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

Reseña: A synthetic proof of Pappus’ theorem in Tarski’s geometry

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre geometría titulado A synthetic proof of Pappus’ theorem in Tarski’s geometry

Sus autores son Gabriel Braun y Julien Narboux (del Équipe Informatique Géométrique et Graphique en la Universidad de Estrasburgo, Francia).

Su resumen es

In this paper, we report on the formalization of a synthetic proof of Pappus’ theorem. We provide two versions of the theorem: the first one is proved in neutral geometry (without assuming the parallel postulate), the second (usual) version is proved in Euclidean geometry. The proof that we formalize is the one presented by Hilbert in The Foundations of Geometry which has been detailed by Schwabhäuser, Szmielew and Tarski in part I of Metamathematische Methoden in der Geometrie. We highlight the steps which are still missing in this later version. The proofs are checked formally using the Coq proof assistant. Our proofs are based on Tarski’s axiom system for geometry without any continuity axiom. This theorem is an important milestone toward obtaining the arithmetization of geometry which will allow us to provide a connection between analytic and synthetic geometry.

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