Menu Close

Etiqueta: Reseña

Reseña: Decreasing diagrams for Church-Rosser modulo

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre reescritura titulado Decreasing diagrams for Church-Rosser modulo.

Su autor es Bertram Felgenhauer (del Computational Logic Research Group en la Universidad de Innsbruck, Austria).

Su resumen es

This theory formalizes a commutation version of decreasing diagrams for Church-Rosser modulo. The proof follows Felgenhauer and van Oostrom (RTA 2013). The theory also provides important specializations, in particular van Oostrom’s conversion version (TCS 2008) of decreasing diagrams.

We follow the development described in 1: Conversions are mapped to Greek strings, and we prove that whenever a local peak (or cliff) is replaced by a joining sequence from a locally decreasing diagram, then the corresponding Greek strings become smaller in a specially crafted well-founded order on Greek strings. Once there are no more local peaks or cliffs are left, the result is a valley that establishes the Church-Rosser modulo property.

As special cases we provide non-commutation versions and the conversion version of decreasing diagrams by van Oostrom 3. We also formalize extended decreasingness 2.

El trabajo se ha publicado en The Archive of Formal Proofs.

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

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.

Reseña: Matrices, Jordan normal forms, and spectral radius theory

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre
álgebra lineal titulado Matrices, Jordan normal forms, and spectral radius theory.

Sus autores son René Thiemann y Akihisa Yamada (del Computational Logic Group en la Universidad de Innsbruck, Austria)

Su resumen es

Matrix interpretations are useful as measure functions in termination proving. In order to use these interpretations also for complexity analysis, the growth rate of matrix powers has to examined. Here, we formalized a central result of spectral radius theory, namely that the growth rate is polynomially bounded if and only if the spectral radius of a matrix is at most one.

To formally prove this result we first studied the growth rates of matrices in Jordan normal form, and partially prove the result that every complex matrix has a Jordan normal form: we are restricted to upper-triangular matrices since we did not yet formalize the Schur decomposition.

The whole development is based on a new abstract type for matrices, which is also executable by a suitable setup of the code generator. It completely subsumes our former AFP-entry on executable matrices, and its main advantage is its close connection to the HMA-representation which allowed us to easily adapt existing proofs on determinants.

All the results have been applied to improve CeTA, our certifier to validate termination and complexity proof certificates.

El trabajo se ha publicado en The Archive of Formal Proofs .

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

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.

Reseña: Formalization of error-correcting codes (from Hamming to modern coding theory)

Se ha publicado un artículo de razonamiento formalizado en Coq sobre codificación titulado Formalization of error-correcting codes (from Hamming to modern coding theory)

Sus autores son

Su resumen es

By adding redundancy to transmitted data, error-correcting codes (ECCs) make it possible to communicate reliably over noisy channels. Minimizing redundancy and (de)coding time has driven much research, culminating with Low-Density Parity-Check (LDPC) codes. At first sight, ECCs may be considered as a trustful piece of computer systems because classical results are well-understood. But ECCs are also performance-critical so that new hardware calls for new implementations whose testing is always an issue. Moreover, research about ECCs is still flourishing with papers of ever-growing complexity. In order to provide means for implementers to perform verification and for researchers to firmly assess recent advances, we have been developing a formalization of ECCs using the SSReflect extension of the Coq proof-assistant. We report on the formalization of linear ECCs, duly illustrated with a theory about the celebrated Hamming codes and the verification of the sum-product algorithm for decoding LDPC codes.

El trabajo se presentó el 25 de agosto en el ITP 2015 (The 6th conference on Interactive Theorem Proving).

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

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.

Reseña: Verified over-approximation of the diameter of propositionally factored transition systems

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre verificación titulado Verified over-approximation of the diameter of propositionally factored transition systems.

Sus autores son
+ Mohammad Abdulaziz (del Software Systems Research Group del NICTA en Camberra, Australia),
+ Charles Gretton (de la Australian National University en Camberra, Australia) y
+ Michael Norrish (del Software Systems Research Group del NICTA en Camberra, Australia)

Su resumen es

