Isabelle/HOL

Se ha publicado un artículo de razonamiento formalizado en Coq titulado “Concrete semantics” with Coq and CoqHammer.

Sus autores son

• Łukasz Czajka (de la Universidad de Copenhagen),
• Burak Ekici (de la Universidad de Innsbruck) y
• Cezary Kaliszyk (de la Universidad de Innsbruck).

Su resumen es

The “Concrete Semantics” book gives an introduction to imperative programming languages accompanied by an Isabelle/HOL formalization. In this paper we discuss a re-formalization of the book using the Coq proof assistant. In order to achieve a similar brevity of the formal text we extensively use CoqHammer, as well as Coq Ltac-level automation. We compare the formalization efficiency, compactness, and the readability of the proof scripts originating from a Coq re-formalization of two chapters from the book.

El trabajo se ha presentado el 15 de agosto en el CICM 2018 (11th Conference on Intelligent Computer Mathematics).

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

Se ha publicado un artículo de demostración asistida por ordenador titulado Comparison of two theorem provers: Isabelle/HOL and Coq.

Sus autores son

• Artem Yushkovskiy de ITMO University (St. Petersburg, Russia)
• Stavros Tripakis de Aalto University (Espoo, Finland)

Su resumen es

The need for formal definition of the very basis of mathematics arose in the last century. The scale and complexity of mathematics, along with discovered paradoxes, revealed the danger of accumulating errors across theories. Although, according to Gödel’s incompleteness theorems, it is not possible to construct a single formal system which will describe all phenomena in the world, being complete and consistent at the same time, it gave rise to rather practical areas of logic, such as the theory of automated theorem proving. This is a set of techniques used to verify mathematical statements mechanically using logical reasoning. Moreover, it can be used to solve complex engineering problems as well, for instance, to prove the security properties of a software system or an algorithm. This paper compares two widespread tools for automated theorem proving, Isabelle/HOL and Coq, with respect to expressiveness, limitations and usability. For this reason, it firstly gives a brief introduction to the bases of formal systems and automated deduction theory, their main problems and challenges, and then provides detailed comparison of most notable features of the selected theorem provers with support of illustrative proof examples.