LMF2013: Tableros semánticos

PorJosé A. Alonso

En la clase de hoy del curso Lógica matemática y fundamentos se ha presentado un nuevo sistema deductivo: los tableros semánticos.

Hemos visto cómo los problemas de tautología y de consecuencia lógica se reducen a problemas de consistencia:

  • F es una tautología syss \{\neg F\} es inconsistente.
  • F es consecuencia lógica de S syss S \cup \{\neg F\} es inconsistente.

Por tanto, para resolver ambos problemas basta con tener un procedimiento sistemático de búsqueda de modelos. Uno de dichos procedimientos es el de tableros semánticos.

Una ventaja de los tableros semánticos frente a la deducción natural es la reducción del número lo que facilita su automatización.

Además, se ha presentado el sistema Tree Proof Generator que busca automáticamente el tablero semántico correspondiente a la fórmula introducida.

Las transparencias de esta clase son las del tema 3 (tableros proposicionales) y las del tema 9 (tableros de primer orden)
Read More “LMF2013: Tableros semánticos”

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