eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
15
10.4230/DagSemProc.05021.1
article
05021 Abstracts Collection – Mathematics, Algorithms, Proofs
Coquand, Thierry
Lombardi, Henri
Roy, Marie-Françoise
From 09.01.05 to 14.01.05, the Dagstuhl Seminar 05021 ``Mathematics, Algorithms, Proofs'' was held in the International Conference and Research Center (IBFI),
Schloss Dagstuhl.
During the seminar, several participants presented their current
research, and ongoing work and open problems were discussed. Abstracts of
the presentations given during the seminar as well as abstracts of
seminar results and ideas are put together in this paper. The first section
describes the seminar topics and goals in general.
LinkstFo extended abstracts or full papers are provided, if available.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.1/DagSemProc.05021.1.pdf
Constructive mathematics
computer algebra
proof systems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
3
10.4230/DagSemProc.05021.2
article
05021 Executive Summary – Mathematics, Algorithms, Proofs
Coquand, Thierry
This workshop was the third MAP meeting,
a continuation of the seminar "Verification and constructive algebra" held in Dagstuhl from 6 to 10 January 2003.
The goal of these meetings is to bring together people from the communities of formal proofs, constructive
mathematics and computer algebra (in a wide meaning).
The special
emphasis of the present meeting was on the constructive mathematics and efficient proofs in computer algebra.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.2/DagSemProc.05021.2.pdf
Constructive mathematics
computer algebra
proof systems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
9
10.4230/DagSemProc.05021.3
article
A dynamical solution of Kronecker's problem
Yengui, Ihsen
In this paper,
I present a new decision procedure for the ideal
membership problem for polynomial rings over principal domains
using discrete valuation domains. As a particular case, I solve a
fundamental algorithmic question in the theory of multivariate
polynomials over the integers called ``Kronecker's problem", that
is the problem of finding a decision procedure for the ideal
membership problem for $mathbb{Z}[X_1,ldots, X_n]$. The
techniques utilized are easily generalizable to Dedekind domains.
In order to avoid the expensive complete factorization in the
basic principal ring, I introduce the notion of ``dynamical
Gr"obner bases" of polynomial ideals over a principal domain. As
application, I give an alternative dynamical solution to
``Kronecker's problem".
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.3/DagSemProc.05021.3.pdf
Dynamical GrÃƒÂ¶bner basis
ideal membership problem
principal domains
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
6
10.4230/DagSemProc.05021.4
article
A Nilregular Element Property
Coquand, Thierry
Lombardi, Henri
Schuster, Peter
An element or an ideal of a commutative ring is nilregular if and only if
it is regular modulo the nilradical. We prove that if the ring is
Noetherian, then every nilregular ideal contains a nilregular element. In
constructive mathematics, this proof can then be seen as an algorithm to
produce nilregular elements of nilregular ideals whenever the ring is coherent,
Noetherian, and discrete. As an application, we give a constructive proof of
the Eisenbud--Evans--Storch theorem that every algebraic set in
$n$--dimensional affine space is the intersection of $n$ hypersurfaces.
The input of the algorithm is an arbitrary finite list of polynomials,
which need not arrive in a special form such as a Gr"obner basis.
We dispense with prime ideals when defining concepts or carrying out proofs.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.4/DagSemProc.05021.4.pdf
Lists of generators
polynomial ideals
Krull dimension
Zariski topology
commutative Noetherian rings
constructive algebra
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
2
10.4230/DagSemProc.05021.5
article
Abel and the Concept of the Genus of a Curve
Edwards, Harold M.
This talk is about the treatement of the Genus of a Curve by Abel, following the book "Essays in Constructive Mathematics".
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.5/DagSemProc.05021.5.pdf
Constructive Mathematics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
5
10.4230/DagSemProc.05021.6
article
Approximate fixed points of nonexpansive functions in product spaces
Kohlenbach, Ulrich
Leustean, Laurentiu
In this talk, we present another case study in the general program of proof mining in fixed point theory. Thus, we generalize results obtained by W. Kirk in the theory of approximated fixed points of nonexpansive mappings in product spaces
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.6/DagSemProc.05021.6.pdf
Proof mining
fixed point theory
approximated fixed points
nonexpansive functions
product spaces
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
12
10.4230/DagSemProc.05021.7
article
Certified mathematical hierarchies: the FoCal system
Prevosto, Virgile
The focal language (formerly Foc) allows a
programmer to incrementally build mathematical
structures and to formally prove their
correctness. focal encourages a development
process by refinement, deriving step-by-step
implementations from specifications. This
refinement process is realized using an
inheritance mechanism on structures which can mix
primitive operations, axioms, algorithms and
proofs. Inheritance from existing structures allows to reuse their components under some
conditions, which are statically checked by the compiler.
In this talk, we first present the main
constructions of the language. Then we show a
shallow embedding of these constructions in
the Coq proof assistant, which is used to check
the proofs made in Focal. Such a proof can be
either an hand-written Coq script, made in an
environment set up by the Focal compiler, or a
Coq term given the zenon theorem prover, which is partly developped within Focal. Last, we present a formalization of focal structures and show that the Coq embedding is conform to this model.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.7/DagSemProc.05021.7.pdf
Specifications
proofs
inheritance
refinement
types
Focal
Coq
computer algebra
mathematics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
12
10.4230/DagSemProc.05021.8
article
Coequalisers of formal topology
Palmgren, Erik
We give a predicative construction of quotients of formal topologies. Along with earlier results on the match up between of continuous functions on real numbers (in the sense of Bishop's constructive mathematics) and approximable mappings on the formal space of reals, we argue that formal topology gives an adequate foundation for constructive algebraic topology, also in the predicative sense. Predicativity is of essence when formalising the subject in logical frameworks based on Martin-LÃƒÂ¶f type theories.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.8/DagSemProc.05021.8.pdf
Formal topology
type theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
13
10.4230/DagSemProc.05021.9
article
Constructive algebraic integration theory without choice
Spitters, Bas
We present a constructive algebraic integration theory. The theory is constructive in the sense of Bishop, however we avoid the axiom of countable, or dependent, choice. Thus our results can be interpreted in any topos. Since we avoid impredicative methods the results may also be interpreted in Martin-LÃƒÂ¶f type theory or in a predicative topos in the sense of Moerdijk and Palmgren.
We outline how to develop most of Bishop's theorems on integration theory that do not mention points explicitly. Coquand's constructive version of the
Stone representation theorem is an important tool in this process. It is also used to give a new proof of Bishop's spectral theorem.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.9/DagSemProc.05021.9.pdf
Algebraic integration theory
spectral theorem
choiceless constructive mathematics
pointfree topology
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
4
10.4230/DagSemProc.05021.10
article
Constructive Proofs or Constructive Statements?
Rubio Garcia, Julio
A question raised at previous MAP meetings is
the following. Is Sergeraert's "Constructive
Algebraic Topology" (CAT, in short) really
constructive (in the strict logical sense of the
word "constructive")? We have not an answer to
that question, but we are interested in the
following: could have a positive (or negative)
answer to the previous question an influence in
the problem of proving the correctness of CAT
programs (as Kenzo)?
Studying this problem, we have observed that, in
fact, many CAT programs can be extracted from
the statements (that is, from the specification
of certain objects and constructions), without
needing an extraction from proofs. This remark
shows that the logic used in the proofs is
uncoupled with respect to the correctness of
programs. Thus, the first question posed could
be quite irrelevant from the practical point of
view. These rather speculative ideas will be
illustrated by means of some elementary
examples, where the Isabelle code extraction
tool can be successfully applied.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.10/DagSemProc.05021.10.pdf
Program extraction
symbolic computation
constructive logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
0
10.4230/DagSemProc.05021.11
article
Diagrammatic logic and exceptions:an introduction
Duval, Dominique
Reynaud, Jean-Claude
For dealing with computational effects in computer
science, it may be helpful to use several logics:
typically, a logic with implicit effects for the
language, and a more classical logic for the user.
Hence, the study of computational effects should
take place in a framework where distinct logics
can be related. In this paper, such a framework is
presented: it is a category, called the category
of propagators. Each propagator defines a kind of
logic, called a diagrammatic logic, which is
endowed with a deduction system and a sound notion
of models. Morphisms of propagators provide the
required relationships between diagrammatic
logics. The category of propagators has been
introduced by Duval and Lair in 2002, it is based
on the notion of sketches, which is due to
Ehresmann in the 1960's. Then, the paper outlines
how Duval and Reynaud in 2004 used the category of
propagators for dealing with the computational
effect of raising and handling exceptions. Another
application of diagrammatic logic is presented by
Dominguez et al. in the same conference
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.11/DagSemProc.05021.11.pdf
Specifications
Semantics
Exceptions
Sketches
Diagrammatic Logic
Extensive Categories
Monads.
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
7
10.4230/DagSemProc.05021.12
article
Enabling conditions for interpolated rings
Richman, Fred
If A is a subring of a ring B, then an interpolated ring is the union of A and {b in B : P} for some proposition P. These interpolated rings come up frequently in the construction of Brouwerian examples. We study conditions on the inclusion of A in B that guarantee, for some property of rings, that if A and B both have that property, then so does any interpolated ring. Classically, no condition is necessary because each interpolated ring is either A or B. We also would like such a condition to be necessary in the sense that if it fails, and every interpolated ring has the property, then some omniscience principle holds.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.12/DagSemProc.05021.12.pdf
Brouwerian example
interpolated ring
intuitionistic algebra
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
5
10.4230/DagSemProc.05021.13
article
Generalized metatheorems on the extractability of uniform bounds in functional analysis
Gerhardy, Philipp
Kohlenbach, Ulrich
Recently U.Kohlenbach proved general metatheorems for the extraction of (uniform) bounds from classical
proofs in functional analysis. The proof was based on
a combination of GÃƒÂ¶del's functional interpretation
and Bezem's strong majorization relation. We present
a generalization of the majorization relation which
allows to generalize Kohlenbach's metatheorems
significantly. Finally, we will discuss some examples
which are now covered by the new metatheorems.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.13/DagSemProc.05021.13.pdf
Proof mining
majorization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
8
10.4230/DagSemProc.05021.14
article
Henselian Local Rings: Around a Work in Progress
Perdry, Hervé
Alonso, Mariemi
Lombardi, Henri
I shall outline an elementary and effective construction of the Henselization of a local ring (which could be implemented in some computer algebra systems) and an effective proof of several classical results about Henselian local rings.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.14/DagSemProc.05021.14.pdf
Local rings
henselian local rings
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
2
10.4230/DagSemProc.05021.15
article
Introduction to My Book "Essays in Constructive Mathematics"
Edwards, Harold M.
The talk will describe the overall approach and the major topics of the book, recently published by Springer.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.15/DagSemProc.05021.15.pdf
Constructive Mathematics
Galois Theory
Genus of a Curve.
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
11
10.4230/DagSemProc.05021.16
article
Introduction to the Flyspeck Project
Hales, Thomas C.
This article gives an introduction to a long-term project called Flyspeck, whose purpose is to give a formal verification of the Kepler Conjecture. The Kepler Conjecture asserts that the density of a
packing of equal radius balls in three dimensions cannot exceed $pi/sqrt{18}$.
The original proof of the Kepler Conjecture, from 1998, relies extensively on computer calculations. Because the proof relies on relatively few external results, it is a natural choice for a formalization effort.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.16/DagSemProc.05021.16.pdf
Certified proofs
Kepler conjecture
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
18
10.4230/DagSemProc.05021.17
article
Programming and certifying a CAD algorithm in the Coq system
Mahboubi, Assia
A. Tarski has shown in 1948 that one can perform quantifier elimination in the theory of real closed fields. The introduction of the Cylindrical Algebraic Decomposition (CAD) method has later allowed to design rather feasible algorithms. Our aim is to program a reflectional decision procedure for the Coq system, using the CAD, to decide whether a (possibly multivariate) system of polynomial inequalities with rational coefficients has a solution or not. We have therefore
implemented various computer algebra tools
like gcd computations, subresultant polynomial or Bernstein polynomials.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.17/DagSemProc.05021.17.pdf
Computer algebra
Bernstein polynomials
subresultants
CAD
Coq
certification.
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
2
10.4230/DagSemProc.05021.18
article
Proving Bounds for Real Linear Programs in Isabelle/HOL
Obua, Steven
Linear programming is a basic mathematical technique for optimizing a
linear function on a domain that is constrained by linear inequalities.
We restrict ourselves to linear programs on bounded domains that involve only
real variables. In the context of theorem proving, this restriction makes it
possible for any given linear program to obtain certificates from external
linear programming tools that help to prove arbitrarily precise bounds for the
given linear program. To this end, an explicit formalization of matrices
in Isabelle/HOL is presented, and how the concept of lattice-ordered rings
allows for a smooth integration of matrices with the axiomatic type classes of
Isabelle.
As our work is a contribution to the Flyspeck project, we demonstrate that via
reflection and with the above techniques it is now possible to prove bounds
for the linear programs arising in the proof of the Kepler conjecture
sufficiently fast.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.18/DagSemProc.05021.18.pdf
Certified proofs
Kepler conjecture
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
3
10.4230/DagSemProc.05021.19
article
Some Notes On ``When is 0.999... equal to 1?
Schneider, Carsten
In joint work Robin Pemantle and I (2004) consider a doubly infinite sum which is not equal to 1, as first suspected, but evaluates to a sum of products of values of the zeta function. Subsequently, I report on this project.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.19/DagSemProc.05021.19.pdf
Symbolic summation
computer algebra
proofs
harmonic numbers
zeta-relations
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
4
10.4230/DagSemProc.05021.20
article
Subdiscriminant of symmetric matrices are sums of squares
Roy, Marie-Françoise
We present a very elementary algebraic proof providing an explicit sum of squares.
This result generalizes a result on discriminants of symmetric matrices
due to Ilyushechkin
and proved also by P. Lax.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.20/DagSemProc.05021.20.pdf
Real algebra
sums of squares
subdiscriminants
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
25
10.4230/DagSemProc.05021.21
article
Towards a Verified Enumeration of All Tame Plane Graphs
Nipkow, Tobias
Bauer, Gertrud
In his proof of the Kepler conjecture, Thomas Hales introduced the notion of tame graphs and provided a Java program for enumerating all tame plane graphs. We have translated his Java program into an executable function in HOL ("the generator"), have formalized the notions of tameness and planarity in HOL, and have partially proved that the generator returns all tame plane graphs. Running the generator in ML has shows that the list of plane tame graphs ("the archive") that Thomas Hales also provides is complete. Once we have finished the completeness proof for the generator.
In addition we checked the redundancy of the archive by formalising an executable notion of isomorphism between plane graphs, and checking if the archive contains only graphs produced by the generator. It turned out that 2257 of the 5128 graphs in the archive are either not tame or isomorphic to another graph in the archive.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.21/DagSemProc.05021.21.pdf
Kepler conjecture
certified proofs
flyspeck
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
23
10.4230/DagSemProc.05021.22
article
Towards Diagrammatic Specifications of Symbolic Computation Systems
Dominguez, César
Duval, Dominique
Lamban, Laureano
Rubio Garcia, Julio
The aim of this work is to present an ongoing project to
formalize, in the framework of diagrammatic logic (due to
Dominique Duval and Christian Lair) some data structures appearing
in Sergeraert's symbolic computation systems Kenzo and EAT. More
precisely, we intend to translate into the diagrammatic setting a
previous work based on standard algebraic specification
techniques. In particular, we give hints on the reason why an
important construction (called imp construction) in the
specification of the systems can be understood as a freely
generating functor between suitable categories of diagrammatic
realizations. Even if very partial, these positive results seem to
indicate that this new kind of specification is promising in the
field of symbolic computation.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.22/DagSemProc.05021.22.pdf
Specification
symbolic computation
sketches
diagrammatic logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-16
5021
1
20
10.4230/DagSemProc.05021.23
article
Unifying Functional Interpretations
Oliva, Paulo
The purpose of this article is to present a parametrised functional interpretation. Depending on the choice of the two parameters one obtains well-known functional interpretations, among others GÃƒÂ¶del's Dialectica interpretation, Diller-Nahm's variant of the Dialectica interpretation, Kreisel's modified realizability, Kohlenbach's monotone interpretations and Stein's family of functional interpretations. We show that all these interpretations only differ on two basic choices, which are captured by the parameters, namely the choices of (1) "how much" of the counter-examples for A becomes witnesses for the negation of A, and of (2) "how much" information about the witnesses of A one is interested in.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.23/DagSemProc.05021.23.pdf
Functional interpretation
modified realizability
Dialectica interpretation
intuitionistic logic