To guarantee the completeness of bounded model checking (BMC) we require a completeness threshold. The diameter of the Kripke model of the transition system is a valid completeness threshold for BMC of safety properties. The recurrence diameter gives us an upper bound on the diameter for use in practice. Transition systems are usually described using (propositionally) factored representations. Bounds for such lifted representations are calculated in a compositional way, by first identifying and bounding atomic subsystems, and then composing those results according to subsystem dependencies to arrive at a bound for the concrete system. Compositional approaches are invalid when using the diameter to bound atomic subsystems, and valid when using the recurrence diameter. We provide a novel overapproximation of the diameter, called the sublist diameter, that is tighter than the recurrence diameter. We prove that compositional approaches are valid using it to bound atomic subsystems. Those proofs are mechanised in HOL4. We also describe a novel verified compositional bounding technique which provides tighter overall bounds compared to existing bottom-up approaches.

El trabajo se presentó el 26 de agosto en el ITP 2015 (The 6th conference on Interactive Theorem Proving).

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

Reseña: Stream fusion for Isabelle’s code generator

Se ha publicado un artículo de automatización del razonamiento formalizado en Isabelle/HOL Stream fusion for Isabelle’s code generator.

Sus autores son Andreas Lochbihler y Alexandra Maximova (del Information Security Group en la Escuela Politécnica Federal de Zúrich, Suiza).

Su resumen es

Stream fusion eliminates intermediate lists in functional code. We formalise stream fusion for finite and coinductive lists in Isabelle/HOL and implement the transformation in the code preprocessor. Our initial results show that optimisations during code extraction can boost the performance of the generated code, but the transformation requires further engineering to be usable in practice.

Su contenido es un resumen de la tesis de Máster Stream Fusion for Isabelle’s Code Generator realizada por Alexandra Maximova y dirigida por Andreas Lochbihler.

El trabajo se presentó el 25 de agosto en el ITP 2015 (The 6th conference on Interactive Theorem Proving).

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

Reseña: The Akra-Bazzi theorem and the Master theorem

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado The Akra-Bazzi theorem and the Master theorem.

Su autor es Manuel Eberl (del Theorem Proving Group en la Technische Universität München, Munich, Alemania).

Su resumen es

This article contains a formalisation of the Akra-Bazzi method based on a proof by Leighton. It is a generalisation of the well-known Master Theorem for analysing the complexity of Divide & Conquer algorithms. We also include a generalised version of the Master theorem based on the Akra-Bazzi theorem, which is easier to apply than the Akra-Bazzi theorem itself.

Some proof methods that facilitate applying the Master theorem are also included. For a more detailed explanation of the formalisation and the proof methods, see the accompanying paper (publication forthcoming).

El trabajo se ha publicado en AFP (The Archive of Formal Proofs).

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

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático y Lógica computacional y teoría de modelos.

Reseña: Landau symbols en Isabelle/HOL

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado Landau symbols en Isabelle/HOL.

Sus autor es Manuel Eberl (del Theorem Proving Group en la Technische Universität München, Munich, Alemania).

Su resumen es

This entry provides Landau symbols to describe and reason about the asymptotic growth of functions for sufficiently large inputs. A number of simplification procedures are provided for additional convenience: cancelling of dominated terms in sums under a Landau symbol, cancelling of common factors in products, and a decision procedure for Landau expressions containing products of powers of functions like x, ln(x), ln(ln(x)) etc.

El trabajo se ha publicado en The Archive of Formal Proofs.

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

Este trabajo puede servir como lectura complementaria del curso de Razonamiento automático.

Reseña: MathCheck: A math assistant via a combination of computer algebra systems and SAT solvers

Se ha publicado un artículo de aplicación del razonamiento automático en la enseñanza titulado MathCheck: A math assistant via a combination of computer algebra systems and SAT solvers.

Sus autores son
+ Edward Zulkoski (del GSD Lab (Generative software development lab))
+ Vijay Ganesh (del Waterloo computer-aided reasoning group) y
+ Krzysztof Czarnecki (del GSD Lab (Generative software development lab))

de la Univ. de Waterloo, Ontario, Canadá.

Su resumen es

