En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones de los ejercicios sobre conjuntos de la 19ª relación.
Los ejercicios y su solución se muestran a continuación
Read More “I1M2014: Ejercicios de operaciones con conjuntos en Haskell”
En la primera parte de la clase de hoy del curso de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los ejercicios de la relación 18. El objetivo de la relación es implementar la regla de Ruffini y sus aplicaciones utilizando las implementaciones del TAD de polinomio estudiadas en el tema 21.
En los ejercicios se usan las siguientes librerías:
Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2014: División y factorización de polinomios mediante la regla de Ruffini”
Se ha publicado un artículo de razonamiento formalizado en Coq titulado Program verification by coinduction.
Sus autores son Brandon Moore y Grigore Rosu (del Formal Systems Laboratory en la Universidad de Illinois en Urbana-Champaign).
Su resumen es
We present a program verification framework based on coinduction, which makes it feasible to verify programs directly against an operational semantics, without requiring intermediates like axiomatic semantics or verification condition generators. Specifications can be written and proved using any predicates on the state space of the operational semantics.
We implement our approach in Coq, giving a certifying language-independent verification framework. The core proof system is implemented as a single module imported unchanged into proofs of programs in any semantics. A comfortable level of automation is provided by instantiating a simple heuristic with tactics for language-specific tasks such as finding the successor of a symbolic state, and for domain-specific reasoning about the predicates used in a particular specification. This approach also smoothly allows manual assistance at points the automation cannot handle.
We demonstrate the power of our approach by verifying algorithms as complicated as Schorr-Waite graph marking, and the versatility by instantiating it for object languages in several styles of semantics. Despite the greater flexibility and generality of our approach, proof size and proof/certificate-checking time compare favorably with Bedrock, another Coq-based certifying program verification framework.
En la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado la deducción natural en la lógica proposicional.
También se ha presentado cómo escribir demostraciones por deducción natural en Pandora del que se mostró un videotutorial.
Las transparencias de estas clases son las del tema 2
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra lineal titulado QR decomposition.
Sus autores son Jose Divasón y Jesús Aransay (de la Universidad de la Rioja).
Su resumen es
QR decomposition is an algorithm to decompose a real matrix A into the product of two other matrices Q and R, where Q is orthogonal and R is invertible and upper triangular. The algorithm is useful for the least squares problem; i.e., the computation of the best approximation of an unsolvable system of linear equations. As a side-product, the Gram-Schmidt process has also been formalized. A refinement using immutable arrays is presented as well. The development relies, among others, on the AFP entry Implementing field extensions of the form Q{sqrt(b)}” by René Thiemann, which allows execution of the algorithm using symbolic computations. Verified code can be generated and executed using floats as well.
El trabajo se ha publicado la semana pasada en The Archive of Formal Proofs
El código de las correspondientes teorías en Isabelle se encuentra aquí.