Catálogo de publicaciones - libros

We discuss the halting probability Ω, whose bits are irreducible mathematical facts, that is, facts which cannot be derived from any principles simpler than they are. In other words, you need a mathematical theory with bits of axioms in order to be able to determine bits of Ω. This pathological property of Ω is difficult to reconcile with traditional philosophies of mathematics and with traditional views of the nature of mathematical proof and of mathematical knowledge. Instead Ω suggests a quasi-empirical view of math that emphasizes the similarities between mathematics and physics rather than the differences.

Math-aware fine-grain search is expected to be widely available. A key question is what roles it can play in mathematics. It will be argued that, besides finding information, math search can help advance and manage mathematical knowledge. This paper will present the short-term goals and state of the art of math-aware fine-grain search. Afterwards, it will focus on how math search can help advance and manage mathematical knowledge, and discuss what needs to be done to fulfill those roles, emphasizing two key components. The first is similarity search, and how it applies to (1) discovering and drawing upon connections between different fields, and (2) proof development. The second is math metadata, which math search will surely encourage and benefit from, and which will be pivotal to mathematical knowledge management.

Isabelle/Isar is a generic framework for human-readable formal proof documents, based on higher-order natural deduction. The Isar proof language provides general principles that may be instantiated to particular object-logics and applications. We discuss specific Isar language elements that support complex induction patterns of practical importance. Despite the additional bookkeeping required for induction with local facts and parameters, definitions, simultaneous goals and multiple rules, the resulting Isar proof texts turn out well-structured and readable. Our techniques can be applied to non-standard variants of induction as well, such as co-induction and nominal induction. This demonstrates that Isar provides a viable platform for building domain-specific tools that support fully-formal mathematical proof composition.

The generic proof assistant Isabelle provides a landscape of specification contexts that is considerably richer than that of most other provers. Theories are the level of specification where object-logics are axiomatised. Isabelle’s proof language Isar enables local exploration in contexts generated in the course of natural deduction proofs. Finally, locales, which may be seen as detached proof contexts, offer an intermediate level of specification geared towards reuse. All three kinds of contexts are structured, to different extents. We analyse the “topology” of Isabelle’s landscape of specification contexts, by means of development graphs, in order to establish what kinds of reuse are possible.

Proofs contain important mathematical knowledge and for mathematical knowledge management it is important to represent them adequately. They can be given at different levels of abstraction and writing a proof is typically a compromise between two extremes. On the one hand it should be in full detail so that it can be checked without using any intelligence, on the other hand it should be concise and informative. Making everything fully explicit is not adequate for most mathematical fields since easy parts do not need any communication. In particular in traditional proofs, computations are typically not made explicit, but a reader is expected to check them for him- or herself. Barendregt formulated a principle, the Poincaré Principle, which allows to separate reasoning and computation. However, should any computation be hidden? Or only easy computations? What is easy? How can we be sure that computations are correct? In this contribution, relevant notions are discussed and a principle is introduced which allows for checkable proofs which give a choice to see on request two different types of argument. The first type of argument states why any computation of this kind is correct. The second type states a (typically lengthy) detailed low-level proof of a trace of the computation.

and , programs that represent and execute several steps of deduction, are fundamental to theorem provers providing automated tools for creating proofs quickly and easily. The language used for tactics is usually a full-scale programming language, separate from the language used to represent proofs. Consequently, there is also a separation between the use of theorems in proofs and the use of tactics. Our goal is to represent tactics in a way that allows them to be treated at the same level as proofs and theorems. We also want a representation that allows us to formally translate tactics into the proof steps they represent. We extend a system presented in [1,2] to represent tactics at the same level as theorems and move freely from tactics to proof steps and provide an example of its usefulness.

We consider an extension of OMDoc proofs with alternative sub-proofs and proofs at different level of detail, and an affine non-deterministic fragment of the -calculus seen as a proof format. We provide explanations in pseudo-natural language of proofs in both formats, and a formal correspondence between the two by means of two mutually inverse encodings of one format in the other one.

Cut-elimination is the most prominent form of proof transformation in logic. The elimination of cuts in formal proofs corresponds to the removal of intermediate statements (lemmas) in mathematical proofs. The cut-elimination method CERES (cut-elimination by resolution) works by constructing a set of clauses from a proof with cuts. Any resolution refutation of this set then serves as a skeleton of an -proof with only atomic cuts.

In this paper we present an extension of CERES to a calculus which is stronger than the Gentzen calculus (it contains rules for introduction of definitions and equality rules). This extension makes it much easier to formalize mathematical proofs and increases the performance of the cut-elimination method. The system CERES already proved efficient in handling very large proofs.

In this paper we investigate how to extract proof procedural information contained in declarative representations of mathematical knowledge, such as axioms, definitions, lemmas and theorems (collectively called ) and how to effectively include it into automated proof search techniques. In the context of the proof planner and the agent-based reasoning system Ω-, we present techniques to automatically synthesize proof planning methods and Ω--agents from assertions such that they can be used by these systems. This in turn enables a user to effectively use these systems without having to know the peculiarities of coding methods and agents.

Many textbook proofs are essentially human-readable representations of natural deduction proofs. Terms in dependent type theory provide formally checkable representations of natural deduction proofs. We show how the new mathematical assistant system Scunak can be used to verify a textbook proof by translating the version into a proof term in a dependent type theory. We also show how Scunak can give interesting output upon failure.