HOL Light

Se ha publicado un artículo de razonamiento formalizado en HOL Light sobre geometría titulado Compass-free navigation of mazes

Sus autores son Phil Scott y Jacques Fleuriot (de la Universidad de Edimburgo).

Su resumen es

If you find yourself in a corridor of a standard maze, a sure and easy way to escape is to simply pick the left (or right) wall, and then follow it along its twists and turns and around the dead-ends till you eventually arrive at the exit. But what happens when you cannot tell left from right? What if you cannot tell North from South? What if you cannot judge distances, and have no idea what it means to follow a wall in a given direction? The possibility of escape in these circumstances is suggested in the statement of an unproven theorem given in David Hilbert’s celebrated Foundations of Geometry, in which he effectively claimed that a standard maze could be fully navigated using axioms and concepts based solely on the relations of points lying on lines in a specified order. We discuss our algorithm for this surprisingly challenging version of the maze navigation problem, and our HOL Light verification of its correctness from Hilbert’s axioms.

El trabajo se ha presentado en el SCSS 2016 (7th International Symposium on Symbolic Computation in Software Science).

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

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

Se ha publicado un artículo de razonamiento formalizado en HOL Light sobre topología titulado A formalisation of metric spaces in HOL Light.

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

Su resumen es

We present a computer formalisation of metric spaces in the HOL Light theorem prover. Basic results of the theory of complete metric spaces are proved. A simple decision procedure for the theory of metric space is implemented.

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

Se ha publicado un artículo de razonamiento formalizado en HOL Light sobre cinemática titulado Formal kinematic analysis of the two-link planar manipulator.

Sus autores son Binyameen Farooq, Osman Hasan, Sohail Iqbal (de la Universidad de Islamabad, Pakistán).

Su resumen es

Kinematic analysis is used for trajectory planning of robotic manipulators and is an integral step of their design. The main idea behind kinematic analysis is to study the motion of the robot based on the geometrical relationship of the robotic links and their joints. Given the continuous nature of kinematic analysis, traditional computer-based verification methods, such as simulation, numerical methods or model checking, fail to provide reliable results. This fact makes robotic designs error prone, which may lead to disastrous consequences given the safety-critical nature of robotic applications. Leveraging upon the high expressiveness of higher-order logic, we propose to use higher-order-logic theorem proving for conducting formal kinematic analysis. As a first step towards this direction, we utilize the geometry theory of HOL-Light to develop formal reasoning support for the kinematic analysis of a two-link planar manipulator, which forms the basis for many mechanical structures in robotics. To illustrate the usefulness of our foundational formalization, we present the formal kinematic analysis of a biped walking robot.

El trabajo se ha presentado en el ICFEM 2013 (15th International Conference on Formal Engineering Methods). Las trasparencias de la presentación se encuentran aquí.

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