We present a method and an associated system, called Math-Check, that embeds the functionality of a computer algebra system (CAS) within the inner loop of a conflict-driven clause-learning SAT solver. SAT+CAS systems, a la MathCheck, can be used as an assistant by mathematicians to either counterexample or finitely verify open universal conjectures on any mathematical topic (e.g., graph and number theory, algebra, geometry, etc.) supported by the underlying CAS system. Such a SAT+CAS system combines the efficient search routines of modern SAT solvers, with the expressive power of CAS, thus complementing both. The key insight behind the power of the SAT+CAS combination is that the CAS system can help cut down the search-space of the SAT solver, by providing learned clauses that encode theory-specific lemmas, as it searches for a counterexample to the input conjecture (just like the T in DPLL(T)). In addition, the combination enables a more efficient encoding of problems than a pure Boolean representation.

In this paper, we leverage the graph-theoretic capabilities of an open-source CAS, called SAGE. As case studies, we look at two long-standing open mathematical conjectures from graph theory regarding properties of hypercubes: the first conjecture states that any matching of any d-dimensional hypercube can be extended to a Hamiltonian cycle; and the second states that given an edge-antipodal coloring of a hypercube, there always exists a monochromatic path between two antipodal vertices. Previous results have shown the conjectures true up to certain low-dimensional hypercubes, and attempts to extend them have failed until now. Using our SAT+CAS system, MathCheck, we extend these two conjectures to higher-dimensional hypercubes. We provide detailed performance analysis and show an exponential reduction in search space via the SAT+CAS combination relative to finite brute-force search.

El trabajo se ha presentado en el CADE-25 (The 25th International Conference on Automated Deduction).

El sistema MatCheck se encuentra aquí y su código aquí.

Reseña: Exploring theories with a model-finding assistant

Se ha publicado un artículo de automatización del razonamiento titulado Exploring theories with a model-finding assistant.

Sus autores son Salman Saghafi, Ryan Danas y Daniel J. Dougherty (del Applied Logic and Security Lab en el Worcester Polytechnic Institute, Worcester, Massachusetts, USA).

Su resumen es

We present an approach to understanding first-order theories by exploring their models. A typical use case is the analysis of artifacts such as policies, protocols, configurations, and software designs. For the analyses we offer, users are not required to frame formal properties or construct derivations. Rather, they can explore examples of their designs, confirming the expected instances and perhaps recognizing bugs inherent in surprising instances.

Key foundational ideas include: the information preorder on models given by homomorphism, an inductively-defined refinement of the Herbrand base of a theory, and a notion of provenance for elements and facts in models. The implementation makes use of SMT-solving and an algorithm for minimization with respect to the information preorder on models.

Our approach is embodied in a tool, Razor, that is complete for finite satisfiability and provides a read-eval-print loop used to navigate the set of finite models of a theory and to display provenance.

El trabajo se ha presentado en el CADE-25 (The 25th International Conference on Automated Deduction).

El código en Haskell del sistema Razor se encuentra aquí.

Este trabajo puede servir en los cursos de Lógica informática, Lógica matemática y fundamentos, Razonamiento automático y Lógica computacional y teoría de modelos.

Reseña: Stumbling around in the dark: Lessons from everyday mathematics

Se ha publicado un artículo sobre el papel de la lógica computacional en el desarrollo matemático titulado Stumbling around in the dark: Lessons from everyday mathematics.

Su autora es Ursula Martin (de la Univ. de Oxford).

Su resumen es

The growing use of the internet for collaboration, and of numeric and symbolic software to perform calculations it is impossible to do by hand, not only augment the capabilities of mathematicians, but also afford new ways of observing what they do. In this essay we look at four case studies to see what we can learn about the everyday practice of mathematics: the polymath experiments for the collaborative production of mathematics, which tell us about mathematicians attitudes to working together in public; the minipolymath experiments in the same vein, from which we can examine in finer grained detail the kinds of activities that go on in developing a proof; the mathematical questions and answers in math overflow, which tell us about mathematical-research-in-the-small; and finally the role of computer algebra, in particular the GAP system, in the production of mathematics. We conclude with perspectives on the role of computational logic.

El trabajo se ha presentado como conferencia invitada en el CADE-25. Las transparencias de la presentación se encuentran aquí.