En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos estudiado el tipo abstracto de los grafos y su implementación en Haskell mediante vectores de adyacencia.
Las transparencias usadas en la clase son las páginas 1-18 del tema 22:
Read More “I1M2012: El TAD de los grafos y su implementación en Haskell mediante vectores de adyacencia”
Se ha publicado un artículo de verificación formal con ACL2 sobre sistemas SAT titulado Verifying refutations with extended resolution.
Sus autores son Marijn J. H. Heule, Warren A. Hunt, Jr. y Nathan Wetzler (de la Universidad de Tejas en Austin).
El trabajo se presentó la semana pasada en el CADE-24 (the 24th International Conference on Automated Deduction).
Su resumen es
Modern SAT solvers use preprocessing and inprocessing techniques that are not solely based on resolution; existing unsatisfiability proof formats do not support SAT solvers using such techniques. We present a new proof format for checking unsatisfiability proofs produced by SAT solvers that use techniques such as extended resolution and blocked clause addition. Our new format was designed with three goals: proofs should be easy to generate, proofs should be compact, and validating proofs must be simple. We show how existing preprocessors and solvers can be modified to generate proofs in our new format. Additionally, we implemented a mechanically-verified proof checker in ACL2 and a proof checker in C for the proposed format.
El correspondiente código ACL2 se encuentra aquí.
Se ha publicado un trabajo de automatización del razonamiento en Isabelle titulado A Web interface for Isabelle: The next generation.
Sus autores son Christoph Lüth y Martin Ring (de la Universidad de Bremen, Alemania).
El trabajo se presentará en julio en el CICM 2013 (Conferences on Intelligent Computer Mathematics).
Su resumen es
We present Clide, a web interface for the interactive theorem prover Isabelle. Clide uses latest web technology and the Isabelle/PIDE framework to implement a web-based interface for asynchronous proof document management that competes with, and in some aspects even surpasses, conventional user interfaces for Isabelle such as Proof General or Isabelle/jEdit.
Se ha publicado un trabajo de razonamiento formalizado en HOL4 titulado On the formalization of continuous-time Markov chains in HOL.
Sus autores son Liya Liu, Osman Hasan y Sofiène Tahar (de la Concordia University, Montreal, Canadá).
Su resumen es
Continuous-time Markov chain has been extensively applied to model diverse real-world systems. The analysis of these systems has been conducted using conventional simulation technique and computer algebra systems, more recently, probabilistic model checking. However, these methods either cannot guarantee accurate analysis or are not scalable due to the unacceptable computation consumption. As a complemental technique, theorem proving is proposed to reason about continuous-time Markov chain using HOL theorem proving. To our best knowledge, the formalization of continuous-time Markov chain has not been found in any theorem prover. In this report, we provide the idea on the formal definition of continuous-time Markov chain and two of its formally verified properties as the first step to formalize the continuous-time Markov chain theory. Also, we present the next step and the predict the potential challenges in the formalization process. Finally, a certain of applications are listed to be targeted using the formalized continuous-time Markov chain.
En la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de los ejercicios de verificación en Isabelle de propiedades de funciones sobre listas de las siguientes relaciones: