From 7e6b1084a85f42ff8518c20ec3908f3043e9f727 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Sun, 24 Sep 2017 13:20:57 -0400
Subject: [PATCH] books/bookvolbib add Coercion references
Goal: Proving Axiom Correct
\index{Traytel, Dmitriy}
\index{Berghofer, Stefan}
\index{Nipkow, Tobias}
\begin{chunk}{axiom.bib}
@article{Tray11,
author = "Traytel, Dmitriy and Berghofer, Stefan and Nipkow, Tobias",
title = "Extending Hindley-Milner Type Inference with Coercive
Structural Subtyping",
journal = "LNCS",
volume = "7078",
pages = "89-104",
year = "2011",
abstract =
"We investigate how to add coercive structural subtyping to a type
system for simply-typed lambda calculus with Hindley-Milner
polymorphism. Coercions allow to convert between different types, and
their automatic insertion can greatly increase readability of
terms. We present a type inference algorithm that, given a term
without type information, computes a type assignment and determines at
which positions in the term coercions have to be inserted to make it
type-correct according to the standard Hindley-Milner system (without
any subtypes). The algorithm is sound and, if the subtype relation
on base types is a disjoint union of lattices, also complete. The
algorithm has been implemented in the proof assistant Isabelle.",
paper = "Tray11.pdf",
keywords = "coercion"
}
\end{chunk}
\index{Ab\'anades, M.}
\index{Botana, F.}
\index{Kov\'acs, Z.}
\index{Recio, T.}
\index{S\'olyom-Gecse, C.}
\begin{chunk}{axiom.bib}
@article{Aban16,
author = "Abanades, M. and Botana, F. and Kovacs, Z. and Recio, T. and
Solyom-Gecse, C.",
title = "Development of automatic reasoning tools in GeoGebra",
journal = "ACM Comm. Computer Algebra",
volume = "50",
pages = "85-88",
year = "2016",
abstract =
"Much effort has been put into the implementation of automatic proving
in interactive geometric environments (e.g. Java Geometry Expert,
GeoGebra). The closely related concept of automatic discovery, remains
however almost unexplored.
This software presentation will demonstrate our results towards the
incorporation of automatic discovery capabilities into GeoGebra, an
educational software with tens of millions of users worldwide. As main
result, we report on a new command, currently available in the
official version, that allows the automatic discovery of loci of
points in diagrams defined by implicit conditions. This represents an
extension of a previous command, similar in nature, but restricted to
loci defined by the standard mover-tracer construction. Our proposal
successfully automates the `dummy locus dragging' in dynamic
geometry. This makes the cycle conjecturing-checking-proving
accessible for general users in elementary geometry.",
paper = "Aban16.pdf"
}
\end{chunk}
\index{Avigad, Jeremy}
\begin{chunk}{axiom.bib}
@article{Avig12a,
author = "Avigad, Jeremy",
title = "Type Inference in Mathematics",
journal = "European Association of Theoretical Computer Science",
volume = "106",
pages = "78-98",
year = "2012",
abstract =
"In the theory of programming languages, type inference is the process
of inferring the type of an expression automatically, often making use
of information from the context in which the expression appears. Such
mechanisms turn out to be extremely useful in the practice of
interactive theorem proving, whereby users interact with a
computational proof assistant to construct formal axiomatic
derivations of mathematical theorems. This article explains some of
the mechanisms for type inference used by the Mathematical
Components project, which is working towards a verification of the
Feit-Thompson theorem.",
paper = "Avig12a.pdf",
keywords = "coercion"
}
\end{chunk}
\index{Abraham, Erika}
@inproceedings{Abra15,
author = "Abraham, Erika",
title = "Building Bridges between Symbolic Computation and Satisfiability
Checking",
booktitle = "ISSAC 15",
year = "2015",
pages = "1-6",
publisher = "ACM",
isbn = "978-1-4503-3435-8",
abstract =
"The satisfiability problem is the problem of deciding whether a
logical formula is satisfiable. For first-order arithmetic theories,
in the early 20th century some novel solutions in form of decision
procedures were developed in the area of mathematical logic. With the
advent of powerful computer architectures, a new research line started
to develop practically feasible implementations of such decision
procedures. Since then, symbolic computation has grown to an extremely
successful scientific area, supporting all kinds of scientific
computing by efficient computer algebra systems.
Independently, around 1960 a new technology called SAT solving started
its career. Restricted to propositional logic, SAT solvers showed to
be very efficient when employed by formal methods for verification. It
did not take long till the power of SAT solving for Boolean problems
had been extended to cover also different theories. Nowadays, fast
SAT-modulo-theories (SMT) solvers are available also for arithmetic
problems.
Due to their different roots, symbolic computation and SMT solving
tackle the satisfiability problem differently. We discuss differences
and similarities in their approaches, highlight potentials of
combining their strengths, and discuss the challenges that come with
this task.",
paper = "Abra15.pdf"
}
\end{chunk}
\index{Abraham, Erika}
\begin{chunk}{axiom.bib}
@inproceedings{Abra16,
author = "Abraham, Erika",
title = "Symbolic Computation Techniques in Satisfiability Checking",
booktitle = "SYNASC 2016",
publisher = "IEEE Press",
year = "2016",
isbn = "978-1-5090-5707-8",
pages = "3-10"
}
\end{chunk}
\index{Kauers, Manuel}
\begin{chunk}{axiom.bib}
@article{Kaue11,
author = "Kauers, Manuel",
title = "How to use Cylindrical Algebraic Decomposition",
journal = {S\'emminaire Lotharingien de Combinatoire},
volume = "65",
year = "2011",
comment = "Article B65a",
abstract =
"We take some items from a textbook on inequalities and show how to
prove them with computer algebra using the Cylindrical Algebraic
Decomposition algorithm. This is an example collection for standard
applications of this algorithm, intended as a guide for potential users.",
paper = "Kaue11.pdf"
}
\end{chunk}
\index{Abraham, Erika}
\index{Jebelean, Tudor}
\begin{chunk}{axiom.bib}
@inproceedings{Abra17,
author = "Abraham, Erika and Jebelean, Tudor",
title = "Adapting Cylindrical Algebraic Decomposition for Proof Specific
Tasks",
booktitle = "IJCAI 2017",
year = "2017",
comment = "Extended Abstract",
paper = "Abra17.pdf"
}
\end{chunk}
\index{Abraham, Erika}
\index{Abbott, John}
\index{Becker, Bernd}
\index{Bigatti, Anna M.}
\index{Brain, Martin}
\index{Cimatti, Alessandro}
\index{Davenport, James H.}
\index{England, Matthew}
\index{Fontaine, Pascal}
\index{Forrest, Stephen}
\index{Ganesh, Vijay}
\index{Griggio, Alberto}
\index{Kroenig, Daniel}
\index{Seiler, Werner M.}
\begin{chunk}{axiom.bib}
@misc{Abraxx,
author = "Abraham, Erika and Abbott, John and Becker, Bernd and
Bigatti, Anna M. and Brain, Martin and Cimatti, Alessandro and
Davenport, James H. and England, Matthew and Fontaine, Pascal
and Forrest, Stephen and Ganesh, Vijay and Griggio, Alberto and
Kroenig, Daniel and Seiler, Werner M.",
title = "SC2 challenges: when Satisfiability Checking and Symbolic
Computation join forces",
year = "2017",
abstract =
"Symbolic Computation and Satisfiability Checking are two research
areas, both having their individual scientific focus but with common
interests, e.g., in the development, implementation and application
of decision procedures for arithmetic theories. Despite their
commonalities, the two communities are rather weakly connected. The
aim of the SC 2 initiative is to strengthen the connection between
these communities by creating common platforms, initiating interaction
and exchange, identifying common challenges, and developing a common
roadmap from theory along the way to tools and (industrial) applications.",
paper = "Abraxx.pdf"
}
\end{chunk}
\index{de Moura, Leonardo}
\index{Avigad, Jeremy}
\index{Kong, Soonho}
\index{Roux, Cody}
\begin{chunk}{axiom.bib}
@misc{Mour15,
author = "de Moura, Leonardo and Avigad, Jeremy and Kong, Soonho and
Roux, Cody",
title = "Elaboration in Dependent Type Theory",
year = "2015",
abstract =
"To be usable in practice, interactive theorem provers need to provide
convenient and efficient means of writing expressions, definitions,
and proofs. This involves inferring information that is often left
implicit in an ordinary mathematical text, and resolving ambiguities
in mathematical expressions. We refer to the process of passing from a
quasi-formal and partially- specified expression to a completely
precise formal one as {\sl elaboration}. We describe an elaboration
algorithms for dependent type theory that has been implemented in the
Lean theorem prover. Lean's elaborator supports higher-order
unification, type class inference, ad hoc overloading, insertion of
coercions, the use of tactics, and the computational reduction of
terms. The interactions between these components are subtle and
complex, and the elaboration algorithm has been carefully designed to
balance efficiency and usability. We describe the central design
goals, and the means by which they are achieved.",
paper = "Mour15.pdf",
keywords = "coercion"
}
\end{chunk}
\index{Reynolds, John C.}
\begin{chunk}{axiom.bib}
@article{Reyn05,
author = "Reynolds, John C.",
title = "An Overview of Separation Logic",
journal = "LNCS",
volume = "4171",
pages = "460-469",
abstract =
"After some general remarks about program verification, we introduce
separation logic, a novel extension of Hoare logic that can strengthen
the applicability and scalability of program verification for
imperative programs that use shared mutable data structures or
shared-memory concurrency",
paper = "Reyn05.pdf",
}
\end{chunk}
\index{Reynolds, John C.}
\begin{chunk}{axiom.bib}
@inproceedings{Reyn02,
author = "Reynolds, John C.",
title = "Separation Logic: A Logic for Shared Mutable Data Structures",
booktitle = "Logic in Computer Science '02",
year = "2002",
pages = "55-74",
isbn = "0-7695-1483-9",
abstract =
"In joint work with Peter O'Hearn and others, based on early ideas of
Burstall, we have developed an extension of Hoare logic that permits
reasoning about low-level imperativeprograms that use shared mutable
data structure.The simple imperative programming language is extended
with commands (not expressions) for accessing and modifying shared
structures, and for explicit allocation and deallocation of
storage. Assertions are extended by introducing a "separating
conjunction" that asserts that its sub-formulas hold for disjoint
parts of the heap, and a closely related "separating
implication". Coupled with the inductive definition of predicates on
abstract data structures, this extension permits the concise and
flexible description of structures with controlled sharing.In this
paper, we will survey the current development of this program logic,
including extensions that permit unrestricted address arithmetic,
dynamically allocated arrays, and recursive procedures. We will also
discuss promising future directions.",
paper = "Reyn02.pdf"
}
\end{chunk}
\index{Hearn, Peter W.O.}
\begin{chunk}{axiom.bib}
@misc{Hear12,
author = "Hearn, Peter W.O.",
title = "A Primer on Separation Logic (and Automatic Program
Verification and Analysis",
year = "2012",
abstract =
"These are the notes to accompany a course at the Marktoberdorf PhD
summer school in 2011. The course consists of an introduction to
separation logic, with a slant towards its use in automatic program
verification and analysis.",
paper = "Hear12.pdf"
}
\end{chunk}
\index{Kaliszyk, Cezary}
\begin{chunk}{axiom.bib}
@phdthesis{Kali09,
author = "Kaliszyk, Cezary"
title = "Correctness and Availability: Building Computer Algebra on top
of Proof Assistants and making Proof Assistants available over
the Web",
year = "2009",
school = "Radboud University, Nijmegen",
link = "\url{http://cl-informatik.uibk.ac.at/users/cek/docs/09/kaliszyk\_thesis\_webdoc.pdf}",
abstract =
"In this thesis we present an approach to extending the usability
of proof assistants in mathematics and computer science. We do it
in two ways: by combining proof assistants with computer algebra
systems and by providing interactive access to such systems on
the web.",
paper = "Kali09.pdf"
}
\end{chunk}
---
books/axiom.bib | 267 +++++++++++++++++++++++++++++-
books/bookvolbib.pamphlet | 362 ++++++++++++++++++++++++++++++++++++++++-
changelog | 2 +
patch | 342 +++++++++++++++++++++++++++++++++++++-
src/axiom-website/patches.html | 2 +
5 files changed, 957 insertions(+), 18 deletions(-)
diff --git a/books/axiom.bib b/books/axiom.bib
index a184cd6..ff134a1 100644
--- a/books/axiom.bib
+++ b/books/axiom.bib
@@ -6636,12 +6636,119 @@ paper = "Brea89.pdf"
paper = "Yous04.pdf"
}
+@article{Aban16,
+ author = "Abanades, M. and Botana, F. and Kovacs, Z. and Recio, T. and
+ Solyom-Gecse, C.",
+ title = "Development of automatic reasoning tools in GeoGebra",
+ journal = "ACM Comm. Computer Algebra",
+ volume = "50",
+ pages = "85-88",
+ year = "2016",
+ abstract =
+ "Much effort has been put into the implementation of automatic proving
+ in interactive geometric environments (e.g. Java Geometry Expert,
+ GeoGebra). The closely related concept of automatic discovery, remains
+ however almost unexplored.
+
+ This software presentation will demonstrate our results towards the
+ incorporation of automatic discovery capabilities into GeoGebra, an
+ educational software with tens of millions of users worldwide. As main
+ result, we report on a new command, currently available in the
+ official version, that allows the automatic discovery of loci of
+ points in diagrams defined by implicit conditions. This represents an
+ extension of a previous command, similar in nature, but restricted to
+ loci defined by the standard mover-tracer construction. Our proposal
+ successfully automates the `dummy locus dragging' in dynamic
+ geometry. This makes the cycle conjecturing-checking-proving
+ accessible for general users in elementary geometry.",
+ paper = "Aban16.pdf"
+}
+
+@inproceedings{Abra15,
+ author = "Abraham, Erika",
+ title = "Building Bridges between Symbolic Computation and Satisfiability
+ Checking",
+ booktitle = "ISSAC 15",
+ year = "2015",
+ pages = "1-6",
+ publisher = "ACM",
+ isbn = "978-1-4503-3435-8",
+ abstract =
+ "The satisfiability problem is the problem of deciding whether a
+ logical formula is satisfiable. For first-order arithmetic theories,
+ in the early 20th century some novel solutions in form of decision
+ procedures were developed in the area of mathematical logic. With the
+ advent of powerful computer architectures, a new research line started
+ to develop practically feasible implementations of such decision
+ procedures. Since then, symbolic computation has grown to an extremely
+ successful scientific area, supporting all kinds of scientific
+ computing by efficient computer algebra systems.
+
+ Independently, around 1960 a new technology called SAT solving started
+ its career. Restricted to propositional logic, SAT solvers showed to
+ be very efficient when employed by formal methods for verification. It
+ did not take long till the power of SAT solving for Boolean problems
+ had been extended to cover also different theories. Nowadays, fast
+ SAT-modulo-theories (SMT) solvers are available also for arithmetic
+ problems.
+
+ Due to their different roots, symbolic computation and SMT solving
+ tackle the satisfiability problem differently. We discuss differences
+ and similarities in their approaches, highlight potentials of
+ combining their strengths, and discuss the challenges that come with
+ this task.",
+ paper = "Abra15.pdf"
+}
+
+@inproceedings{Abra16,
+ author = "Abraham, Erika",
+ title = "Symbolic Computation Techniques in Satisfiability Checking",
+ booktitle = "SYNASC 2016",
+ publisher = "IEEE Press",
+ year = "2016",
+ isbn = "978-1-5090-5707-8",
+ pages = "3-10"
+}
+
+@inproceedings{Abra17,
+ author = "Abraham, Erika and Jebelean, Tudor",
+ title = "Adapting Cylindrical Algebraic Decomposition for Proof Specific
+ Tasks",
+ booktitle = "IJCAI 2017",
+ year = "2017",
+ comment = "Extended Abstract",
+ paper = "Abra17.pdf"
+}
+
+@misc{Abraxx,
+ author = "Abraham, Erika and Abbott, John and Becker, Bernd and
+ Bigatti, Anna M. and Brain, Martin and Cimatti, Alessandro and
+ Davenport, James H. and England, Matthew and Fontaine, Pascal
+ and Forrest, Stephen and Ganesh, Vijay and Griggio, Alberto and
+ Kroenig, Daniel and Seiler, Werner M.",
+ title = "SC2 challenges: when Satisfiability Checking and Symbolic
+ Computation join forces",
+ year = "2017",
+ abstract =
+ "Symbolic Computation and Satisfiability Checking are two research
+ areas, both having their individual scientific focus but with common
+ interests, e.g., in the development, implementation and application
+ of decision procedures for arithmetic theories. Despite their
+ commonalities, the two communities are rather weakly connected. The
+ aim of the SC 2 initiative is to strengthen the connection between
+ these communities by creating common platforms, initiating interaction
+ and exchange, identifying common challenges, and developing a common
+ roadmap from theory along the way to tools and (industrial) applications.",
+ paper = "Abraxx.pdf"
+}
+
@book{Acze13,
author = "Aczel, Peter et al.",
title = "Homotopy Type Theory: Univalent Foundations of Mathematics",
publisher = "Institute for Advanced Study",
year = "2013",
- link = "\url{https://hott.github.io/book/nightly/hott-letter-1075-g3c53219.pdf}",
+ link =
+ "\url{https://hott.github.io/book/nightly/hott-letter-1075-g3c53219.pdf}",
paper = "Acze13.pdf"
}
@@ -6762,6 +6869,28 @@ paper = "Brea89.pdf"
paper = "Aker93.pdf"
}
+@article{Avig12a,
+ author = "Avigad, Jeremy",
+ title = "Type Inference in Mathematics",
+ journal = "European Association of Theoretical Computer Science",
+ volume = "106",
+ pages = "78-98",
+ year = "2012",
+ abstract =
+ "In the theory of programming languages, type inference is the process
+ of inferring the type of an expression automatically, often making use
+ of information from the context in which the expression appears. Such
+ mechanisms turn out to be extremely useful in the practice of
+ interactive theorem proving, whereby users interact with a
+ computational proof assistant to construct formal axiomatic
+ derivations of mathematical theorems. This article explains some of
+ the mechanisms for type inference used by the Mathematical
+ Components project, which is working towards a verification of the
+ Feit-Thompson theorem.",
+ paper = "Avig12a.pdf",
+ keywords = "coercion"
+}
+
@misc{Avig14,
author = "Avigad, Jeremy",
title = "LEAN proof of GCD",
@@ -6811,7 +6940,7 @@ paper = "Brea89.pdf"
which enables the communication between both systems illustrated by
some examples that can be solved by theorems and algorithms",
paper = "Ball95.pdf",
- keywords = "CAS-Proof"
+ keywords = "axiomref, CAS-Proof"
}
@@ -8167,6 +8296,19 @@ paper = "Brea89.pdf"
keywords = "axiomref, CAS-Proof"
}
+@misc{Hear12,
+ author = "Hearn, Peter W.O.",
+ title = "A Primer on Separation Logic (and Automatic Program
+ Verification and Analysis",
+ year = "2012",
+ abstract =
+ "These are the notes to accompany a course at the Marktoberdorf PhD
+ summer school in 2011. The course consists of an introduction to
+ separation logic, with a slant towards its use in automatic program
+ verification and analysis.",
+ paper = "Hear12.pdf"
+}
+
@misc{Heer02,
author = "Heeren, Bastiaan and Hage, Jurriaan and Swierstra, Doaitse",
title = "Generalizing Hindley-Milner Type Inference Algorithms",
@@ -9025,6 +9167,32 @@ paper = "Brea89.pdf"
be implemented in functional programming and type theory."
}
+@misc{Mour15,
+ author = "de Moura, Leonardo and Avigad, Jeremy and Kong, Soonho and
+ Roux, Cody",
+ title = "Elaboration in Dependent Type Theory",
+ year = "2015",
+ comment = "arXiv:1505.04324v2",
+ abstract =
+ "To be usable in practice, interactive theorem provers need to provide
+ convenient and efficient means of writing expressions, definitions,
+ and proofs. This involves inferring information that is often left
+ implicit in an ordinary mathematical text, and resolving ambiguities
+ in mathematical expressions. We refer to the process of passing from a
+ quasi-formal and partially- specified expression to a completely
+ precise formal one as {\sl elaboration}. We describe an elaboration
+ algorithms for dependent type theory that has been implemented in the
+ Lean theorem prover. Lean's elaborator supports higher-order
+ unification, type class inference, ad hoc overloading, insertion of
+ coercions, the use of tactics, and the computational reduction of
+ terms. The interactions between these components are subtle and
+ complex, and the elaboration algorithm has been carefully designed to
+ balance efficiency and usability. We describe the central design
+ goals, and the means by which they are achieved.",
+ paper = "Mour15.pdf",
+ keywords = "coercion"
+}
+
@misc{Mour16,
author = "de Moura, Leonardo and Avigad, Jeremy and Kong, Soonho and
Roux, Cody",
@@ -9042,7 +9210,8 @@ paper = "Brea89.pdf"
the computational reduction of terms. The interactions between these
components are subtle and complex, and Lean's elaborator has been
carefully designed to balance efficiency and usability.",
- paper = "Mour16.pdf"
+ paper = "Mour16.pdf",
+ keywords = "coercion"
}
@book{Nipk14,
@@ -9454,6 +9623,49 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@inproceedings{Reyn02,
+ author = "Reynolds, John C.",
+ title = "Separation Logic: A Logic for Shared Mutable Data Structures",
+ booktitle = "Logic in Computer Science '02",
+ year = "2002",
+ pages = "55-74",
+ isbn = "0-7695-1483-9",
+ abstract =
+ "In joint work with Peter O'Hearn and others, based on early ideas of
+ Burstall, we have developed an extension of Hoare logic that permits
+ reasoning about low-level imperativeprograms that use shared mutable
+ data structure.The simple imperative programming language is extended
+ with commands (not expressions) for accessing and modifying shared
+ structures, and for explicit allocation and deallocation of
+ storage. Assertions are extended by introducing a ``separating
+ conjunction'' that asserts that its sub-formulas hold for disjoint
+ parts of the heap, and a closely related ``separating
+ implication''. Coupled with the inductive definition of predicates on
+ abstract data structures, this extension permits the concise and
+ flexible description of structures with controlled sharing.In this
+ paper, we will survey the current development of this program logic,
+ including extensions that permit unrestricted address arithmetic,
+ dynamically allocated arrays, and recursive procedures. We will also
+ discuss promising future directions.",
+ paper = "Reyn02.pdf"
+}
+
+@article{Reyn05,
+ author = "Reynolds, John C.",
+ title = "An Overview of Separation Logic",
+ year = "2005",
+ journal = "LNCS",
+ volume = "4171",
+ pages = "460-469",
+ abstract =
+ "After some general remarks about program verification, we introduce
+ separation logic, a novel extension of Hoare logic that can strengthen
+ the applicability and scalability of program verification for
+ imperative programs that use shared mutable data structures or
+ shared-memory concurrency",
+ paper = "Reyn05.pdf",
+}
+
@misc{Robe15,
author = "Roberts, Siobhan",
title = "In Mathematics, Mistakes Aren't What They Used To Be",
@@ -9619,6 +9831,30 @@ paper = "Brea89.pdf"
paper = "Ther01.pdf"
}
+@article{Tray11,
+ author = "Traytel, Dmitriy and Berghofer, Stefan and Nipkow, Tobias",
+ title = "Extending Hindley-Milner Type Inference with Coercive
+ Structural Subtyping",
+ journal = "LNCS",
+ volume = "7078",
+ pages = "89-104",
+ year = "2011",
+ abstract =
+ "We investigate how to add coercive structural subtyping to a type
+ system for simply-typed lambda calculus with Hindley-Milner
+ polymorphism. Coercions allow to convert between different types, and
+ their automatic insertion can greatly increase readability of
+ terms. We present a type inference algorithm that, given a term
+ without type information, computes a type assignment and determines at
+ which positions in the term coercions have to be inserted to make it
+ type-correct according to the standard Hindley-Milner system (without
+ any subtypes). The algorithm is sound and, if the subtype relation
+ on base types is a disjoint union of lattices, also complete. The
+ algorithm has been implemented in the proof assistant Isabelle.",
+ paper = "Tray11.pdf",
+ keywords = "coercion"
+}
+
@misc{Troe97,
author = "Troelstra, A.S.",
title = "From constructivism to computer science",
@@ -14614,6 +14850,21 @@ paper = "Brea89.pdf"
paper = "Jova12.pdf"
}
+@article{Kaue11,
+ author = "Kauers, Manuel",
+ title = "How to use Cylindrical Algebraic Decomposition",
+ journal = {S\'emminaire Lotharingien de Combinatoire},
+ volume = "65",
+ year = "2011",
+ comment = "Article B65a",
+ abstract =
+ "We take some items from a textbook on inequalities and show how to
+ prove them with computer algebra using the Cylindrical Algebraic
+ Decomposition algorithm. This is an example collection for standard
+ applications of this algorithm, intended as a guide for potential users.",
+ paper = "Kaue11.pdf"
+}
+
@book{LaVa06,
author = "LaValle, Steven M.",
title = "Planning Algorithms",
@@ -28181,7 +28432,7 @@ paper = "Brea89.pdf"
computer algebra whose coercion relations cannot be captured by a
finite set of first-order rewrite rules.",
paper = "Webe05.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, coercion"
}
@InProceedings{Webe94,
@@ -28204,7 +28455,7 @@ paper = "Brea89.pdf"
the corresponding type inference problems were known to be
undecidable.",
paper = "Webe94.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, coercion"
}
@article{Webe95,
@@ -28216,8 +28467,8 @@ paper = "Brea89.pdf"
pages = "25-38",
year = "1995",
link = "\url{http://cg.cs.uni-bonn.de/personal-pages/weber/publications/pdf/WeberA/Weber94e.pdf}",
- abstract = "
- Modern computer algebra systems (e.g. AXIOM) support a rich type
+ abstract =
+ "Modern computer algebra systems (e.g. AXIOM) support a rich type
system including parameterized data types and the possibility of
implicit coercions between types. In such a type system it will be
frequently the case that there are different ways of building
@@ -28228,7 +28479,7 @@ paper = "Brea89.pdf"
examples. Moreover, we will give some informal reasoning why the
formally defined restrictions can be satisfied by an actual system.",
paper = "Webe95.pdf",
- keywords = "axiomref",
+ keywords = "axiomref, coercion",
beebe = "Weber:1993:CCA"
}
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 494fe73..6f873da 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -9204,13 +9204,158 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp1215-1231
\subsection{A} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Ab\'anades, M.}
+\index{Botana, F.}
+\index{Kov\'acs, Z.}
+\index{Recio, T.}
+\index{S\'olyom-Gecse, C.}
+\begin{chunk}{axiom.bib}
+@article{Aban16,
+ author = "Abanades, M. and Botana, F. and Kovacs, Z. and Recio, T. and
+ Solyom-Gecse, C.",
+ title = "Development of automatic reasoning tools in GeoGebra",
+ journal = "ACM Comm. Computer Algebra",
+ volume = "50",
+ pages = "85-88",
+ year = "2016",
+ abstract =
+ "Much effort has been put into the implementation of automatic proving
+ in interactive geometric environments (e.g. Java Geometry Expert,
+ GeoGebra). The closely related concept of automatic discovery, remains
+ however almost unexplored.
+
+ This software presentation will demonstrate our results towards the
+ incorporation of automatic discovery capabilities into GeoGebra, an
+ educational software with tens of millions of users worldwide. As main
+ result, we report on a new command, currently available in the
+ official version, that allows the automatic discovery of loci of
+ points in diagrams defined by implicit conditions. This represents an
+ extension of a previous command, similar in nature, but restricted to
+ loci defined by the standard mover-tracer construction. Our proposal
+ successfully automates the `dummy locus dragging' in dynamic
+ geometry. This makes the cycle conjecturing-checking-proving
+ accessible for general users in elementary geometry.",
+ paper = "Aban16.pdf"
+}
+
+\end{chunk}
+
+\index{Abraham, Erika}
+\begin{chunk}{axiom.bib}
+@inproceedings{Abra15,
+ author = "Abraham, Erika",
+ title = "Building Bridges between Symbolic Computation and Satisfiability
+ Checking",
+ booktitle = "ISSAC 15",
+ year = "2015",
+ pages = "1-6",
+ publisher = "ACM",
+ isbn = "978-1-4503-3435-8",
+ abstract =
+ "The satisfiability problem is the problem of deciding whether a
+ logical formula is satisfiable. For first-order arithmetic theories,
+ in the early 20th century some novel solutions in form of decision
+ procedures were developed in the area of mathematical logic. With the
+ advent of powerful computer architectures, a new research line started
+ to develop practically feasible implementations of such decision
+ procedures. Since then, symbolic computation has grown to an extremely
+ successful scientific area, supporting all kinds of scientific
+ computing by efficient computer algebra systems.
+
+ Independently, around 1960 a new technology called SAT solving started
+ its career. Restricted to propositional logic, SAT solvers showed to
+ be very efficient when employed by formal methods for verification. It
+ did not take long till the power of SAT solving for Boolean problems
+ had been extended to cover also different theories. Nowadays, fast
+ SAT-modulo-theories (SMT) solvers are available also for arithmetic
+ problems.
+
+ Due to their different roots, symbolic computation and SMT solving
+ tackle the satisfiability problem differently. We discuss differences
+ and similarities in their approaches, highlight potentials of
+ combining their strengths, and discuss the challenges that come with
+ this task.",
+ paper = "Abra15.pdf"
+}
+
+\end{chunk}
+
+\index{Abraham, Erika}
+\begin{chunk}{axiom.bib}
+@inproceedings{Abra16,
+ author = "Abraham, Erika",
+ title = "Symbolic Computation Techniques in Satisfiability Checking",
+ booktitle = "SYNASC 2016",
+ publisher = "IEEE Press",
+ year = "2016",
+ isbn = "978-1-5090-5707-8",
+ pages = "3-10"
+}
+
+\end{chunk}
+
+\index{Abraham, Erika}
+\index{Jebelean, Tudor}
+\begin{chunk}{axiom.bib}
+@inproceedings{Abra17,
+ author = "Abraham, Erika and Jebelean, Tudor",
+ title = "Adapting Cylindrical Algebraic Decomposition for Proof Specific
+ Tasks",
+ booktitle = "IJCAI 2017",
+ year = "2017",
+ comment = "Extended Abstract",
+ paper = "Abra17.pdf"
+}
+
+\end{chunk}
+
+\index{Abraham, Erika}
+\index{Abbott, John}
+\index{Becker, Bernd}
+\index{Bigatti, Anna M.}
+\index{Brain, Martin}
+\index{Cimatti, Alessandro}
+\index{Davenport, James H.}
+\index{England, Matthew}
+\index{Fontaine, Pascal}
+\index{Forrest, Stephen}
+\index{Ganesh, Vijay}
+\index{Griggio, Alberto}
+\index{Kroenig, Daniel}
+\index{Seiler, Werner M.}
+\begin{chunk}{axiom.bib}
+@misc{Abraxx,
+ author = "Abraham, Erika and Abbott, John and Becker, Bernd and
+ Bigatti, Anna M. and Brain, Martin and Cimatti, Alessandro and
+ Davenport, James H. and England, Matthew and Fontaine, Pascal
+ and Forrest, Stephen and Ganesh, Vijay and Griggio, Alberto and
+ Kroenig, Daniel and Seiler, Werner M.",
+ title = "SC2 challenges: when Satisfiability Checking and Symbolic
+ Computation join forces",
+ year = "2017",
+ abstract =
+ "Symbolic Computation and Satisfiability Checking are two research
+ areas, both having their individual scientific focus but with common
+ interests, e.g., in the development, implementation and application
+ of decision procedures for arithmetic theories. Despite their
+ commonalities, the two communities are rather weakly connected. The
+ aim of the SC 2 initiative is to strengthen the connection between
+ these communities by creating common platforms, initiating interaction
+ and exchange, identifying common challenges, and developing a common
+ roadmap from theory along the way to tools and (industrial) applications.",
+ paper = "Abraxx.pdf"
+}
+
+\end{chunk}
+
\begin{chunk}{axiom.bib}
@book{Acze13,
author = "Aczel, Peter et al.",
title = "Homotopy Type Theory: Univalent Foundations of Mathematics",
publisher = "Institute for Advanced Study",
year = "2013",
- link = "\url{https://hott.github.io/book/nightly/hott-letter-1075-g3c53219.pdf}",
+ link =
+ "\url{https://hott.github.io/book/nightly/hott-letter-1075-g3c53219.pdf}",
paper = "Acze13.pdf"
}
@@ -9361,6 +9506,32 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp1215-1231
\index{Avigad, Jeremy}
\begin{chunk}{axiom.bib}
+@article{Avig12a,
+ author = "Avigad, Jeremy",
+ title = "Type Inference in Mathematics",
+ journal = "European Association of Theoretical Computer Science",
+ volume = "106",
+ pages = "78-98",
+ year = "2012",
+ abstract =
+ "In the theory of programming languages, type inference is the process
+ of inferring the type of an expression automatically, often making use
+ of information from the context in which the expression appears. Such
+ mechanisms turn out to be extremely useful in the practice of
+ interactive theorem proving, whereby users interact with a
+ computational proof assistant to construct formal axiomatic
+ derivations of mathematical theorems. This article explains some of
+ the mechanisms for type inference used by the Mathematical
+ Components project, which is working towards a verification of the
+ Feit-Thompson theorem.",
+ paper = "Avig12a.pdf",
+ keywords = "coercion"
+}
+
+\end{chunk}
+
+\index{Avigad, Jeremy}
+\begin{chunk}{axiom.bib}
@misc{Avig14,
author = "Avigad, Jeremy",
title = "LEAN proof of GCD",
@@ -9428,7 +9599,7 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp1215-1231
which enables the communication between both systems illustrated by
some examples that can be solved by theorems and algorithms",
paper = "Ball95.pdf",
- keywords = "CAS-Proof"
+ keywords = "axiomref, CAS-Proof"
}
@@ -11228,6 +11399,23 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{Hearn, Peter W.O.}
+\begin{chunk}{axiom.bib}
+@misc{Hear12,
+ author = "Hearn, Peter W.O.",
+ title = "A Primer on Separation Logic (and Automatic Program
+ Verification and Analysis",
+ year = "2012",
+ abstract =
+ "These are the notes to accompany a course at the Marktoberdorf PhD
+ summer school in 2011. The course consists of an introduction to
+ separation logic, with a slant towards its use in automatic program
+ verification and analysis.",
+ paper = "Hear12.pdf"
+}
+
+\end{chunk}
+
\index{Heeren, Bastiaan}
\index{Hage, Jurriaan},
\index{Swierstra, Doaitse}
@@ -11487,6 +11675,27 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{Kaliszyk, Cezary}
+\begin{chunk}{axiom.bib}
+@phdthesis{Kali09,
+ author = "Kaliszyk, Cezary"
+ title = "Correctness and Availability: Building Computer Algebra on top
+ of Proof Assistants and making Proof Assistants available over
+ the Web",
+ year = "2009",
+ school = "Radboud University, Nijmegen",
+ link = "\url{http://cl-informatik.uibk.ac.at/users/cek/docs/09/kaliszyk\_thesis\_webdoc.pdf}",
+ abstract =
+ "In this thesis we present an approach to extending the usability
+ of proof assistants in mathematics and computer science. We do it
+ in two ways: by combining proof assistants with computer algebra
+ systems and by providing interactive access to such systems on
+ the web.",
+ paper = "Kali09.pdf"
+}
+
+\end{chunk}
+
\index{Kaufmann, Matt}
\index{Moore, J Strother}
\begin{chunk}{axiom.bib}
@@ -12300,6 +12509,39 @@ England, Matthew; Wilson, David
\index{Kong, Soonho}
\index{Roux, Cody}
\begin{chunk}{axiom.bib}
+@misc{Mour15,
+ author = "de Moura, Leonardo and Avigad, Jeremy and Kong, Soonho and
+ Roux, Cody",
+ title = "Elaboration in Dependent Type Theory",
+ year = "2015",
+ comment = "arXiv:1505.04324v2",
+ abstract =
+ "To be usable in practice, interactive theorem provers need to provide
+ convenient and efficient means of writing expressions, definitions,
+ and proofs. This involves inferring information that is often left
+ implicit in an ordinary mathematical text, and resolving ambiguities
+ in mathematical expressions. We refer to the process of passing from a
+ quasi-formal and partially- specified expression to a completely
+ precise formal one as {\sl elaboration}. We describe an elaboration
+ algorithms for dependent type theory that has been implemented in the
+ Lean theorem prover. Lean's elaborator supports higher-order
+ unification, type class inference, ad hoc overloading, insertion of
+ coercions, the use of tactics, and the computational reduction of
+ terms. The interactions between these components are subtle and
+ complex, and the elaboration algorithm has been carefully designed to
+ balance efficiency and usability. We describe the central design
+ goals, and the means by which they are achieved.",
+ paper = "Mour15.pdf",
+ keywords = "coercion"
+}
+
+\end{chunk}
+
+\index{de Moura, Leonardo}
+\index{Avigad, Jeremy}
+\index{Kong, Soonho}
+\index{Roux, Cody}
+\begin{chunk}{axiom.bib}
@misc{Mour16,
author = "de Moura, Leonardo and Avigad, Jeremy and Kong, Soonho and
Roux, Cody",
@@ -12317,7 +12559,8 @@ England, Matthew; Wilson, David
the computational reduction of terms. The interactions between these
components are subtle and complex, and Lean's elaborator has been
carefully designed to balance efficiency and usability.",
- paper = "Mour16.pdf"
+ paper = "Mour16.pdf",
+ keywords = "coercion"
}
\end{chunk}
@@ -12893,6 +13136,57 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
+\index{Reynolds, John C.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Reyn02,
+ author = "Reynolds, John C.",
+ title = "Separation Logic: A Logic for Shared Mutable Data Structures",
+ booktitle = "Logic in Computer Science '02",
+ year = "2002",
+ pages = "55-74",
+ isbn = "0-7695-1483-9",
+ abstract =
+ "In joint work with Peter O'Hearn and others, based on early ideas of
+ Burstall, we have developed an extension of Hoare logic that permits
+ reasoning about low-level imperativeprograms that use shared mutable
+ data structure.The simple imperative programming language is extended
+ with commands (not expressions) for accessing and modifying shared
+ structures, and for explicit allocation and deallocation of
+ storage. Assertions are extended by introducing a ``separating
+ conjunction'' that asserts that its sub-formulas hold for disjoint
+ parts of the heap, and a closely related ``separating
+ implication''. Coupled with the inductive definition of predicates on
+ abstract data structures, this extension permits the concise and
+ flexible description of structures with controlled sharing.In this
+ paper, we will survey the current development of this program logic,
+ including extensions that permit unrestricted address arithmetic,
+ dynamically allocated arrays, and recursive procedures. We will also
+ discuss promising future directions.",
+ paper = "Reyn02.pdf"
+}
+
+\end{chunk}
+
+\index{Reynolds, John C.}
+\begin{chunk}{axiom.bib}
+@article{Reyn05,
+ author = "Reynolds, John C.",
+ title = "An Overview of Separation Logic",
+ year = "2005",
+ journal = "LNCS",
+ volume = "4171",
+ pages = "460-469",
+ abstract =
+ "After some general remarks about program verification, we introduce
+ separation logic, a novel extension of Hoare logic that can strengthen
+ the applicability and scalability of program verification for
+ imperative programs that use shared mutable data structures or
+ shared-memory concurrency",
+ paper = "Reyn05.pdf",
+}
+
+\end{chunk}
+
\index{Roberts, Siobhan}
\begin{chunk}{axiom.bib}
@misc{Robe15,
@@ -13105,6 +13399,36 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
+\index{Traytel, Dmitriy}
+\index{Berghofer, Stefan}
+\index{Nipkow, Tobias}
+\begin{chunk}{axiom.bib}
+@article{Tray11,
+ author = "Traytel, Dmitriy and Berghofer, Stefan and Nipkow, Tobias",
+ title = "Extending Hindley-Milner Type Inference with Coercive
+ Structural Subtyping",
+ journal = "LNCS",
+ volume = "7078",
+ pages = "89-104",
+ year = "2011",
+ abstract =
+ "We investigate how to add coercive structural subtyping to a type
+ system for simply-typed lambda calculus with Hindley-Milner
+ polymorphism. Coercions allow to convert between different types, and
+ their automatic insertion can greatly increase readability of
+ terms. We present a type inference algorithm that, given a term
+ without type information, computes a type assignment and determines at
+ which positions in the term coercions have to be inserted to make it
+ type-correct according to the standard Hindley-Milner system (without
+ any subtypes). The algorithm is sound and, if the subtype relation
+ on base types is a disjoint union of lattices, also complete. The
+ algorithm has been implemented in the proof assistant Isabelle.",
+ paper = "Tray11.pdf",
+ keywords = "coercion"
+}
+
+\end{chunk}
+
\index{Troelstra, A.S.}
\begin{chunk}{axiom.bib}
@misc{Troe97,
@@ -20793,6 +21117,28 @@ Proc ISSAC 97 pp172-175 (1997)
\end{chunk}
+\subsection{K} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\index{Kauers, Manuel}
+\begin{chunk}{axiom.bib}
+@article{Kaue11,
+ author = "Kauers, Manuel",
+ title = "How to use Cylindrical Algebraic Decomposition",
+ journal = {S\'emminaire Lotharingien de Combinatoire},
+ volume = "65",
+ year = "2011",
+ comment = "Article B65a",
+ abstract =
+ "We take some items from a textbook on inequalities and show how to
+ prove them with computer algebra using the Cylindrical Algebraic
+ Decomposition algorithm. This is an example collection for standard
+ applications of this algorithm, intended as a guide for potential users.",
+ paper = "Kaue11.pdf"
+}
+
+\end{chunk}
+
+
\subsection{L} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{LaValle, Steven M.}
@@ -42180,7 +42526,7 @@ IBM T. J. Watson Research Center (2001)
computer algebra whose coercion relations cannot be captured by a
finite set of first-order rewrite rules.",
paper = "Webe05.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, coercion"
}
\end{chunk}
@@ -42232,7 +42578,7 @@ IBM T. J. Watson Research Center (2001)
the corresponding type inference problems were known to be
undecidable.",
paper = "Webe94.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, coercion"
}
\end{chunk}
@@ -42248,8 +42594,8 @@ IBM T. J. Watson Research Center (2001)
pages = "25-38",
year = "1995",
link = "\url{http://cg.cs.uni-bonn.de/personal-pages/weber/publications/pdf/WeberA/Weber94e.pdf}",
- abstract = "
- Modern computer algebra systems (e.g. AXIOM) support a rich type
+ abstract =
+ "Modern computer algebra systems (e.g. AXIOM) support a rich type
system including parameterized data types and the possibility of
implicit coercions between types. In such a type system it will be
frequently the case that there are different ways of building
@@ -42260,7 +42606,7 @@ IBM T. J. Watson Research Center (2001)
examples. Moreover, we will give some informal reasoning why the
formally defined restrictions can be satisfied by an actual system.",
paper = "Webe95.pdf",
- keywords = "axiomref",
+ keywords = "axiomref, coercion",
beebe = "Weber:1993:CCA"
}
diff --git a/changelog b/changelog
index a27aaad..506aabf 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20170924 tpd src/axiom-website/patches.html 20170924.01.tpd.patch
+20170924 tpd books/bookvolbib add references
20170907 tpd src/axiom-website/patches.html 20170907.01.tpd.patch
20170907 tpd books/bookvol5 update credits list
20170907 tpd books/bookvol10.4 update credits list
diff --git a/patch b/patch
index f08820a..7721955 100644
--- a/patch
+++ b/patch
@@ -1,3 +1,341 @@
-books/bookheader.tex add Jerry Archibald, Philip Santas, David Saunders
+books/bookvolbib add Coercion references
-Goal: Axiom Maintenance
+Goal: Proving Axiom Correct
+
+\index{Traytel, Dmitriy}
+\index{Berghofer, Stefan}
+\index{Nipkow, Tobias}
+\begin{chunk}{axiom.bib}
+@article{Tray11,
+ author = "Traytel, Dmitriy and Berghofer, Stefan and Nipkow, Tobias",
+ title = "Extending Hindley-Milner Type Inference with Coercive
+ Structural Subtyping",
+ journal = "LNCS",
+ volume = "7078",
+ pages = "89-104",
+ year = "2011",
+ abstract =
+ "We investigate how to add coercive structural subtyping to a type
+ system for simply-typed lambda calculus with Hindley-Milner
+ polymorphism. Coercions allow to convert between different types, and
+ their automatic insertion can greatly increase readability of
+ terms. We present a type inference algorithm that, given a term
+ without type information, computes a type assignment and determines at
+ which positions in the term coercions have to be inserted to make it
+ type-correct according to the standard Hindley-Milner system (without
+ any subtypes). The algorithm is sound and, if the subtype relation
+ on base types is a disjoint union of lattices, also complete. The
+ algorithm has been implemented in the proof assistant Isabelle.",
+ paper = "Tray11.pdf",
+ keywords = "coercion"
+}
+
+\end{chunk}
+
+\index{Ab\'anades, M.}
+\index{Botana, F.}
+\index{Kov\'acs, Z.}
+\index{Recio, T.}
+\index{S\'olyom-Gecse, C.}
+\begin{chunk}{axiom.bib}
+@article{Aban16,
+ author = "Abanades, M. and Botana, F. and Kovacs, Z. and Recio, T. and
+ Solyom-Gecse, C.",
+ title = "Development of automatic reasoning tools in GeoGebra",
+ journal = "ACM Comm. Computer Algebra",
+ volume = "50",
+ pages = "85-88",
+ year = "2016",
+ abstract =
+ "Much effort has been put into the implementation of automatic proving
+ in interactive geometric environments (e.g. Java Geometry Expert,
+ GeoGebra). The closely related concept of automatic discovery, remains
+ however almost unexplored.
+
+ This software presentation will demonstrate our results towards the
+ incorporation of automatic discovery capabilities into GeoGebra, an
+ educational software with tens of millions of users worldwide. As main
+ result, we report on a new command, currently available in the
+ official version, that allows the automatic discovery of loci of
+ points in diagrams defined by implicit conditions. This represents an
+ extension of a previous command, similar in nature, but restricted to
+ loci defined by the standard mover-tracer construction. Our proposal
+ successfully automates the `dummy locus dragging' in dynamic
+ geometry. This makes the cycle conjecturing-checking-proving
+ accessible for general users in elementary geometry.",
+ paper = "Aban16.pdf"
+}
+
+\end{chunk}
+
+\index{Avigad, Jeremy}
+\begin{chunk}{axiom.bib}
+@article{Avig12a,
+ author = "Avigad, Jeremy",
+ title = "Type Inference in Mathematics",
+ journal = "European Association of Theoretical Computer Science",
+ volume = "106",
+ pages = "78-98",
+ year = "2012",
+ abstract =
+ "In the theory of programming languages, type inference is the process
+ of inferring the type of an expression automatically, often making use
+ of information from the context in which the expression appears. Such
+ mechanisms turn out to be extremely useful in the practice of
+ interactive theorem proving, whereby users interact with a
+ computational proof assistant to construct formal axiomatic
+ derivations of mathematical theorems. This article explains some of
+ the mechanisms for type inference used by the Mathematical
+ Components project, which is working towards a verification of the
+ Feit-Thompson theorem.",
+ paper = "Avig12a.pdf",
+ keywords = "coercion"
+}
+
+\end{chunk}
+
+\index{Abraham, Erika}
+@inproceedings{Abra15,
+ author = "Abraham, Erika",
+ title = "Building Bridges between Symbolic Computation and Satisfiability
+ Checking",
+ booktitle = "ISSAC 15",
+ year = "2015",
+ pages = "1-6",
+ publisher = "ACM",
+ isbn = "978-1-4503-3435-8",
+ abstract =
+ "The satisfiability problem is the problem of deciding whether a
+ logical formula is satisfiable. For first-order arithmetic theories,
+ in the early 20th century some novel solutions in form of decision
+ procedures were developed in the area of mathematical logic. With the
+ advent of powerful computer architectures, a new research line started
+ to develop practically feasible implementations of such decision
+ procedures. Since then, symbolic computation has grown to an extremely
+ successful scientific area, supporting all kinds of scientific
+ computing by efficient computer algebra systems.
+
+ Independently, around 1960 a new technology called SAT solving started
+ its career. Restricted to propositional logic, SAT solvers showed to
+ be very efficient when employed by formal methods for verification. It
+ did not take long till the power of SAT solving for Boolean problems
+ had been extended to cover also different theories. Nowadays, fast
+ SAT-modulo-theories (SMT) solvers are available also for arithmetic
+ problems.
+
+ Due to their different roots, symbolic computation and SMT solving
+ tackle the satisfiability problem differently. We discuss differences
+ and similarities in their approaches, highlight potentials of
+ combining their strengths, and discuss the challenges that come with
+ this task.",
+ paper = "Abra15.pdf"
+}
+
+\end{chunk}
+
+\index{Abraham, Erika}
+\begin{chunk}{axiom.bib}
+@inproceedings{Abra16,
+ author = "Abraham, Erika",
+ title = "Symbolic Computation Techniques in Satisfiability Checking",
+ booktitle = "SYNASC 2016",
+ publisher = "IEEE Press",
+ year = "2016",
+ isbn = "978-1-5090-5707-8",
+ pages = "3-10"
+}
+
+\end{chunk}
+
+\index{Kauers, Manuel}
+\begin{chunk}{axiom.bib}
+@article{Kaue11,
+ author = "Kauers, Manuel",
+ title = "How to use Cylindrical Algebraic Decomposition",
+ journal = {S\'emminaire Lotharingien de Combinatoire},
+ volume = "65",
+ year = "2011",
+ comment = "Article B65a",
+ abstract =
+ "We take some items from a textbook on inequalities and show how to
+ prove them with computer algebra using the Cylindrical Algebraic
+ Decomposition algorithm. This is an example collection for standard
+ applications of this algorithm, intended as a guide for potential users.",
+ paper = "Kaue11.pdf"
+}
+
+\end{chunk}
+
+\index{Abraham, Erika}
+\index{Jebelean, Tudor}
+\begin{chunk}{axiom.bib}
+@inproceedings{Abra17,
+ author = "Abraham, Erika and Jebelean, Tudor",
+ title = "Adapting Cylindrical Algebraic Decomposition for Proof Specific
+ Tasks",
+ booktitle = "IJCAI 2017",
+ year = "2017",
+ comment = "Extended Abstract",
+ paper = "Abra17.pdf"
+}
+
+\end{chunk}
+
+\index{Abraham, Erika}
+\index{Abbott, John}
+\index{Becker, Bernd}
+\index{Bigatti, Anna M.}
+\index{Brain, Martin}
+\index{Cimatti, Alessandro}
+\index{Davenport, James H.}
+\index{England, Matthew}
+\index{Fontaine, Pascal}
+\index{Forrest, Stephen}
+\index{Ganesh, Vijay}
+\index{Griggio, Alberto}
+\index{Kroenig, Daniel}
+\index{Seiler, Werner M.}
+\begin{chunk}{axiom.bib}
+@misc{Abraxx,
+ author = "Abraham, Erika and Abbott, John and Becker, Bernd and
+ Bigatti, Anna M. and Brain, Martin and Cimatti, Alessandro and
+ Davenport, James H. and England, Matthew and Fontaine, Pascal
+ and Forrest, Stephen and Ganesh, Vijay and Griggio, Alberto and
+ Kroenig, Daniel and Seiler, Werner M.",
+ title = "SC2 challenges: when Satisfiability Checking and Symbolic
+ Computation join forces",
+ year = "2017",
+ abstract =
+ "Symbolic Computation and Satisfiability Checking are two research
+ areas, both having their individual scientific focus but with common
+ interests, e.g., in the development, implementation and application
+ of decision procedures for arithmetic theories. Despite their
+ commonalities, the two communities are rather weakly connected. The
+ aim of the SC 2 initiative is to strengthen the connection between
+ these communities by creating common platforms, initiating interaction
+ and exchange, identifying common challenges, and developing a common
+ roadmap from theory along the way to tools and (industrial) applications.",
+ paper = "Abraxx.pdf"
+}
+
+\end{chunk}
+
+\index{de Moura, Leonardo}
+\index{Avigad, Jeremy}
+\index{Kong, Soonho}
+\index{Roux, Cody}
+\begin{chunk}{axiom.bib}
+@misc{Mour15,
+ author = "de Moura, Leonardo and Avigad, Jeremy and Kong, Soonho and
+ Roux, Cody",
+ title = "Elaboration in Dependent Type Theory",
+ year = "2015",
+ abstract =
+ "To be usable in practice, interactive theorem provers need to provide
+ convenient and efficient means of writing expressions, definitions,
+ and proofs. This involves inferring information that is often left
+ implicit in an ordinary mathematical text, and resolving ambiguities
+ in mathematical expressions. We refer to the process of passing from a
+ quasi-formal and partially- specified expression to a completely
+ precise formal one as {\sl elaboration}. We describe an elaboration
+ algorithms for dependent type theory that has been implemented in the
+ Lean theorem prover. Lean's elaborator supports higher-order
+ unification, type class inference, ad hoc overloading, insertion of
+ coercions, the use of tactics, and the computational reduction of
+ terms. The interactions between these components are subtle and
+ complex, and the elaboration algorithm has been carefully designed to
+ balance efficiency and usability. We describe the central design
+ goals, and the means by which they are achieved.",
+ paper = "Mour15.pdf",
+ keywords = "coercion"
+}
+
+\end{chunk}
+
+\index{Reynolds, John C.}
+\begin{chunk}{axiom.bib}
+@article{Reyn05,
+ author = "Reynolds, John C.",
+ title = "An Overview of Separation Logic",
+ journal = "LNCS",
+ volume = "4171",
+ pages = "460-469",
+ abstract =
+ "After some general remarks about program verification, we introduce
+ separation logic, a novel extension of Hoare logic that can strengthen
+ the applicability and scalability of program verification for
+ imperative programs that use shared mutable data structures or
+ shared-memory concurrency",
+ paper = "Reyn05.pdf",
+}
+
+\end{chunk}
+
+\index{Reynolds, John C.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Reyn02,
+ author = "Reynolds, John C.",
+ title = "Separation Logic: A Logic for Shared Mutable Data Structures",
+ booktitle = "Logic in Computer Science '02",
+ year = "2002",
+ pages = "55-74",
+ isbn = "0-7695-1483-9",
+ abstract =
+ "In joint work with Peter O'Hearn and others, based on early ideas of
+ Burstall, we have developed an extension of Hoare logic that permits
+ reasoning about low-level imperativeprograms that use shared mutable
+ data structure.The simple imperative programming language is extended
+ with commands (not expressions) for accessing and modifying shared
+ structures, and for explicit allocation and deallocation of
+ storage. Assertions are extended by introducing a "separating
+ conjunction" that asserts that its sub-formulas hold for disjoint
+ parts of the heap, and a closely related "separating
+ implication". Coupled with the inductive definition of predicates on
+ abstract data structures, this extension permits the concise and
+ flexible description of structures with controlled sharing.In this
+ paper, we will survey the current development of this program logic,
+ including extensions that permit unrestricted address arithmetic,
+ dynamically allocated arrays, and recursive procedures. We will also
+ discuss promising future directions.",
+ paper = "Reyn02.pdf"
+}
+
+\end{chunk}
+
+\index{Hearn, Peter W.O.}
+\begin{chunk}{axiom.bib}
+@misc{Hear12,
+ author = "Hearn, Peter W.O.",
+ title = "A Primer on Separation Logic (and Automatic Program
+ Verification and Analysis",
+ year = "2012",
+ abstract =
+ "These are the notes to accompany a course at the Marktoberdorf PhD
+ summer school in 2011. The course consists of an introduction to
+ separation logic, with a slant towards its use in automatic program
+ verification and analysis.",
+ paper = "Hear12.pdf"
+}
+
+\end{chunk}
+
+\index{Kaliszyk, Cezary}
+\begin{chunk}{axiom.bib}
+@phdthesis{Kali09,
+ author = "Kaliszyk, Cezary"
+ title = "Correctness and Availability: Building Computer Algebra on top
+ of Proof Assistants and making Proof Assistants available over
+ the Web",
+ year = "2009",
+ school = "Radboud University, Nijmegen",
+ link = "\url{http://cl-informatik.uibk.ac.at/users/cek/docs/09/kaliszyk\_thesis\_webdoc.pdf}",
+ abstract =
+ "In this thesis we present an approach to extending the usability
+ of proof assistants in mathematics and computer science. We do it
+ in two ways: by combining proof assistants with computer algebra
+ systems and by providing interactive access to such systems on
+ the web.",
+ paper = "Kali09.pdf"
+}
+
+\end{chunk}
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 6517fbc..4f4fc89 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5822,6 +5822,8 @@ src/axiom-website/documentation.html add Caviness quote

books/bookvol3 Additional explanations and references

20170907.01.tpd.patch
add Jerry Archibald, Philip Santas, David Saunders

+20170924.01.tpd.patch
+books/bookvolbib add references

--
1.9.1