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

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

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.