Reseña: A formal proof of Kruskal’s tree theorem in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado A formal proof of Kruskal’s tree theorem in Isabelle/HOL.

Su autor es Christian Sternagel (del JAIST, Japón).

Su resumen es

We give the first formalization of Kruskal’s tree theorem in a proof assistant – the closure of a long-standing challenge. More concretely, we present our Isabelle/HOL development of Nash-Williams’ minimal bad sequence argument for proving the tree theorem. Along the way, we discuss proofs of Dickson’s lemma and Higman’s lemma; and close all gaps in the original proofs.

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

Reseña: Formalizing Knuth-Bendix orders and Knuth-Bendix completion

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre sistemas de reescritura titulado Formalizing Knuth-Bendix orders and Knuth-Bendix completion.

Sus autores son Christian Sternagel (del Instituto japonés de ciencias y tecnología) y René Thiemann (de la Univ. de Innsbruck, Austria).

El trabajo se presentará en junio en la RTA 2013 (24th International Conference
on Rewriting Techniques and Applications).

Su resumen es

We present extensions of our Isabelle Formalization of Rewriting that cover two historically related concepts: the Knuth-Bendix order and the Knuth-Bendix completion procedure. The former, besides being the first development of its kind in a proof assistant, is based on a generalized version of the Knuth-Bendix order. We compare our version to variants from the literature and show all properties required to certify termination proofs of TRSs. The latter comprises the formalization of important facts that are related to completion, like Birkhoff’s theorem, the critical pair theorem, and a soundness proof of completion, showing that the strict encompassment condition is superfluous for finite runs. As a result, we are able to certify completion proofs.

El código con las correspondientes teorías Isabelle se encuentra en la versión 2.10 de IsaFoR/CeTA.

Reseña: Developing an auction theory toolbox

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Developing an auction theory toolbox.

Sus autores son Christoph Lange, Colin Rowat, Wolfgang Windsteiger y Manfred Kerber.

Su resumen es

Auctions allocate trillions of dollars in goods and services every year. Auction design can have significant consequences, but its practice outstrips theory. We seek to advance auction theory with help from mechanised reasoning. To that end we are developing a toolbox of formalised representations of key facts of auction theory, which will allow auction designers to have relevant properties of their auctions machine-checked. As a first step, we are investigating the suitability of different mechanised reasoning systems (Isabelle, Theorema, and TPTP) for reproducing a key result of auction theory: Vickrey’s celebrated 1961 theorem on the properties of second price auctions – the foundational result in modern auction theory. Based on our formalisation experience, we give tentative recommendations on what system to use for what purpose in auction theory, and outline further steps towards a complete auction theory toolbox.

El trabajo se presentó en la AISB Convention 2013.

Los códigos de las correspondientes teorías se encuentran Auction Theory Toolbox (ATT). Contiene los códigos de las formalizaciones en CASL, Isabelle, Mizar y Theorema.

Reseña: Formalization of incremental simplex algorithm by stepwise refinement

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Formalization of incremental simplex algorithm by stepwise refinement.

Sus autores son Mirko Spasić and Filip Marić (de la Universidad de Belgrado).

Su resumen es

We present an Isabelle/HOL formalization and total correctness proof for the incremental version of the Simplex algorithm which is used in most state-of-the-art SMT solvers. Formalization relies on stepwise program and data refinement, starting from a simple specification, going through a number of fine refinement steps, and ending up in a fully executable functional implementation. Symmetries present in the algorithm are handled with special care.

El trabajo se presentó en el FM2012 (18th International Symposium on Formal Methods) y las transparencias de la presentación se encuentran aquí.

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

Reseña: Coinductive pearl: Modular first-order logic completeness

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre metalógica titulado Coinductive pearl: Modular first-order logic completeness.

Sus autores son Jasmin Christian Blanchette, Andrei Popescu y Dmitriy Traytel (de la Universidad Técnica de Munich).

Su resumen es

Codatatypes are unfortunately still missing in many programming languages and proof assistants. We make a case for their usefulness by revisiting a classic result: the completeness theorem for first-order logic established through a Gentzen system. Codatatypes help capture the essence of the proof, which establishes an abstract property of derivation trees independently of the concrete syntax or inference rules. This separation of concerns simplifies the presentation, especially for readers acquainted with lazy data structures. The proof is formalized in Isabelle/HOL and demonstrates the recently introduced definitional package for codatatypes and its integration with Isabelle’s Haskell code generator.

El código de las teorías Isabelle correspodientes se encuentra aquí.