Menu Close

Etiqueta: Reseña

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

Reseña: Formalising type-logical grammars in Agda

Se ha publicado un artículo de razonamiento formalizado en Agda titulado Formalising type-logical grammars in Agda.

Su autor es Pepijn Kokke (de la Univ. de Utrecht, Países Bajos).

Su resumen es

In recent years, the interest in using proof assistants to formalise and reason about mathematics and programming languages has grown. Type-logical grammars, being closely related to type theories and systems used in functional programming, are a perfect candidate to next apply this curiosity to. The advantages of using proof assistants is that they allow one to write formally verified proofs about one’s type-logical systems, and that any theory, once implemented, can immediately be computed with. The downside is that in many cases the formal proofs are written as an afterthought, are incomplete, or use obtuse syntax. This makes it that the verified proofs are often much more difficult to read than the pen-and-paper proofs, and almost never directly published. In this paper, we will try to remedy that by example.

Concretely, we use Agda to model the Lambek-Grishin calculus, a grammar logic with a rich vocabulary of type-forming operations. We then present a verified procedure for cut elimination in this system. Then we briefly outline a continuation-passing style translation from proofs in the Lambek-Grishin calculus to programs in Agda. And finally, we will put our system to use in the analysis of a simple example sentence.

El trabajo se ha presentado en TYpe Theory and LExical Semantics.

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

Reseña: Efficient, mechanically-verified validation of satisfiability solvers

Se ha publicado una tesis doctoral de razonamiento formalizado en ACL2 Efficient, mechanically-verified validation of satisfiability solvers.

Su autor es Nathan Wetzler (de The Mechanized Theorem Proving Group en The University of Texas at Austin).

Los directores de la tesis son Warren A. Hunt, Jr. y Marijn J. H. Heule.

Su resumen es

Satisfiability (SAT) solvers are commonly used for a variety of applications, including hardware verification, software verification, theorem proving, debugging, and hard combinatorial problems. These applications rely on the efficiency and correctness of SAT solvers. When a problem is determined to be unsatisfiable, how can one be confident that a SAT solver has fully exhausted the search space? Traditionally, unsatisfiability results have been expressed using resolution or clausal proof systems. Resolution-based proofs contain perfect reconstruction information, but these proofs are extremely large and difficult to emit from a solver. Clausal proofs rely on rediscovery of inferences using a limited number of techniques, which typically takes several orders of magnitude longer than the solving time. Moreover, neither of these proof systems has been able to express contemporary solving techniques such as bounded variable addition. This combination of issues has left SAT solver authors unmotivated to produce proofs of unsatisfiability.

The work from this dissertation focuses on validating satisfiability solver output in the unsatisfiability case. We developed a new clausal proof format called DRAT that facilitates compact proofs that are easier to emit and capable of expressing all contemporary solving and preprocessing techniques. Furthermore, we implemented a validation utility called DRAT-trim that is able to validate proofs in a time similar to that of the discovery time. The DRAT format has seen widespread adoption in the SAT community and the DRAT-trim utility was used to validate the results of the 2014 SAT Competition.

DRAT-trim uses many advanced techniques to realize its performance gains, so why should the results of DRAT-trim be trusted? Mechanical verification enables users to model programs and algorithms and then prove their correctness with a proof assistant, such as ACL2. We designed a new modeling technique for ACL2 that combines efficient model execution with an agile and convenient theory. Finally, we used this new technique to construct a fast, mechanically-verified validation tool for proofs of unsatisfiability. This research allows SAT solver authors and users to have greater confidence in their results and applications by ensuring the validity of unsatisfiability results.

Reseña: TryLogic tutorial (An approach to learning Logic by proving and refuting)

Se ha publicado un artículo de aplicación del razonamiento asistido por ordenador a la enseñanza titulado TryLogic tutorial: An approach to learning Logic by proving and refuting

Sus autores son Patrick Terrematte y João Marcos (del Group for Logic, Language, Information, Theory and Applications (LoLITA) en la Federal University of Rio Grande do Norte (UFRN) de Brasil).

Su resumen es

Aiming to offer a framework for blended learning to the teaching of proof theory, the present paper describes an interactive tutorial, called TryLogic, teaching how to solve logical conjectures either by proofs or refutations. The paper also describes the integration of our infrastructure with the Virtual Learning Environment Moodle through the IMS Learning Tools Interoperability specification, and evaluates the tool we have developed.

El trabajo se ha presentado en TTL2015 (Fourth International Conference on Tools for Teaching Logic)

Reseña: Formal study of functional orbits in finite domains

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Formal study of functional orbits in finite domains.

Su autor es Jean-François Dufourd (del grupo Computer Science in Geometry and Graphics (IGG) en la Univ. de Estrasburgo, Francia).

Su resumen es

In computer science, functional orbits − i.e tracks left by iterating a function − in a finite domain naturally appear at a high or a low level. This paper introduces a Coq logical orbit framework, the purpose of which is to help rigorously developing software systems with some complex data structures from specification to implementation.

The result is a Coq library of orbit concepts formalized as definitions, lemmas and theorems. Most of them are inspired by our previous work in geometric modelling, where combinatorial hypermaps were used to describe surface subdivisions appearing in computational geometry problems, e.g. building convex hulls or Delaunay diagrams. Now, this domain remains a reference for us, but our results are drastically extended and usable in other computer science areas. The proof of Floyd’s cycle-detection algorithm, known as “the tortoise and the hare”, confirms that point.

The library contains operations to observe, traverse and update orbits − addition, deletion, mutation, transposition − with proofs of their behavior. It focuses on the important case where the involved function is a partial injection. In this case, it defines a connectivity relationship and evaluates the variation of the number of connected components during updates.

El trabajo se ha publicado en Theoretical Computer Science.