From 7159c841117cb6c3baa44582f886a48c5af8c686 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Mon, 9 Oct 2017 18:32:03 -0400
Subject: [PATCH] books/bookvolbib add references
Goal: Proving Axiom Correct
\index{Sturm, T.}
\begin{chunk}{axiom.bib}
@techreport{Stur95,
author = "Sturm, T.",
title = "A REDUCE package for first-order logic",
type = "technical report",
institution = "Universitat Passau",
year = "1995",
}
\end{chunk}
\index{Crole, R.L.}
\begin{chunk}{axiom.bib}
@book{Crol93,
author = "Crole, R.L.",
title = "Categories for Types",
publisher = "Cambridge University Press",
year = "1993",
isbn = "978-0521457019"
}
\end{chunk}
\index{Mendelson, Elliot}
\begin{chunk}{axiom.bib}
@book{Mend87,
author = "Mendelson, Elliot",
title = "Introduction to Mathematical Logic",
publisher = "Wadsworth and Brooks/Cole",
year = "1987",
isbn = "978-1482237726"
}
\end{chunk}
\index{Devlin, Keith J.}
\begin{chunk}{axiom.bib}
@book{Devl79,
author = "Devlin, Keith J.",
title = "Fundamentals of Contemporary Set Theory",
publisher = "Springer-Verlag",
year = "1979",
isbn = "978-0387904412"
}
\end{chunk}
\index{Davenport, James H.}
\begin{chunk}{axiom.bib}
@misc{Dave93a,
author = "Davenport, James H.",
title = "C9: Universal Algebra",
year = "1993",
comment = "Lecture Notes for 2nd year undergrad and mather's course
in Universal Algebra",
school = "University of Bath"
}
\end{chunk}
\index{Goguen, J.A.}
\index{Meseguer, J.}
\begin{chunk}{axiom.bib}
@article{Gogu82,
author = "Goguen, J.A. and Meseguer, J.",
title = "Completeness of Many-sorted Equational Logic",
journal = "ACM SIGPLAN Notices",
volume = "17",
number = "1",
year = "1982",
pages = "9-17",
abstract =
"The rules of deduction which are usually used for many-sorted
equational logic in computer science, for example in the study of
abstract data types, are not sound. Correcting these rules by
introducing explicit quantifiers yields a system which, although it is
sound, is not complete; some new rules are needed for the addition and
deletion of quantifiers. This note is intended as an informal, but
precise, introduction to the main issues and results. It gives an
example showing the unsoundness of the usual rules; it also gives a
completeness theorem for our new rules, and gives necessary and
sufficient conditions for the old rules to agree with the new.",
paper = "Gogu82.pdf",
}
\end{chunk}
\index{Padawitz, Peter}
\begin{chunk}{axiom.bib}
@article{Pada80,
author = "Padawitz, Peter",
title = "New results on completeness and consistency of abstract data
types",
journal = "LNCS",
volume = "88",
pages = "460-473",
year = "1980",
abstract =
"If an algebraic specification is designed in a structured way, a
small specification is stepwise enriched by more complex operations
and their defining equations. Based on normalization properties of
term reductions we present sufficient ``local'' conditions for the
completeness and consistency of enrichment steps, which can be
efficiently verified in many cases where other attempts to prove the
enrichment property ``syntactically'' have failed so far."
}
\end{chunk}
\index{Kounalis, Emmanuel}
\index{Rusinowitch, Michael}
\begin{chunk}{axiom.bib}
@inproceedings{Koun90,
author = "Kounalis, Emmanuel and Rusinowitch, Michael",
title = "A Proof System for Conditional Algebraic Specifications",
booktitle = "Conference Conditional and Typed Rewriting Systems",
year = "1990",
abstract =
"Algebraic specifications provide a formal basis for designing
data-structures and reasoning about their properties.
Sufficient-completeness and consistency are fundamental
notions for building algebraic specifications in a modular way. We
give in this paper effective methods for testing these properties for
specifications with conditional axioms."
}
\end{chunk}
---
books/axiom.bib | 102 ++++++++++++++++++++++++-
books/bookvolbib.pamphlet | 136 ++++++++++++++++++++++++++++++++-
changelog | 2 +
patch | 168 +++++++++++++++++++++++++++--------------
src/axiom-website/patches.html | 2 +
5 files changed, 348 insertions(+), 62 deletions(-)
diff --git a/books/axiom.bib b/books/axiom.bib
index 52ddaf2..d954b86 100644
--- a/books/axiom.bib
+++ b/books/axiom.bib
@@ -7197,7 +7197,8 @@ paper = "Brea89.pdf"
components from their specifications, and thus covers the whole
software development process from the specification of requirements to
the finished system. These methos are potentially applicable to the
- development of correct hardware systems as well"
+ development of correct hardware systems as well",
+ keywords = "axiomref, CAS-Proof"
}
@@ -7747,6 +7748,14 @@ paper = "Brea89.pdf"
keywords = "axiomref, CAS-Proof"
}
+@book{Crol93,
+ author = "Crole, R.L.",
+ title = "Categories for Types",
+ publisher = "Cambridge University Press",
+ year = "1993",
+ isbn = "978-0521457019"
+}
+
@InProceedings{Dani06,
author = "Danielsson, Nils Anders and Hughes, John and Jansson, Patrik and
Gibbons, Jeremy",
@@ -7777,6 +7786,15 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@misc{Dave93a,
+ author = "Davenport, James H.",
+ title = "C9: Universal Algebra",
+ year = "1993",
+ comment = "Lecture Notes for 2nd year undergrad and mather's course
+ in Universal Algebra",
+ school = "University of Bath"
+}
+
@article{Dave08,
author = "Davenport, James H.",
title = "Effective Set Membership in Computer Algebra and Beyond",
@@ -7835,6 +7853,14 @@ paper = "Brea89.pdf"
paper = "Dimi79.pdf"
}
+@book{Devl79,
+ author = "Devlin, Keith J.",
+ title = "Fundamentals of Contemporary Set Theory",
+ publisher = "Springer-Verlag",
+ year = "1979",
+ isbn = "978-0387904412"
+}
+
@inproceedings{Dybj90,
author = "Dybjer, Peter",
title = {Inductive Sets and Families in Marin-L\"of's Type Theory and
@@ -8180,6 +8206,28 @@ paper = "Brea89.pdf"
paper = "Gime16.pdf"
}
+@article{Gogu82,
+ author = "Goguen, J.A. and Meseguer, J.",
+ title = "Completeness of Many-sorted Equational Logic",
+ journal = "ACM SIGPLAN Notices",
+ volume = "17",
+ number = "1",
+ year = "1982",
+ pages = "9-17",
+ abstract =
+ "The rules of deduction which are usually used for many-sorted
+ equational logic in computer science, for example in the study of
+ abstract data types, are not sound. Correcting these rules by
+ introducing explicit quantifiers yields a system which, although it is
+ sound, is not complete; some new rules are needed for the addition and
+ deletion of quantifiers. This note is intended as an informal, but
+ precise, introduction to the main issues and results. It gives an
+ example showing the unsoundness of the usual rules; it also gives a
+ completeness theorem for our new rules, and gives necessary and
+ sufficient conditions for the old rules to agree with the new.",
+ paper = "Gogu82.pdf",
+}
+
@misc{Gord96,
author = "Gordon, Mike",
title = "From LCF to HOL: a short history",
@@ -8665,6 +8713,20 @@ paper = "Brea89.pdf"
keywords = "CAS-Proof"
}
+@inproceedings{Koun90,
+ author = "Kounalis, Emmanuel and Rusinowitch, Michael",
+ title = "A Proof System for Conditional Algebraic Specifications",
+ booktitle = "Conference Conditional and Typed Rewriting Systems",
+ year = "1990",
+ abstract =
+ "Algebraic specifications provide a formal basis for designing
+ data-structures and reasoning about their properties.
+ Sufficient-completeness and consistency are fundamental
+ notions for building algebraic specifications in a modular way. We
+ give in this paper effective methods for testing these properties for
+ specifications with conditional axioms."
+}
+
@phdthesis{Kreb15,
author = "Krebbers, Robbert Jan",
title = "The C standard formalized in Coq",
@@ -8937,7 +8999,8 @@ paper = "Brea89.pdf"
automated theorem provers and discuss possible advantages and
disadvantages of these approaches. We also discuss some possible case
studies.",
- paper = "Mart97.ps"
+ paper = "Mart97.ps",
+ keywords = "axiomref, CAS-Proof"
}
@book{Maso86,
@@ -9029,6 +9092,14 @@ paper = "Brea89.pdf"
paper = "Melq12.pdf"
}
+@book{Mend87,
+ author = "Mendelson, Elliot",
+ title = "Introduction to Mathematical Logic",
+ publisher = "Wadsworth and Brooks/Cole",
+ year = "1987",
+ isbn = "978-1482237726"
+}
+
@inproceedings{Mesh01,
author = "Meshveliani, Sergei D.",
title = "Computer Algebra with Haskell: Applying
@@ -9352,6 +9423,24 @@ paper = "Brea89.pdf"
paper = "Nguy16.pdf"
}
+@article{Pada80,
+ author = "Padawitz, Peter",
+ title = "New results on completeness and consistency of abstract data
+ types",
+ journal = "LNCS",
+ volume = "88",
+ pages = "460-473",
+ year = "1980",
+ abstract =
+ "If an algebraic specification is designed in a structured way, a
+ small specification is stepwise enriched by more complex operations
+ and their defining equations. Based on normalization properties of
+ term reductions we present sufficient ``local'' conditions for the
+ completeness and consistency of enrichment steps, which can be
+ efficiently verified in many cases where other attempts to prove the
+ enrichment property ``syntactically'' have failed so far."
+}
+
@inproceedings{Pare93,
author = "Parent, Catherine",
title = "Developing Certified Programs in the System Coq: The Program
@@ -9895,6 +9984,14 @@ paper = "Brea89.pdf"
paper = "Ster17.pdf"
}
+@techreport{Stur95,
+ author = "Sturm, T.",
+ title = "A REDUCE package for first-order logic",
+ type = "technical report",
+ institution = "Universitat Passau",
+ year = "1995",
+}
+
@article{Ther01,
author = "Th\'ery, Laurent",
title = "A Machine-Checked Implementation of Buchberger's Algorithm",
@@ -20310,6 +20407,7 @@ paper = "Brea89.pdf"
within computer algebra, and also to outline some of the theoretical
issues raised by this practical application. We also give a
substantial bibliography.",
+ paper = "Dave00.pdf",
keywords = "axiomref"
}
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index e1da20b..e3c6269 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -9904,7 +9904,8 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp1215-1231
components from their specifications, and thus covers the whole
software development process from the specification of requirements to
the finished system. These methos are potentially applicable to the
- development of correct hardware systems as well"
+ development of correct hardware systems as well",
+ keywords = "axiomref, CAS-Proof"
}
@@ -10625,6 +10626,18 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp1215-1231
\end{chunk}
+\index{Crole, R.L.}
+\begin{chunk}{axiom.bib}
+@book{Crol93,
+ author = "Crole, R.L.",
+ title = "Categories for Types",
+ publisher = "Cambridge University Press",
+ year = "1993",
+ isbn = "978-0521457019"
+}
+
+\end{chunk}
+
\subsection{D} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Daly, Timothy}
@@ -10680,6 +10693,19 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp1215-1231
\index{Davenport, James H.}
\begin{chunk}{axiom.bib}
+@misc{Dave93a,
+ author = "Davenport, James H.",
+ title = "C9: Universal Algebra",
+ year = "1993",
+ comment = "Lecture Notes for 2nd year undergrad and mather's course
+ in Universal Algebra",
+ school = "University of Bath"
+}
+
+\end{chunk}
+
+\index{Davenport, James H.}
+\begin{chunk}{axiom.bib}
@article{Dave08,
author = "Davenport, James H.",
title = "Effective Set Membership in Computer Algebra and Beyond",
@@ -10787,6 +10813,18 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{Devlin, Keith J.}
+\begin{chunk}{axiom.bib}
+@book{Devl79,
+ author = "Devlin, Keith J.",
+ title = "Fundamentals of Contemporary Set Theory",
+ publisher = "Springer-Verlag",
+ year = "1979",
+ isbn = "978-0387904412"
+}
+
+\end{chunk}
+
\index{Dybjer, Peter}
\begin{chunk}{axiom.bib}
@inproceedings{Dybj90,
@@ -11239,6 +11277,33 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{Goguen, J.A.}
+\index{Meseguer, J.}
+\begin{chunk}{axiom.bib}
+@article{Gogu82,
+ author = "Goguen, J.A. and Meseguer, J.",
+ title = "Completeness of Many-sorted Equational Logic",
+ journal = "ACM SIGPLAN Notices",
+ volume = "17",
+ number = "1",
+ year = "1982",
+ pages = "9-17",
+ abstract =
+ "The rules of deduction which are usually used for many-sorted
+ equational logic in computer science, for example in the study of
+ abstract data types, are not sound. Correcting these rules by
+ introducing explicit quantifiers yields a system which, although it is
+ sound, is not complete; some new rules are needed for the addition and
+ deletion of quantifiers. This note is intended as an informal, but
+ precise, introduction to the main issues and results. It gives an
+ example showing the unsoundness of the usual rules; it also gives a
+ completeness theorem for our new rules, and gives necessary and
+ sufficient conditions for the old rules to agree with the new.",
+ paper = "Gogu82.pdf",
+}
+
+\end{chunk}
+
\index{Gordon, Mike}
\begin{chunk}{axiom.bib}
@misc{Gord96,
@@ -11853,6 +11918,25 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{Kounalis, Emmanuel}
+\index{Rusinowitch, Michael}
+\begin{chunk}{axiom.bib}
+@inproceedings{Koun90,
+ author = "Kounalis, Emmanuel and Rusinowitch, Michael",
+ title = "A Proof System for Conditional Algebraic Specifications",
+ booktitle = "Conference Conditional and Typed Rewriting Systems",
+ year = "1990",
+ abstract =
+ "Algebraic specifications provide a formal basis for designing
+ data-structures and reasoning about their properties.
+ Sufficient-completeness and consistency are fundamental
+ notions for building algebraic specifications in a modular way. We
+ give in this paper effective methods for testing these properties for
+ specifications with conditional axioms."
+}
+
+\end{chunk}
+
\index{Krebbers, Robbert Jan}
\begin{chunk}{axiom.bib}
@phdthesis{Kreb15,
@@ -12198,7 +12282,8 @@ England, Matthew; Wilson, David
automated theorem provers and discuss possible advantages and
disadvantages of these approaches. We also discuss some possible case
studies.",
- paper = "Mart97.ps"
+ paper = "Mart97.ps",
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -12317,6 +12402,18 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{Mendelson, Elliot}
+\begin{chunk}{axiom.bib}
+@book{Mend87,
+ author = "Mendelson, Elliot",
+ title = "Introduction to Mathematical Logic",
+ publisher = "Wadsworth and Brooks/Cole",
+ year = "1987",
+ isbn = "978-1482237726"
+}
+
+\end{chunk}
+
\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
@inproceedings{Mesh01,
@@ -12781,6 +12878,28 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\subsection{P} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Padawitz, Peter}
+\begin{chunk}{axiom.bib}
+@article{Pada80,
+ author = "Padawitz, Peter",
+ title = "New results on completeness and consistency of abstract data
+ types",
+ journal = "LNCS",
+ volume = "88",
+ pages = "460-473",
+ year = "1980",
+ abstract =
+ "If an algebraic specification is designed in a structured way, a
+ small specification is stepwise enriched by more complex operations
+ and their defining equations. Based on normalization properties of
+ term reductions we present sufficient ``local'' conditions for the
+ completeness and consistency of enrichment steps, which can be
+ efficiently verified in many cases where other attempts to prove the
+ enrichment property ``syntactically'' have failed so far."
+}
+
+\end{chunk}
+
\index{Parent, Catherine}
\begin{chunk}{axiom.bib}
@inproceedings{Pare93,
@@ -13456,6 +13575,18 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
+\index{Sturm, T.}
+\begin{chunk}{axiom.bib}
+@techreport{Stur95,
+ author = "Sturm, T.",
+ title = "A REDUCE package for first-order logic",
+ type = "technical report",
+ institution = "Universitat Passau",
+ year = "1995",
+}
+
+\end{chunk}
+
\subsection{T} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Th\'ery, Laurent}
@@ -29051,6 +29182,7 @@ VM/370 SPAD.SCRIPTS August 24, 1979 SPAD.SCRIPT
within computer algebra, and also to outline some of the theoretical
issues raised by this practical application. We also give a
substantial bibliography.",
+ paper = "Dave00.pdf",
keywords = "axiomref"
}
diff --git a/changelog b/changelog
index fe5fed2..ec81ad2 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20171009 tpd src/axiom-website/patches.html 20171009.01.tpd.patch
+20171009 tpd books/bookvolbib add references
20170929 tpd src/axiom-website/patches.html 20170929.01.tpd.patch
20170929 tpd books/bookvolbib add references
20170924 tpd src/axiom-website/patches.html 20170924.01.tpd.patch
diff --git a/patch b/patch
index 7c92d10..9967af7 100644
--- a/patch
+++ b/patch
@@ -2,79 +2,131 @@ books/bookvolbib add references
Goal: Proving Axiom Correct
-\index{Meshveliani, Sergei D.}
+\index{Sturm, T.}
\begin{chunk}{axiom.bib}
-@misc{Mesh13,
- author = "Meshveliani, Sergei D.",
- title = Dependent Types for an Adequate Programming of Algebra",
- link = "\url{http://ceur-ws.org/Vol-1010/paper-05.pdf}",
- year = "2005",
- abstract =
- "This research compares the authorâ€™s experience in program- ming
- algebra in Haskell and in Agda (currently the former experience is
- large, and the latter is small). There are discussed certain hopes and
- doubts related to the dependently typed and verified programming of
- symbolic computation. This concerns the 1) authorâ€™s experience
- history, 2) algebraic class hierarchy design, 3) proof cost overhead
- in evaluation and in coding, 4) other subjects. Various examples are
- considered.",
- paper = "Mesh13.pdf"
+@techreport{Stur95,
+ author = "Sturm, T.",
+ title = "A REDUCE package for first-order logic",
+ type = "technical report",
+ institution = "Universitat Passau",
+ year = "1995",
}
\end{chunk}
-\index{Norell, Ulf}
-\index{Chapman, James}
+\index{Crole, R.L.}
\begin{chunk}{axiom.bib}
-@misc{Nore08,
- author = "Norell, Ulf and Chapman, James",
- title = "Dependently Typed Programming in Agda",
- link = "\url{http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf}",
- year = "2008",
- paper = "Nore08.pdf"
+@book{Crol93,
+ author = "Crole, R.L.",
+ title = "Categories for Types",
+ publisher = "Cambridge University Press",
+ year = "1993",
+ isbn = "978-0521457019"
}
\end{chunk}
-\index{Bidoit, M.}
-\index{Kreowski, H.-J.}
-\index{Lescanne, P.}
-\index{Orejas, F.}
-\index{Sannella, D.}
+\index{Mendelson, Elliot}
\begin{chunk}{axiom.bib}
-@book{Bido91,
- author = "Bidoit, M. and Kreowski, H.-J. and Lescanne, P. and
- Orejas, F. and Sannella, D.",
- title = "Algebraic System Specification and Development",
+@book{Mend87,
+ author = "Mendelson, Elliot",
+ title = "Introduction to Mathematical Logic",
+ publisher = "Wadsworth and Brooks/Cole",
+ year = "1987",
+ isbn = "978-1482237726"
+}
+
+\end{chunk}
+
+\index{Devlin, Keith J.}
+\begin{chunk}{axiom.bib}
+@book{Devl79,
+ author = "Devlin, Keith J.",
+ title = "Fundamentals of Contemporary Set Theory",
publisher = "Springer-Verlag",
- comment = "LNCS 501",
- year = "1991",
- isbn = "3-540-54060-1",
+ year = "1979",
+ isbn = "978-0387904412"
+}
+
+\end{chunk}
+
+\index{Davenport, James H.}
+\begin{chunk}{axiom.bib}
+@misc{Dave93a,
+ author = "Davenport, James H.",
+ title = "C9: Universal Algebra",
+ year = "1993",
+ comment = "Lecture Notes for 2nd year undergrad and mather's course
+ in Universal Algebra",
+ school = "University of Bath"
+}
+
+\end{chunk}
+
+\index{Goguen, J.A.}
+\index{Meseguer, J.}
+\begin{chunk}{axiom.bib}
+@article{Gogu82,
+ author = "Goguen, J.A. and Meseguer, J.",
+ title = "Completeness of Many-sorted Equational Logic",
+ journal = "ACM SIGPLAN Notices",
+ volume = "17",
+ number = "1",
+ year = "1982",
+ pages = "9-17",
abstract =
- "A great deal of work has been devoted to methods of specification
- based on the simple idea that a functional program can be modelled as
- a {\sl many-sorted algebra}, i.e. as a number of sets of data values
- (one set of values for each data type) together with a number of total
- functions on those sets corresponding to the functions in the
- program. This abstracts away from the algorithms used to compute the
- functions and how those algorithms are expressed in a given
- programming language, focusing instead on the representation of data
- and the input/output behavior of functions. The pioneering work in
- this area is [Zil 74],[Gut 75], [GTW 76], of which the latter -- the
- so-called {\sl initial algebra approach} -- is the most formal This
- idea was soon taken up by other workers, see e.g. [GGM 76], [GHM 76],
- [BG 77], [GHM 78]. Today the field of algebraic specification has
- grown into one of the major areas of research in theoretical computer
- science. More than fifteen years of research have led to an abundance
- of competing and complementary theories and approaches. The algebraic
- approach provides a conceptual basis, theoretical fundations, and
- prototype tools for the stepwise formal development of correct system
- components from their specifications, and thus covers the whole
- software development process from the specification of requirements to
- the finished system. These methos are potentially applicable to the
- development of correct hardware systems as well"
+ "The rules of deduction which are usually used for many-sorted
+ equational logic in computer science, for example in the study of
+ abstract data types, are not sound. Correcting these rules by
+ introducing explicit quantifiers yields a system which, although it is
+ sound, is not complete; some new rules are needed for the addition and
+ deletion of quantifiers. This note is intended as an informal, but
+ precise, introduction to the main issues and results. It gives an
+ example showing the unsoundness of the usual rules; it also gives a
+ completeness theorem for our new rules, and gives necessary and
+ sufficient conditions for the old rules to agree with the new.",
+ paper = "Gogu82.pdf",
+}
+\end{chunk}
+
+\index{Padawitz, Peter}
+\begin{chunk}{axiom.bib}
+@article{Pada80,
+ author = "Padawitz, Peter",
+ title = "New results on completeness and consistency of abstract data
+ types",
+ journal = "LNCS",
+ volume = "88",
+ pages = "460-473",
+ year = "1980",
+ abstract =
+ "If an algebraic specification is designed in a structured way, a
+ small specification is stepwise enriched by more complex operations
+ and their defining equations. Based on normalization properties of
+ term reductions we present sufficient ``local'' conditions for the
+ completeness and consistency of enrichment steps, which can be
+ efficiently verified in many cases where other attempts to prove the
+ enrichment property ``syntactically'' have failed so far."
}
\end{chunk}
+\index{Kounalis, Emmanuel}
+\index{Rusinowitch, Michael}
+\begin{chunk}{axiom.bib}
+@inproceedings{Koun90,
+ author = "Kounalis, Emmanuel and Rusinowitch, Michael",
+ title = "A Proof System for Conditional Algebraic Specifications",
+ booktitle = "Conference Conditional and Typed Rewriting Systems",
+ year = "1990",
+ abstract =
+ "Algebraic specifications provide a formal basis for designing
+ data-structures and reasoning about their properties.
+ Sufficient-completeness and consistency are fundamental
+ notions for building algebraic specifications in a modular way. We
+ give in this paper effective methods for testing these properties for
+ specifications with conditional axioms."
+}
+
+\end{chunk}
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index d166d22..4ff3742 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5826,6 +5826,8 @@ add Jerry Archibald, Philip Santas, David Saunders

books/bookvolbib add references

20170929.01.tpd.patch
books/bookvolbib add references

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

--
1.9.1