From 18c885a75bdbb489166cdeca54faf44c439c94b5 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Fri, 15 Dec 2017 17:38:40 0500
Subject: [PATCH] books/bookvolbib add references
MIMEVersion: 1.0
ContentType: text/plain; charset=UTF8
ContentTransferEncoding: 8bit
Goal: Proving Axiom Correct
\index{Girard, JeanYves}
\index{Taylor, Paul}
\index{Lafont, Yves}
\begin{chunk}{axiom.bib}
@book{Gira03,
author = "Girard, JeanYves and Taylor, Paul and Lafont, Yves",
title = {{Proofs and Types}},
publisher = "Cambridge University Press",
link = "\url{http://www.paultaylor.eu/stable/prot.pdf}",
year = "2003"
}
\end{chunk}
\index{Rabe,Florian}
\index{Kohlhase, Michael}
\begin{chunk}{axiom.bib}
@article{Rabe13,
author = "Rabe,Florian and Kohlhase, Michael",
title = {{A Scalable Module System}},
journal = "Information and Computation",
volume = "230",
pages = "154",
year = "2013",
abstract =
"Symbolic and logic computation systems ranging from computer algebra
systems to theorem provers are finding their way into science,
technology, mathematics and engineering. But such systems rely on
explicitly or implicitly represented mathematical knowledge that needs
to be managed to use such systems effectively.
While mathematical knowledge management (MKM) ``in the small'' is
wellstudied, scaling up to large, highly interconnected corpora
remains difficult. We hold that in order to realize MKM “in the
large”, we need representation languages and software architectures
that are designed systematically with largescale processing in mind.
Therefore, we have designed and implemented the Mmt language – a
module system for mathematical theories. Mmt is designed as the
simplest possible language that combines a module system, a
foundationally uncommitted formal semantics, and webscalable
implementations. Due to a careful choice of representational
primitives, Mmt allows us to integrate existing representation
languages for formal mathematical knowledge in a simple, scalable
formalism. In particular, Mmt abstracts from the underlying
mathematical and logical foundations so that it can serve as a
standardized representation format for a formal digital
library. Moreover, Mmt systematically separates logicdependent and
logicindependent concerns so that it can serve as an interface layer
between computation systems and MKM systems.",
paper = "Rabe13.pdf"
}
\end{chunk}
\index{Rabe, Florian}
\begin{chunk}{axiom.bib}
@article{Rabe13a,
author = "Rabe, Florian",
title = {{The MMT API: A Generic MKM System}},
journal = "LNCS",
volume = "7961",
pages = "339343",
year = "2013",
abstract =
"The Mmt language has been developed as a scalable representation and
interchange language for formal mathematical knowledge. It permits
natural representations of the syntax and semantics of virtually all
declarative languages while making Mmtbased MKM services easy to
implement. It is foundationally unconstrained and can be instantiated
with specific formal languages.
The Mmt API implements the Mmt language along with multiple backends
for persistent storage and frontends for machine and user
access. Moreover, it implements a wide variety of Mmtbased knowledge
management services. The API and all services are generic and can be
applied to any language represented in Mmt. A plugin interface permits
injecting syntactic and semantic idiosyncrasies of individual formal
languages.",
paper = "Rabe13a.pdf"
}
\end{chunk}
\index{Kohlhase, Michael}
\index{Rabe, Florian}
\begin{chunk}{axiom.bib}
@article{Kohl16,
author = "Kohlhase, Michael and Rabe, Florian",
title = {{QED Reloaded: Towards a Pluralistic Formal Library of
Mathematical Knowledge}},
journal = "Journal of Formalized Reasoning",
volume = "9",
number = "1",
pages = "201234",
year = "2016",
abstract =
"Proposed in 1994, the ``QED project'' was one of the seminally
inflnuential initiatives in automated reasoning: It envisioned the
formalization of ``all of mathematics'' and the assembly of these
formalizations in a single coherent database. Even though it never led
to the concrete system, communal resource, or even joint research
envisioned in the QED manifesto, the idea lives on and shapes the
research agendas of a significant part of the community This paper
surveys a decade of work on representation languages and knowledge
management tools for mathematical knowledge conducted in the KWARC
research group at Jacobs University Bremen. It assembles the various
research strands into a coherent agenda for realizing the QED dream
with modern insights and technologies.",
paper = "Kohl16.pdf"
}
\end{chunk}
\index{Rabe, Florian}
\begin{chunk}{axiom.bib}
@article{Rabe16,
author = "Rabe, Florian",
title = {{The Future of Logic: FoundationIndependence}},
journal = "Logica Universalis",
volume = "10",
number = "1",
pages = "120",
year = "2016",
abstract =
"Throughout the twentieth century, the automation of formal logics in
computers has created unprecedented potential for practical
applications of logic—most prominently the mechanical verification of
mathematics and software. But the high cost of these applications
makes them infeasible but for a few flagship projects, and even those
are negligible compared to the everrising needs for verification. One
of the biggest challenges in the future of logic will be to enable
applications at much larger scales and simultaneously at much lower
costs. This will require a far more efficient allocation of
resources. Wherever possible, theoretical and practical results must
be formulated generically so that they can be instantiated to
arbitrary logics; this will allow reusing results in the face of
today’s multitude of applicationoriented and therefore diverging
logical systems. Moreover, the software engineering problems
concerning automation support must be decoupled from the theoretical
problems of designing logics and calculi; this will allow researchers
outside or at the fringe of logic to contribute scalable
logicindependent tools. Anticipating these needs, the author has
developed the Mmt framework. It offers a modern approach towards
defining, analyzing, implementing, and applying logics that focuses on
modular design and logicindependent results. This paper summarizes
the ideas behind and the results about Mmt. It focuses on showing how
Mmt. provides a theoretical and practical framework for the future of
logic.",
paper = "Rabe16.pdf",
}
\end{chunk}
\index{Rabe, Florian}
\begin{chunk}{axiom.bib}
@article{Rabe17,
author = "Rabe, Florian",
title = {{How to Identify, Translate, and Combine Logics?}},
journal = "J. of Logic and Computation",
volume = "27",
number = "6",
pages = "17531798",
year = "2017",
abstract =
"We give general definitions of logical frameworks and
logics. Examples include the logical frameworks LF and Isabelle and
the logics represented in them. We apply this to give general
definitions for equivalence of logics, translation between logics and
combination of logics. We also establish general criteria for the
soundness and completeness of these. Our key messages are that the
syntax and proof systems of logics are theories; that both semantics
and translations are theory morphisms; and that combinations are
colimits. Our approach is based on the Mmt language, which lets us
combine formalist declarative representations (and thus the associated
tool support) with abstract categorical conceptualizations.",
paper = "Rabe17.pdf"
}
\end{chunk}
\index{Halleck, John}
\begin{chunk}{axiom.bib}
@misc{Hall17,
author = "Halleck, John",
title = {{Logic System Interrelationships}},
year = "2017",
link = "\url{http://www.cc.utah.edu/~nahaj/logic/structures/index.html}"
}
\end{chunk}
\index{Yang, Xiang}
\index{Mittal, Rajat}
\begin{chunk}{axiom.bib}
@misc{Yang14,
author ="Yang, Xiang and Mittal, Rajat",
title = {{Acceleration of the Jacobi iterative method by factors exceeding
100 using scheduled relation}},
link = "\url{http://engineering.jhu.edu/fsag/wpcontent/uploads/sites/23/2013/10/JCP_revised_WebPost.pdf}",
paper = "Yang14.pdf"
}
\end{chunk}
\index{Geller, Murray}
\index{Ng, Edward W.}
\begin{chunk}{axiom.bib}
@misc{Gell69,
author = "Geller, Murray and Ng, Edward W.",
title = {{A Table of Integrals of the Exponential Integral}},
link =
"\url{http://nvlpubs.nist.gov/nistpubs/jres/73B/jresv73Bn3p191_A1b.pdf}",
abstract = "
This is a compendium of indefinite and definite integrals of products
of the Exponential Integral with elementary or transcendental functions.",
paper = "Gell69.pdf"
}
\end{chunk}
\index{Piroi, Florina}
\index{Kutsiz, Temur}
\begin{chunk}{axiom.bib}
@article{Piro05,
author = "Piroi, Florina and Kutsiz, Temur",
title = {{The Theorema Environment for Interactive Proof Development}},
journal = "LNAI",
volume = "3835",
pages = "261275",
year = "2005",
abstract =
"We describe an environment that allows the users of the Theorema
system to flexibly control aspects of computersupported proof
development. The environment supports the display and manipulation of
proof trees and proof situations, logs the user activities (commands
communicated with the system during the proving session), and presents
(also unfinished) proofs in a humanoriented style. In particular, the
user can navigate through the proof object, expand/remove proof
branches, provide witness terms, develop several proofs concurrently,
proceed step by step or automatically and so on. The environment
enhances the effectiveness and flexibility of the reasoners of the
Theorema system.",
paper = "Piro05.pdf"
}
\end{chunk}
\index{Priest, Graham}
\begin{chunk}{axiom.bib}
@book{Prie12,
author = "Priest, Graham",
title = {{An Introduction to NonClassical Logic}},
year = "2012",
publisher = "Cambridge University Press"
}
\end{chunk}
\index{Beeson, Michael J.}
\begin{chunk}{axiom.bib}
@article{Bees90,
author = "Beeson, Michael J.",
title = {{Review of Implementing Mathematics with the Nuprl Proof
Development System}},
journal = "J. of Symbolic Logic",
volume = "55",
number = "3",
pages = "12991302",
year = "1990",
link = "\url{http://www.jstor.org/stable/2274489}",
paper = "Bees90.pdf"
}
\end{chunk}
\index{Beeson, Michael J.}
\begin{chunk}{axiom.bib}
#InCollection{Bees89,
author = "Beeson, Michael J.",
title = {{Logic and Computation in MATHPERT: An Expert System for
Learning Mathematics}},
booktitle = "Computers and Mathematics",
publisher = "SpringerVerlag",
year = "1989",
pages = "299307",
isbn = "0387970193"
}
\end{chunk}
\index{Harrison, John}
\begin{chunk}{axiom.bib}
@misc{Harr06a,
author = "Harrison, John",
title = {{Formal Verification of Floatingpoint Arithmetic at Intel}},
year = "2006",
link = "\url{http://www.cl.cam.ac.uk/~jrh13/slides/jnao02jun06/slides.pdf}",
paper = "Harr06a.pdf"
}
\end{chunk}
\index{Beeson, Michael}
\begin{chunk}{axiom.bib}
@article{Bees89a,
author = "Beeson, Michael",
title = {{Some Applications of Gentzen's Proof Theory in Automated
Deduction}},
journal = "LNCS",
volume = "475",
pages = "101156",
year = "1989",
abstract =
"We show that Prolog is intimately connected with Gentzen's cutfree
sequent calculus G, analyzing Prolog computations as the construction
of certain cutfree derivations. We introduce a theoremproving
program GENTZEN based on Gentzen's sequent calculus, which
incorporates some features of Prolog's computation procedure. We show
that GENTZEN has the following properties: (1) It is
(nondeterministically) sound and complete for firstorder
intuitionistic predicate calculus; (2) Its successful computations
coincide with those of Prolog on the Horn clause fragment (both
deterministically and nondeterministically). The proofs of (1) and
(2) contain a new proof of the completeness of (nondeterministic)
Prolog for Horn clause logic, based on our analysis of Prolog in terms
of Gentzen sequents instead of on resolution. GENTZEN has been
implemented and tested on examples including some proofs by induction
in number theory, an example constructed by J. McCarthy to show the
limitations of Prolog, and ``Schubert's Steamroller.'' An extension of
GENTZEN also provides a decision procedure for intuitionistic
propositional calculus (but at some cost in efficiency).",
paper = "Bees89a.pdf"
}
\end{chunk}
\index{Restall, Greg}
\begin{chunk}{axiom.bib}
@book{Rest00,
author = "Restall, Greg",
title = {{An Introduction to Substructural Logics}},
year = "2000",
publisher = "Routledge",
isbn = "041521534X"
}
\end{chunk}
\index{Font, Josep Marie}
\begin{chunk}{axiom.bib}
@book{Font16,
author = "Font, Josep Marie",
title = {{Abstract Algebraic Logic: An Introductory Textbook}},
year = "2016",
publisher = "College Publications, Kings College",
isbn = "9781848902077"
}
\end{chunk}

books/axiom.bib  302 +++++++++++++++
books/bookvolbib.pamphlet  355 ++++++++++++++++++
changelog  2 +
patch  782 ++++++++++++++
src/axiomwebsite/patches.html  2 +
5 files changed, 915 insertions(+), 528 deletions()
diff git a/books/axiom.bib b/books/axiom.bib
index 2404f2b..284d5e4 100644
 a/books/axiom.bib
+++ b/books/axiom.bib
@@ 6478,6 +6478,14 @@ paper = "Brea89.pdf"
year = "1971"
}
+@misc{Yang14,
+ author ="Yang, Xiang and Mittal, Rajat",
+ title = {{Acceleration of the Jacobi iterative method by factors exceeding
+ 100 using scheduled relation}},
+ link = "\url{http://engineering.jhu.edu/fsag/wpcontent/uploads/sites/23/2013/10/JCP_revised_WebPost.pdf}",
+ paper = "Yang14.pdf"
+}
+
@inproceedings{Badd94,
author = "Baddoura, Jamil",
title = {{A Conjecture On Integration in Finite Terms with Elementary
@@ 6632,6 +6640,17 @@ paper = "Brea89.pdf"
publisher = "Dover Publications"
}
+@misc{Ng68,
+ author = "Ng, Edward W. and Geller, Murray",
+ title = {{A Table of Integrals of the Error functions}},
+ link =
+ "\url{http://nvlpubs.nist.gov/nistpubs/jres/73B/jresv73Bn1p1_A1b.pdf}",
+ abstract = "
+ This is a compendium of indefinite and definite integrals of products
+ of the Error functions with elementary and transcendental functions.",
+ paper = "Ng68.pdf"
+}
+
@article{Nort80,
author = "Norton, Lewis M.",
title = {{A Note about Laplace Transform Tables for Computer use}},
@@ 6671,6 +6690,17 @@ paper = "Brea89.pdf"
in Piquette, in review (b)."
}
+@misc{Gell69,
+ author = "Geller, Murray and Ng, Edward W.",
+ title = {{A Table of Integrals of the Exponential Integral}},
+ link =
+ "\url{http://nvlpubs.nist.gov/nistpubs/jres/73B/jresv73Bn3p191_A1b.pdf}",
+ abstract = "
+ This is a compendium of indefinite and definite integrals of products
+ of the Exponential Integral with elementary or transcendental functions.",
+ paper = "Gell69.pdf"
+}
+
@techreport{Segl98,
author = "Segletes, S.B.",
title = {{A compact analytical fit to the exponential integral $E_1(x)$}},
@@ 6943,6 +6973,22 @@ paper = "Brea89.pdf"
paper = "Cons85a.pdf"
}
+@book{Font16,
+ author = "Font, Josep Marie",
+ title = {{Abstract Algebraic Logic: An Introductory Textbook}},
+ year = "2016",
+ publisher = "College Publications, Kings College",
+ isbn = "9781848902077"
+}
+
+@book{Rest00,
+ author = "Restall, Greg",
+ title = {{An Introduction to Substructural Logics}},
+ year = "2000",
+ publisher = "Routledge",
+ isbn = "041521534X"
+}
+
@article{Tryb92,
author = "Trybulec, Zinaida and Swieczkowska, Halina",
title = {{Some Remarks on The Language of Mathematical Texts}},
@@ 7385,7 +7431,7 @@ paper = "Brea89.pdf"
@inproceedings{Ball95,
author = "Ballarin, Clemens and Homann, Karsten and Calmet, Jacques",
title =
 {{Theorems and Algorithms: An Interface between Isabelle and Maple"}},
+ {{Theorems and Algorithms: An Interface between Isabelle and Maple}},
booktitle = "ISSAC 95",
year = "1995",
pages = "150157",
@@ 7409,7 +7455,6 @@ paper = "Brea89.pdf"
some examples that can be solved by theorems and algorithms",
paper = "Ball95.pdf",
keywords = "axiomref, CASProof"

}
@misc{Ball98,
@@ 7566,6 +7611,47 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+#InCollection{Bees89,
+ author = "Beeson, Michael J.",
+ title = {{Logic and Computation in MATHPERT: An Expert System for
+ Learning Mathematics}},
+ booktitle = "Computers and Mathematics",
+ publisher = "SpringerVerlag",
+ year = "1989",
+ pages = "299307",
+ isbn = "0387970193"
+}
+
+@article{Bees89a,
+ author = "Beeson, Michael",
+ title = {{Some Applications of Gentzen's Proof Theory in Automated
+ Deduction}},
+ journal = "LNCS",
+ volume = "475",
+ pages = "101156",
+ year = "1989",
+ abstract =
+ "We show that Prolog is intimately connected with Gentzen's cutfree
+ sequent calculus G, analyzing Prolog computations as the construction
+ of certain cutfree derivations. We introduce a theoremproving
+ program GENTZEN based on Gentzen's sequent calculus, which
+ incorporates some features of Prolog's computation procedure. We show
+ that GENTZEN has the following properties: (1) It is
+ (nondeterministically) sound and complete for firstorder
+ intuitionistic predicate calculus; (2) Its successful computations
+ coincide with those of Prolog on the Horn clause fragment (both
+ deterministically and nondeterministically). The proofs of (1) and
+ (2) contain a new proof of the completeness of (nondeterministic)
+ Prolog for Horn clause logic, based on our analysis of Prolog in terms
+ of Gentzen sequents instead of on resolution. GENTZEN has been
+ implemented and tested on examples including some proofs by induction
+ in number theory, an example constructed by J. McCarthy to show the
+ limitations of Prolog, and ``Schubert's Steamroller.'' An extension of
+ GENTZEN also provides a decision procedure for intuitionistic
+ propositional calculus (but at some cost in efficiency).",
+ paper = "Bees89a.pdf"
+}
+
@article{Bees92,
author = "Beeson, M.",
title = {{Mathpert: Computer support for learning algebra, trig, and
@@ 9888,11 +9974,21 @@ paper = "Brea89.pdf"
paper = "Harr96.pdf"
}
+@misc{Harr06a,
+ author = "Harrison, John",
+ title = {{Formal Verification of Floatingpoint Arithmetic at Intel}},
+ year = "2006",
+ link = "\url{http://www.cl.cam.ac.uk/~jrh13/slides/jnao02jun06/slides.pdf}",
+ paper = "Harr06a.pdf"
+}
+
@misc{Hear12,
author = "Hearn, Peter W.O.",
title = {{A Primer on Separation Logic (and Automatic Program
Verification and Analysis}},
year = "2012",
+ link =
+"\url{www0.cs.ucl.ac.uk/staff/p.ohearn/papers/Marktoberdorf11LectureNotes.pdf}",
abstract =
"These are the notes to accompany a course at the Marktoberdorf PhD
summer school in 2011. The course consists of an introduction to
@@ 11696,6 +11792,28 @@ paper = "Brea89.pdf"
undergraduate and graduate students."
}
+@article{Piro05,
+ author = "Piroi, Florina and Kutsiz, Temur",
+ title = {{The Theorema Environment for Interactive Proof Development}},
+ journal = "LNAI",
+ volume = "3835",
+ pages = "261275",
+ year = "2005",
+ abstract =
+ "We describe an environment that allows the users of the Theorema
+ system to flexibly control aspects of computersupported proof
+ development. The environment supports the display and manipulation of
+ proof trees and proof situations, logs the user activities (commands
+ communicated with the system during the proving session), and presents
+ (also unfinished) proofs in a humanoriented style. In particular, the
+ user can navigate through the proof object, expand/remove proof
+ branches, provide witness terms, develop several proofs concurrently,
+ proceed step by step or automatically and so on. The environment
+ enhances the effectiveness and flexibility of the reasoners of the
+ Theorema system.",
+ paper = "Piro05.pdf"
+}
+
@article{Plot77,
author = "Plotkin, G.D.",
title = {{LCF Considered as a Programming Language}},
@@ 32282,6 +32400,19 @@ paper = "Brea89.pdf"
keywords = "CASProof"
}
+@article{Bees90,
+ author = "Beeson, Michael J.",
+ title = {{Review of Implementing Mathematics with the Nuprl Proof
+ Development System}},
+ journal = "J. of Symbolic Logic",
+ volume = "55",
+ number = "3",
+ pages = "12991302",
+ year = "1990",
+ link = "\url{http://www.jstor.org/stable/2274489}",
+ paper = "Bees90.pdf"
+}
+
@book{Beez15,
author = "Judson, Tom and Beezer, Rob",
title = {{Abstract Algebra: Theory and Applications}},
@@ 33658,6 +33789,14 @@ paper = "Brea89.pdf"
paper = "Gies05.pdf"
}
+@book{Gira03,
+ author = "Girard, JeanYves and Taylor, Paul and Lafont, Yves",
+ title = {{Proofs and Types}},
+ publisher = "Cambridge University Press",
+ link = "\url{http://www.paultaylor.eu/stable/prot.pdf}",
+ year = "2003"
+}
+
@misc{Gode16,
author = "Godek, Panicz Maciej",
title = {{A Pamphlet Against R}},
@@ 33858,6 +33997,13 @@ paper = "Brea89.pdf"
paper = "Haft06.pdf"
}
+@misc{Hall17,
+ author = "Halleck, John",
+ title = {{Logic System Interrelationships}},
+ year = "2017",
+ link = "\url{http://www.cc.utah.edu/~nahaj/logic/structures/index.html}"
+}
+
@inproceedings{Haml02,
author = "Hamlet, Dick",
title = {{Continuity in Software Systems}},
@@ 34476,6 +34622,31 @@ paper = "Brea89.pdf"
isbn = "0937073814"
}
+@article{Kohl16,
+ author = "Kohlhase, Michael and Rabe, Florian",
+ title = {{QED Reloaded: Towards a Pluralistic Formal Library of
+ Mathematical Knowledge}},
+ journal = "Journal of Formalized Reasoning",
+ volume = "9",
+ number = "1",
+ pages = "201234",
+ year = "2016",
+ abstract =
+ "Proposed in 1994, the ``QED project'' was one of the seminally
+ inflnuential initiatives in automated reasoning: It envisioned the
+ formalization of ``all of mathematics'' and the assembly of these
+ formalizations in a single coherent database. Even though it never led
+ to the concrete system, communal resource, or even joint research
+ envisioned in the QED manifesto, the idea lives on and shapes the
+ research agendas of a significant part of the community This paper
+ surveys a decade of work on representation languages and knowledge
+ management tools for mathematical knowledge conducted in the KWARC
+ research group at Jacobs University Bremen. It assembles the various
+ research strands into a coherent agenda for realizing the QED dream
+ with modern insights and technologies.",
+ paper = "Kohl16.pdf"
+}
+
@article{Kome12,
author = "Komendantsky, V. and Konovalov, A. and Linton, S.A.",
title = {{Interfacing Coq + SSReflect with GAP}},
@@ 35577,6 +35748,13 @@ paper = "Brea89.pdf"
link = "\url{https://www.youtube.com/watch?v=jG61w5pOc2A}"
}
+@book{Prie12,
+ author = "Priest, Graham",
+ title = {{An Introduction to NonClassical Logic}},
+ year = "2012",
+ publisher = "Cambridge University Press"
+}
+
@inproceedings{Popo09,
author = "Popov, Nikolaj and Jebelean, Tudor",
title = {{Functional Program Verification in Theorema Soundness and
@@ 35649,6 +35827,126 @@ paper = "Brea89.pdf"
link = "\url{http://www.puffinwarellc.com/p3a.htm}"
}
+@article{Rabe13,
+ author = "Rabe,Florian and Kohlhase, Michael",
+ title = {{A Scalable Module System}},
+ journal = "Information and Computation",
+ volume = "230",
+ pages = "154",
+ year = "2013",
+ abstract =
+ "Symbolic and logic computation systems ranging from computer algebra
+ systems to theorem provers are finding their way into science,
+ technology, mathematics and engineering. But such systems rely on
+ explicitly or implicitly represented mathematical knowledge that needs
+ to be managed to use such systems effectively.
+
+ While mathematical knowledge management (MKM) ``in the small'' is
+ wellstudied, scaling up to large, highly interconnected corpora
+ remains difficult. We hold that in order to realize MKM “in the
+ large”, we need representation languages and software architectures
+ that are designed systematically with largescale processing in mind.
+
+ Therefore, we have designed and implemented the Mmt language – a
+ module system for mathematical theories. Mmt is designed as the
+ simplest possible language that combines a module system, a
+ foundationally uncommitted formal semantics, and webscalable
+ implementations. Due to a careful choice of representational
+ primitives, Mmt allows us to integrate existing representation
+ languages for formal mathematical knowledge in a simple, scalable
+ formalism. In particular, Mmt abstracts from the underlying
+ mathematical and logical foundations so that it can serve as a
+ standardized representation format for a formal digital
+ library. Moreover, Mmt systematically separates logicdependent and
+ logicindependent concerns so that it can serve as an interface layer
+ between computation systems and MKM systems.",
+ paper = "Rabe13.pdf"
+}
+
+@article{Rabe13a,
+ author = "Rabe, Florian",
+ title = {{The MMT API: A Generic MKM System}},
+ journal = "LNCS",
+ volume = "7961",
+ pages = "339343",
+ year = "2013",
+ abstract =
+ "The Mmt language has been developed as a scalable representation and
+ interchange language for formal mathematical knowledge. It permits
+ natural representations of the syntax and semantics of virtually all
+ declarative languages while making Mmtbased MKM services easy to
+ implement. It is foundationally unconstrained and can be instantiated
+ with specific formal languages.
+
+ The Mmt API implements the Mmt language along with multiple backends
+ for persistent storage and frontends for machine and user
+ access. Moreover, it implements a wide variety of Mmtbased knowledge
+ management services. The API and all services are generic and can be
+ applied to any language represented in Mmt. A plugin interface permits
+ injecting syntactic and semantic idiosyncrasies of individual formal
+ languages.",
+ paper = "Rabe13a.pdf"
+}
+
+@article{Rabe16,
+ author = "Rabe, Florian",
+ title = {{The Future of Logic: FoundationIndependence}},
+ journal = "Logica Universalis",
+ volume = "10",
+ number = "1",
+ pages = "120",
+ year = "2016",
+ abstract =
+ "Throughout the twentieth century, the automation of formal logics in
+ computers has created unprecedented potential for practical
+ applications of logic—most prominently the mechanical verification of
+ mathematics and software. But the high cost of these applications
+ makes them infeasible but for a few flagship projects, and even those
+ are negligible compared to the everrising needs for verification. One
+ of the biggest challenges in the future of logic will be to enable
+ applications at much larger scales and simultaneously at much lower
+ costs. This will require a far more efficient allocation of
+ resources. Wherever possible, theoretical and practical results must
+ be formulated generically so that they can be instantiated to
+ arbitrary logics; this will allow reusing results in the face of
+ today’s multitude of applicationoriented and therefore diverging
+ logical systems. Moreover, the software engineering problems
+ concerning automation support must be decoupled from the theoretical
+ problems of designing logics and calculi; this will allow researchers
+ outside or at the fringe of logic to contribute scalable
+ logicindependent tools. Anticipating these needs, the author has
+ developed the Mmt framework. It offers a modern approach towards
+ defining, analyzing, implementing, and applying logics that focuses on
+ modular design and logicindependent results. This paper summarizes
+ the ideas behind and the results about Mmt. It focuses on showing how
+ Mmt. provides a theoretical and practical framework for the future of
+ logic.",
+ paper = "Rabe16.pdf",
+}
+
+@article{Rabe17,
+ author = "Rabe, Florian",
+ title = {{How to Identify, Translate, and Combine Logics?}},
+ journal = "J. of Logic and Computation",
+ volume = "27",
+ number = "6",
+ pages = "17531798",
+ year = "2017",
+ abstract =
+ "We give general definitions of logical frameworks and
+ logics. Examples include the logical frameworks LF and Isabelle and
+ the logics represented in them. We apply this to give general
+ definitions for equivalence of logics, translation between logics and
+ combination of logics. We also establish general criteria for the
+ soundness and completeness of these. Our key messages are that the
+ syntax and proof systems of logics are theories; that both semantics
+ and translations are theory morphisms; and that combinations are
+ colimits. Our approach is based on the Mmt language, which lets us
+ combine formalist declarative representations (and thus the associated
+ tool support) with abstract categorical conceptualizations.",
+ paper = "Rabe17.pdf"
+}
+
@phdthesis{Rave91,
author = "Ravenscroft, Robert Andrews Jr.",
title = {{Generating Function Algorithms for Symbolic Computation}},
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index d086a67..d64da0c 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 8853,8 +8853,8 @@ when shown in factored form.
\index{Yang, Xiang}
\index{Mittal, Rajat}
\begin{chunk}{ignore}
{Yang14,
+\begin{chunk}{axiom.bib}
+@misc{Yang14,
author ="Yang, Xiang and Mittal, Rajat",
title = {{Acceleration of the Jacobi iterative method by factors exceeding
100 using scheduled relation}},
@@ 9058,11 +9058,12 @@ when shown in factored form.
\index{Ng, Edward W.}
\index{Geller, Murray}
\begin{chunk}{ignore}
{Ng68,
+\begin{chunk}{axiom.bib}
+@misc{Ng68,
author = "Ng, Edward W. and Geller, Murray",
title = {{A Table of Integrals of the Error functions}},
 link = "\url{http://nvlpubs.nist.gov/nistpubs/jres/73B/jresv73Bn1p1_A1b.pdf}",
+ link =
+ "\url{http://nvlpubs.nist.gov/nistpubs/jres/73B/jresv73Bn1p1_A1b.pdf}",
abstract = "
This is a compendium of indefinite and definite integrals of products
of the Error functions with elementary and transcendental functions.",
@@ 9122,11 +9123,12 @@ when shown in factored form.
\index{Geller, Murray}
\index{Ng, Edward W.}
\begin{chunk}{ignore}
{Gell69,
+\begin{chunk}{axiom.bib}
+@misc{Gell69,
author = "Geller, Murray and Ng, Edward W.",
title = {{A Table of Integrals of the Exponential Integral}},
 link = "\url{http://nvlpubs.nist.gov/nistpubs/jres/73B/jresv73Bn3p191_A1b.pdf}",
+ link =
+ "\url{http://nvlpubs.nist.gov/nistpubs/jres/73B/jresv73Bn3p191_A1b.pdf}",
abstract = "
This is a compendium of indefinite and definite integrals of products
of the Exponential Integral with elementary or transcendental functions.",
@@ 9478,6 +9480,30 @@ when shown in factored form.
\end{chunk}
+\index{Font, Josep Marie}
+\begin{chunk}{axiom.bib}
+@book{Font16,
+ author = "Font, Josep Marie",
+ title = {{Abstract Algebraic Logic: An Introductory Textbook}},
+ year = "2016",
+ publisher = "College Publications, Kings College",
+ isbn = "9781848902077"
+}
+
+\end{chunk}
+
+\index{Restall, Greg}
+\begin{chunk}{axiom.bib}
+@book{Rest00,
+ author = "Restall, Greg",
+ title = {{An Introduction to Substructural Logics}},
+ year = "2000",
+ publisher = "Routledge",
+ isbn = "041521534X"
+}
+
+\end{chunk}
+
\index{Trybulec, Zinaida}
\index{Swieczkowska, Halina}
\begin{chunk}{axiom.bib}
@@ 10073,7 +10099,7 @@ when shown in factored form.
@inproceedings{Ball95,
author = "Ballarin, Clemens and Homann, Karsten and Calmet, Jacques",
title =
 {{Theorems and Algorithms: An Interface between Isabelle and Maple"}},
+ {{Theorems and Algorithms: An Interface between Isabelle and Maple}},
booktitle = "ISSAC 95",
year = "1995",
pages = "150157",
@@ 10097,7 +10123,6 @@ when shown in factored form.
some examples that can be solved by theorems and algorithms",
paper = "Ball95.pdf",
keywords = "axiomref, CASProof"

}
\end{chunk}
@@ 10281,6 +10306,55 @@ when shown in factored form.
\end{chunk}
+\index{Beeson, Michael J.}
+\begin{chunk}{axiom.bib}
+#InCollection{Bees89,
+ author = "Beeson, Michael J.",
+ title = {{Logic and Computation in MATHPERT: An Expert System for
+ Learning Mathematics}},
+ booktitle = "Computers and Mathematics",
+ publisher = "SpringerVerlag",
+ year = "1989",
+ pages = "299307",
+ isbn = "0387970193"
+}
+
+\end{chunk}
+
+\index{Beeson, Michael}
+\begin{chunk}{axiom.bib}
+@article{Bees89a,
+ author = "Beeson, Michael",
+ title = {{Some Applications of Gentzen's Proof Theory in Automated
+ Deduction}},
+ journal = "LNCS",
+ volume = "475",
+ pages = "101156",
+ year = "1989",
+ abstract =
+ "We show that Prolog is intimately connected with Gentzen's cutfree
+ sequent calculus G, analyzing Prolog computations as the construction
+ of certain cutfree derivations. We introduce a theoremproving
+ program GENTZEN based on Gentzen's sequent calculus, which
+ incorporates some features of Prolog's computation procedure. We show
+ that GENTZEN has the following properties: (1) It is
+ (nondeterministically) sound and complete for firstorder
+ intuitionistic predicate calculus; (2) Its successful computations
+ coincide with those of Prolog on the Horn clause fragment (both
+ deterministically and nondeterministically). The proofs of (1) and
+ (2) contain a new proof of the completeness of (nondeterministic)
+ Prolog for Horn clause logic, based on our analysis of Prolog in terms
+ of Gentzen sequents instead of on resolution. GENTZEN has been
+ implemented and tested on examples including some proofs by induction
+ in number theory, an example constructed by J. McCarthy to show the
+ limitations of Prolog, and ``Schubert's Steamroller.'' An extension of
+ GENTZEN also provides a decision procedure for intuitionistic
+ propositional calculus (but at some cost in efficiency).",
+ paper = "Bees89a.pdf"
+}
+
+\end{chunk}
+
\index{Beeson, M.}
\begin{chunk}{axiom.bib}
@article{Bees92,
@@ 13323,6 +13397,18 @@ when shown in factored form.
\end{chunk}
+\index{Harrison, John}
+\begin{chunk}{axiom.bib}
+@misc{Harr06a,
+ author = "Harrison, John",
+ title = {{Formal Verification of Floatingpoint Arithmetic at Intel}},
+ year = "2006",
+ link = "\url{http://www.cl.cam.ac.uk/~jrh13/slides/jnao02jun06/slides.pdf}",
+ paper = "Harr06a.pdf"
+}
+
+\end{chunk}
+
\index{Hearn, Peter W.O.}
\begin{chunk}{axiom.bib}
@misc{Hear12,
@@ 13330,6 +13416,8 @@ when shown in factored form.
title = {{A Primer on Separation Logic (and Automatic Program
Verification and Analysis}},
year = "2012",
+ link =
+"\url{www0.cs.ucl.ac.uk/staff/p.ohearn/papers/Marktoberdorf11LectureNotes.pdf}",
abstract =
"These are the notes to accompany a course at the Marktoberdorf PhD
summer school in 2011. The course consists of an introduction to
@@ 15585,6 +15673,33 @@ when shown in factored form.
\end{chunk}
+\index{Piroi, Florina}
+\index{Kutsiz, Temur}
+\begin{chunk}{axiom.bib}
+@article{Piro05,
+ author = "Piroi, Florina and Kutsiz, Temur",
+ title = {{The Theorema Environment for Interactive Proof Development}},
+ journal = "LNAI",
+ volume = "3835",
+ pages = "261275",
+ year = "2005",
+ abstract =
+ "We describe an environment that allows the users of the Theorema
+ system to flexibly control aspects of computersupported proof
+ development. The environment supports the display and manipulation of
+ proof trees and proof situations, logs the user activities (commands
+ communicated with the system during the proving session), and presents
+ (also unfinished) proofs in a humanoriented style. In particular, the
+ user can navigate through the proof object, expand/remove proof
+ branches, provide witness terms, develop several proofs concurrently,
+ proceed step by step or automatically and so on. The environment
+ enhances the effectiveness and flexibility of the reasoners of the
+ Theorema system.",
+ paper = "Piro05.pdf"
+}
+
+\end{chunk}
+
\index{Plotkin, G.D.}
\begin{chunk}{axiom.bib}
@article{Plot77,
@@ 47453,6 +47568,23 @@ J. Symbolic Computation (1993) 15, 393413
\end{chunk}
+\index{Beeson, Michael J.}
+\begin{chunk}{axiom.bib}
+@article{Bees90,
+ author = "Beeson, Michael J.",
+ title = {{Review of Implementing Mathematics with the Nuprl Proof
+ Development System}},
+ journal = "J. of Symbolic Logic",
+ volume = "55",
+ number = "3",
+ pages = "12991302",
+ year = "1990",
+ link = "\url{http://www.jstor.org/stable/2274489}",
+ paper = "Bees90.pdf"
+}
+
+\end{chunk}
+
\index{Judson, Tom}
\index{Beezer, Rob}
\begin{chunk}{axiom.bib}
@@ 50140,6 +50272,20 @@ Report SOL 866R. Department of Operations Research, Stanford University. 1986
\end{chunk}
+\index{Girard, JeanYves}
+\index{Taylor, Paul}
+\index{Lafont, Yves}
+\begin{chunk}{axiom.bib}
+@book{Gira03,
+ author = "Girard, JeanYves and Taylor, Paul and Lafont, Yves",
+ title = {{Proofs and Types}},
+ publisher = "Cambridge University Press",
+ link = "\url{http://www.paultaylor.eu/stable/prot.pdf}",
+ year = "2003"
+}
+
+\end{chunk}
+
\index{Gladwell, I.}
\begin{chunk}{ignore}
\bibitem[Gladwell 79]{Gla79} Gladwell I
@@ 50516,6 +50662,17 @@ Grove, IL, USA and Oxford, UK, 1992
\end{chunk}
+\index{Halleck, John}
+\begin{chunk}{axiom.bib}
+@misc{Hall17,
+ author = "Halleck, John",
+ title = {{Logic System Interrelationships}},
+ year = "2017",
+ link = "\url{http://www.cc.utah.edu/~nahaj/logic/structures/index.html}"
+}
+
+\end{chunk}
+
\index{Hall, G.}
\index{Watt J M.}
\begin{chunk}{ignore}
@@ 51531,6 +51688,36 @@ J. Symbolic Computations 8, 545552 (1989)
\end{chunk}
+\index{Kohlhase, Michael}
+\index{Rabe, Florian}
+\begin{chunk}{axiom.bib}
+@article{Kohl16,
+ author = "Kohlhase, Michael and Rabe, Florian",
+ title = {{QED Reloaded: Towards a Pluralistic Formal Library of
+ Mathematical Knowledge}},
+ journal = "Journal of Formalized Reasoning",
+ volume = "9",
+ number = "1",
+ pages = "201234",
+ year = "2016",
+ abstract =
+ "Proposed in 1994, the ``QED project'' was one of the seminally
+ inflnuential initiatives in automated reasoning: It envisioned the
+ formalization of ``all of mathematics'' and the assembly of these
+ formalizations in a single coherent database. Even though it never led
+ to the concrete system, communal resource, or even joint research
+ envisioned in the QED manifesto, the idea lives on and shapes the
+ research agendas of a significant part of the community This paper
+ surveys a decade of work on representation languages and knowledge
+ management tools for mathematical knowledge conducted in the KWARC
+ research group at Jacobs University Bremen. It assembles the various
+ research strands into a coherent agenda for realizing the QED dream
+ with modern insights and technologies.",
+ paper = "Kohl16.pdf"
+}
+
+\end{chunk}
+
\index{Kolchin, E.R.}
\begin{chunk}{ignore}
\bibitem[Kolchin 73]{Kol73} Kolchin, E.R.
@@ 53420,6 +53607,17 @@ SpringerVerlag.(1983)
\end{chunk}
+\index{Priest, Graham}
+\begin{chunk}{axiom.bib}
+@book{Prie12,
+ author = "Priest, Graham",
+ title = {{An Introduction to NonClassical Logic}},
+ year = "2012",
+ publisher = "Cambridge University Press"
+}
+
+\end{chunk}
+
\index{Polya, G.}
\begin{chunk}{ignore}
\bibitem[Polya 37]{Pol37} Polya, G.
@@ 53592,6 +53790,143 @@ ACM Transactions on Mathematical Software, 32(2):180194, June 2006.
\subsection{R} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Rabe,Florian}
+\index{Kohlhase, Michael}
+\begin{chunk}{axiom.bib}
+@article{Rabe13,
+ author = "Rabe,Florian and Kohlhase, Michael",
+ title = {{A Scalable Module System}},
+ journal = "Information and Computation",
+ volume = "230",
+ pages = "154",
+ year = "2013",
+ abstract =
+ "Symbolic and logic computation systems ranging from computer algebra
+ systems to theorem provers are finding their way into science,
+ technology, mathematics and engineering. But such systems rely on
+ explicitly or implicitly represented mathematical knowledge that needs
+ to be managed to use such systems effectively.
+
+ While mathematical knowledge management (MKM) ``in the small'' is
+ wellstudied, scaling up to large, highly interconnected corpora
+ remains difficult. We hold that in order to realize MKM “in the
+ large”, we need representation languages and software architectures
+ that are designed systematically with largescale processing in mind.
+
+ Therefore, we have designed and implemented the Mmt language – a
+ module system for mathematical theories. Mmt is designed as the
+ simplest possible language that combines a module system, a
+ foundationally uncommitted formal semantics, and webscalable
+ implementations. Due to a careful choice of representational
+ primitives, Mmt allows us to integrate existing representation
+ languages for formal mathematical knowledge in a simple, scalable
+ formalism. In particular, Mmt abstracts from the underlying
+ mathematical and logical foundations so that it can serve as a
+ standardized representation format for a formal digital
+ library. Moreover, Mmt systematically separates logicdependent and
+ logicindependent concerns so that it can serve as an interface layer
+ between computation systems and MKM systems.",
+ paper = "Rabe13.pdf"
+}
+
+\end{chunk}
+
+\index{Rabe, Florian}
+\begin{chunk}{axiom.bib}
+@article{Rabe13a,
+ author = "Rabe, Florian",
+ title = {{The MMT API: A Generic MKM System}},
+ journal = "LNCS",
+ volume = "7961",
+ pages = "339343",
+ year = "2013",
+ abstract =
+ "The Mmt language has been developed as a scalable representation and
+ interchange language for formal mathematical knowledge. It permits
+ natural representations of the syntax and semantics of virtually all
+ declarative languages while making Mmtbased MKM services easy to
+ implement. It is foundationally unconstrained and can be instantiated
+ with specific formal languages.
+
+ The Mmt API implements the Mmt language along with multiple backends
+ for persistent storage and frontends for machine and user
+ access. Moreover, it implements a wide variety of Mmtbased knowledge
+ management services. The API and all services are generic and can be
+ applied to any language represented in Mmt. A plugin interface permits
+ injecting syntactic and semantic idiosyncrasies of individual formal
+ languages.",
+ paper = "Rabe13a.pdf"
+}
+
+\end{chunk}
+
+\index{Rabe, Florian}
+\begin{chunk}{axiom.bib}
+@article{Rabe16,
+ author = "Rabe, Florian",
+ title = {{The Future of Logic: FoundationIndependence}},
+ journal = "Logica Universalis",
+ volume = "10",
+ number = "1",
+ pages = "120",
+ year = "2016",
+ abstract =
+ "Throughout the twentieth century, the automation of formal logics in
+ computers has created unprecedented potential for practical
+ applications of logic—most prominently the mechanical verification of
+ mathematics and software. But the high cost of these applications
+ makes them infeasible but for a few flagship projects, and even those
+ are negligible compared to the everrising needs for verification. One
+ of the biggest challenges in the future of logic will be to enable
+ applications at much larger scales and simultaneously at much lower
+ costs. This will require a far more efficient allocation of
+ resources. Wherever possible, theoretical and practical results must
+ be formulated generically so that they can be instantiated to
+ arbitrary logics; this will allow reusing results in the face of
+ today’s multitude of applicationoriented and therefore diverging
+ logical systems. Moreover, the software engineering problems
+ concerning automation support must be decoupled from the theoretical
+ problems of designing logics and calculi; this will allow researchers
+ outside or at the fringe of logic to contribute scalable
+ logicindependent tools. Anticipating these needs, the author has
+ developed the Mmt framework. It offers a modern approach towards
+ defining, analyzing, implementing, and applying logics that focuses on
+ modular design and logicindependent results. This paper summarizes
+ the ideas behind and the results about Mmt. It focuses on showing how
+ Mmt. provides a theoretical and practical framework for the future of
+ logic.",
+ paper = "Rabe16.pdf",
+}
+
+\end{chunk}
+
+\index{Rabe, Florian}
+\begin{chunk}{axiom.bib}
+@article{Rabe17,
+ author = "Rabe, Florian",
+ title = {{How to Identify, Translate, and Combine Logics?}},
+ journal = "J. of Logic and Computation",
+ volume = "27",
+ number = "6",
+ pages = "17531798",
+ year = "2017",
+ abstract =
+ "We give general definitions of logical frameworks and
+ logics. Examples include the logical frameworks LF and Isabelle and
+ the logics represented in them. We apply this to give general
+ definitions for equivalence of logics, translation between logics and
+ combination of logics. We also establish general criteria for the
+ soundness and completeness of these. Our key messages are that the
+ syntax and proof systems of logics are theories; that both semantics
+ and translations are theory morphisms; and that combinations are
+ colimits. Our approach is based on the Mmt language, which lets us
+ combine formalist declarative representations (and thus the associated
+ tool support) with abstract categorical conceptualizations.",
+ paper = "Rabe17.pdf"
+}
+
+\end{chunk}
+
\index{Rabinowitz, P.}
\begin{chunk}{ignore}
\bibitem[Rabinowitz 70]{Rab70} Rabinowitz P.
diff git a/changelog b/changelog
index 95bee80..fa9d573 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20171215 tpd src/axiomwebsite/patches.html 20171215.01.tpd.patch
+20171215 tpd books/bookvolbib add references
20171206 tpd src/axiomwebsite/patches.html 20171206.01.tpd.patch
20171206 tpd books/bookvolbib add references
20171202 tpd src/axiomwebsite/patches.html 20171202.01.tpd.patch
diff git a/patch b/patch
index eaf8604..10aee34 100644
 a/patch
+++ b/patch
@@ 1,615 +1,365 @@
books/bookvolbib add references
Goal: Proving Axiom Correct  Coercion in CASProof Systesms
+Goal: Proving Axiom Correct
\index{Sozeau, Matthieu}
+\index{Girard, JeanYves}
+\index{Taylor, Paul}
+\index{Lafont, Yves}
\begin{chunk}{axiom.bib}
\incollection{Soze06,
 author = "Sozeau, Matthieu",
 title = {{Subset Coercions in Coq}},
 booktitle = "TYPES: Int. Workshop on Types for Proofs and Programs",
 journal = "LNCS",
 volume = "4502",
 pages = "237252",
 year = "2006",
 abstract =
 "We propose a new language for writing programs with dependent types
 on top of the Coq proof assistant. This language permits to establish
 a phase distinction between writing and proving algorithms in the Coq
 environment. Concretely, this means allowing to write algorithms as
 easily as in a practical functional programming language whilst giving
 them as rich a specification as desired and proving that the code
 meets the specification using the whole Coq proof apparatus. This is
 achieved by extending conversion to an equivalence which relates
 types and subsets based on them, a technique originating from the
 ``Predicate subtyping'' featureof PVS and following mathematical
 convention. The typing judgements can be translated to the Calculus of
 (Co)Inductive Constructions (Cic) by means of an interpretation
 which inserts coercions at the appropriate places.These coercions
 can contain existential variables representing the propositional
 parts of the final term, corresponding to proof obligations (or
 PVS typechecking conditions). A prototype implementation of this
 process is integrated with the Coq environment.",
 paper = "Soze06.pdf"
+@book{Gira03,
+ author = "Girard, JeanYves and Taylor, Paul and Lafont, Yves",
+ title = {{Proofs and Types}},
+ publisher = "Cambridge University Press",
+ link = "\url{http://www.paultaylor.eu/stable/prot.pdf}",
+ year = "2003"
}
\end{chunk}
\index{Pierce, Benjamin}
\begin{chunk}{axiom.bib}
@misc{Pier17,
 author = "Pierce, Benjamin",
 title = "DeepSpec Summer School, Coq Intensive, Part 1 (July 13,2017)",
 year = "2017",
 link = "\url{https://www.youtube.com/watch?v=jG61w5pOc2A}"
}

\end{chunk}
\index{Haftmann, Florian}
\index{Wenzel, Makarius}
+\index{Rabe,Florian}
+\index{Kohlhase, Michael}
\begin{chunk}{axiom.bib}
@article{Haft06,
 author = "Haftmann, Florian and Wenzel, Makarius",
 title = {{Constructive Type Classes in Isabelle}},
 journal = "LNCS",
 volume = "4502",
 year = "2006",
+@article{Rabe13,
+ author = "Rabe,Florian and Kohlhase, Michael",
+ title = {{A Scalable Module System}},
+ journal = "Information and Computation",
+ volume = "230",
+ pages = "154",
+ year = "2013",
abstract =
 "We reconsider the wellknown concept of Haskellstyle type classes
 within the logical framework of Isabelle. So far, axiomatic type
 classes in Isabelle merely account for the logical aspect as
 predicates over types, while the opera tional part is only a
 convention based on raw overloading. Our more elaborate approach to
 constructive type classes provides a seamless integration with
 Isabelle locales, which are able to manage both operations and logical
 properties uniformly. Thus we combine the convenience of type
 classes and the flexibility of locales. Furthermore, we construct
 dictionary terms derived from notions of the type system. This
 additional internal structure provides satisfactory foundations of
 type classes, and supports further applications, such as code
 generation and export of theories and theorems to environments without
 type classes.",
 paper = "Haft06.pdf"
+ "Symbolic and logic computation systems ranging from computer algebra
+ systems to theorem provers are finding their way into science,
+ technology, mathematics and engineering. But such systems rely on
+ explicitly or implicitly represented mathematical knowledge that needs
+ to be managed to use such systems effectively.
+
+ While mathematical knowledge management (MKM) ``in the small'' is
+ wellstudied, scaling up to large, highly interconnected corpora
+ remains difficult. We hold that in order to realize MKM “in the
+ large”, we need representation languages and software architectures
+ that are designed systematically with largescale processing in mind.
+
+ Therefore, we have designed and implemented the Mmt language – a
+ module system for mathematical theories. Mmt is designed as the
+ simplest possible language that combines a module system, a
+ foundationally uncommitted formal semantics, and webscalable
+ implementations. Due to a careful choice of representational
+ primitives, Mmt allows us to integrate existing representation
+ languages for formal mathematical knowledge in a simple, scalable
+ formalism. In particular, Mmt abstracts from the underlying
+ mathematical and logical foundations so that it can serve as a
+ standardized representation format for a formal digital
+ library. Moreover, Mmt systematically separates logicdependent and
+ logicindependent concerns so that it can serve as an interface layer
+ between computation systems and MKM systems.",
+ paper = "Rabe13.pdf"
}
\end{chunk}
\index{Kiessling, Robert}
\index{Luo, Zhaohui}
+\index{Rabe, Florian}
\begin{chunk}{axiom.bib}
@article{Kies03,
 author = "Kiessling, Robert and Luo, Zhaohui",
 title = {{Coercions in HindleyMilner Systems}},
+@article{Rabe13a,
+ author = "Rabe, Florian",
+ title = {{The MMT API: A Generic MKM System}},
journal = "LNCS",
 volume = "3085",
 year = "2003",
 abstract =
 "Coercive subtyping is a theory of abbreviation for dependent type
 theories. In this paper, we incorporate the idea of coercive subtyping
 into the traditional HindleyMilner type systems in functional
 programming languages. This results in a typing system with coercions,
 an extension of the HindleyMilner type system. A type inference
 algorithm is developed and shown to be sound and complete with respect
 to the typing system. A notion of derivational coherence is developed
 to deal with the problem of ambiguity and the corresponding type
 inference algorithm is shown to be sound and complete.",
 paper = "Kies03.pdf"
}

\end{chunk}

\index{Wiedijk, Freek}
\begin{chunk}{axiom.bib}
@article{Wied03,
 author = "Wiedijk, Freek",
 title = {{Formal Proof Sketches}},
 journal = "LNCS",
 volume = "3085",
 year = "2003",
 pages = "378393",
 abstract =
 "Formalized mathematics currently does not look much like informal
 mathematics. Also, formalizing mathematics currently seems far too
 much work to be worth the time of the working mathematician. To
 address both of these problems we introduce the notion of a formal
 proof sketch . This is a proof representation that is in between a
 fully checkable formal proof and a statement without any proof at
 all. Although a formal proof sketch is too high level to be checkable
 by computer, it has a precise notion of correctness (hence the
 adjective formal ). We will show through examples that formal proof
 sketches can closely mimic already existing mathematical
 proofs. Therefore, although a formal proof sketch contains gaps in
 the reasoning from a formal point of view (which is why we call it a
 sketch ), a mathematician probably would call such a text just a
 ‘proof’.",
 paper = "Wied03.pdf"
}

\end{chunk}

\index{Coquand, Thierry}
\index{Persson, Henrik}
\begin{chunk}{axiom.bib}
@article{Coqu98,
 author = "Coquand, Thierry and Persson, Henrik",
 title = {{Groebner Bases in Type Theory}},
 journal = "LNCS",
 volume = "1657",
 year = "1998",
 pages = "3346",
+ volume = "7961",
+ pages = "339343",
+ year = "2013",
abstract =
 "We describe how the theory of Groebner bases, an important part
 of computational algebra, can be developed within Martin Lof’s
 type theory. In particular, we aim for an integrated development
 of the algorithms for computing Groebner bases: we want to prove,
 constructively in type theory, the existence of Groebner bases and
 from such proofs extract the algorithms. Our main contribution is
 a reformulation of the standard theory of Groebner bases which
 uses generalised inductive definitions. We isolate the main
 non–constructive part, a minimal bad sequence argument, and use
 the open induction principle [Rao88,Coq92] to interpret it by
 induction. This leads to short constructive proofs of Dickson’s
 lemma and Hilbert’s basis theorem, which are used to give an
 integrated development of Buchberger’s algorithm. An important
 point of this work is that the elegance and brevity of the
 original proofs are maintained while the new proofs also have a
 direct constructive content. In the appendix we present a
 computer formalisation of Dickson’s lemma and an abstract
 existence proof of Groebner bases.",
 paper = "Coqu98.pdf"
}

\end{chunk}

\index{Filliatre, JeanChristophe}
\begin{chunk}{axiom.bib}
@article{Fill98,
 author = "Filliatre, JeanChristophe",
 title = {{Proof of Imperative Programs in Type Theory}},
 journal = "LNCS",
 volume = "1657",
 year = "1998",
 pages = "7892",
 abstract =
 "We present a new approach to certifying functional programs with
 imperative aspects, in the context of Type Theory. The key is a
 functional translation of imperative programs, based on a combination
 of the type and effect discipline and monads. Then an incomplete proof
 of the specification is built in the Type Theory, whose gaps would
 corre spond to proof obligations. On sequential imperative programs,
 we get the same proof obligations as those given by FloydHoare
 logic. Compared to the latter, our approach also includes functional
 constructions in a straightforward way. This work has been
 implemented in the Coq Proof Assistant and applied on nontrivial
 examples.",
 paper = "Fill98.pdf"
+ "The Mmt language has been developed as a scalable representation and
+ interchange language for formal mathematical knowledge. It permits
+ natural representations of the syntax and semantics of virtually all
+ declarative languages while making Mmtbased MKM services easy to
+ implement. It is foundationally unconstrained and can be instantiated
+ with specific formal languages.
+
+ The Mmt API implements the Mmt language along with multiple backends
+ for persistent storage and frontends for machine and user
+ access. Moreover, it implements a wide variety of Mmtbased knowledge
+ management services. The API and all services are generic and can be
+ applied to any language represented in Mmt. A plugin interface permits
+ injecting syntactic and semantic idiosyncrasies of individual formal
+ languages.",
+ paper = "Rabe13a.pdf"
}
\end{chunk}
\index{Nipkow, Tobias}
+\index{Kohlhase, Michael}
+\index{Rabe, Florian}
\begin{chunk}{axiom.bib}
@article{Nipk02,
 author = "Nipkow, Tobias",
 title = {{Structured Proofs in Isar/HOL}},
 journal = "LNCS",
 volume = "2646",
 year = "2002",
 pages = "259278",
+@article{Kohl16,
+ author = "Kohlhase, Michael and Rabe, Florian",
+ title = {{QED Reloaded: Towards a Pluralistic Formal Library of
+ Mathematical Knowledge}},
+ journal = "Journal of Formalized Reasoning",
+ volume = "9",
+ number = "1",
+ pages = "201234",
+ year = "2016",
abstract =
 "Isar is an extension of the theorem prover Isabelle with a language
 for writing humanreadable structured proofs. This paper is an
 introduction to the basic constructs of this language.",
 paper = "Nipk02.pdf"
+ "Proposed in 1994, the ``QED project'' was one of the seminally
+ inflnuential initiatives in automated reasoning: It envisioned the
+ formalization of ``all of mathematics'' and the assembly of these
+ formalizations in a single coherent database. Even though it never led
+ to the concrete system, communal resource, or even joint research
+ envisioned in the QED manifesto, the idea lives on and shapes the
+ research agendas of a significant part of the community This paper
+ surveys a decade of work on representation languages and knowledge
+ management tools for mathematical knowledge conducted in the KWARC
+ research group at Jacobs University Bremen. It assembles the various
+ research strands into a coherent agenda for realizing the QED dream
+ with modern insights and technologies.",
+ paper = "Kohl16.pdf"
}
\end{chunk}
\index{Carlstrom, Jesper}
+\index{Rabe, Florian}
\begin{chunk}{axiom.bib}
@article{Carl02,
 author = "Carlstrom, Jesper",
 title = {{Subsets, Quotients, and Partial Functions in MartinL\"of's
 Type Theory}},
 journal = "LNCS",
 volume = "2646",
 year = "2002",
 pages = "7894",
+@article{Rabe16,
+ author = "Rabe, Florian",
+ title = {{The Future of Logic: FoundationIndependence}},
+ journal = "Logica Universalis",
+ volume = "10",
+ number = "1",
+ pages = "120",
+ year = "2016",
abstract =
 "We treat subsets, equivalence relations, and partial functions,
 with subsets as propositional functions .In order for these three
 notions to work well together, we propose some changes to the theory
 of subsets as propositional functions .The method used is not to make
 any changes to the type theory itself, but to view the new concepts as
 defined ones.",
 paper = "Carl02.pdf"
+ "Throughout the twentieth century, the automation of formal logics in
+ computers has created unprecedented potential for practical
+ applications of logic—most prominently the mechanical verification of
+ mathematics and software. But the high cost of these applications
+ makes them infeasible but for a few flagship projects, and even those
+ are negligible compared to the everrising needs for verification. One
+ of the biggest challenges in the future of logic will be to enable
+ applications at much larger scales and simultaneously at much lower
+ costs. This will require a far more efficient allocation of
+ resources. Wherever possible, theoretical and practical results must
+ be formulated generically so that they can be instantiated to
+ arbitrary logics; this will allow reusing results in the face of
+ today’s multitude of applicationoriented and therefore diverging
+ logical systems. Moreover, the software engineering problems
+ concerning automation support must be decoupled from the theoretical
+ problems of designing logics and calculi; this will allow researchers
+ outside or at the fringe of logic to contribute scalable
+ logicindependent tools. Anticipating these needs, the author has
+ developed the Mmt framework. It offers a modern approach towards
+ defining, analyzing, implementing, and applying logics that focuses on
+ modular design and logicindependent results. This paper summarizes
+ the ideas behind and the results about Mmt. It focuses on showing how
+ Mmt. provides a theoretical and practical framework for the future of
+ logic.",
+ paper = "Rabe16.pdf",
}
\end{chunk}
\index{Bove, Ana}
+\index{Rabe, Florian}
\begin{chunk}{axiom.bib}
@article{Bove02,
 author = "Bove, Ana",
 title = {{General Recursion in Type Theory}},
 journal = "LNCS",
 volume = "2646",
 pages = "3958",
 abstract =
 "In this work, a method to formalise general recursive algorithms in
 constructive type theory is presented throughout examples. The method
 separates the computational and logical parts of the definitions. As
 a consequence, the resulting typetheoretic algorithms are clear,
 compact and easy to understand. They are as simple as their
 equivalents in a functional programming language, where there is no
 restriction on recursive calls. Given a general recursive algorithm,
 the method consists in defining an inductive specialpurpose
 accessibility predicate that characterises the inputs on which the
 algorithm terminates. The typetheoretic version of the algorithm can
 then be defined by structural recursion on the proof that the input
 values satisfy this predicate. When formalising nested algorithms, the
 specialpurpose accessibility predicate and the typetheoretic version
 of the algorithm must be defined simultaneously because they depend on
 each other. Since the method separates the computational part from
 the logical part of a definition, formalising partial functions
 becomes also possible.",
 paper = "Bove02.pdf"
}

\end{chunk}

\index{Coen, Claudio Sacerdoti}
\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@article{Coen07,
 author = "Coen, Claudio Sacerdoti and Tassi, Enrico",
 title = {{Working with Mathematical Structures in Type Theory}},
 journal = "LNCS",
 volume = "4941",
 year = "2007",
 pages = "157172",
+@article{Rabe17,
+ author = "Rabe, Florian",
+ title = {{How to Identify, Translate, and Combine Logics?}},
+ journal = "J. of Logic and Computation",
+ volume = "27",
+ number = "6",
+ pages = "17531798",
+ year = "2017",
abstract =
 "We address the problem of representing mathematical structures in a
 proof assistant which: 1) is based on a type theory with depen dent
 types, telescopes and a computational version of Leibniz equality; 2)
 implements coercive subtyping, accepting multiple coherent paths
 between type families; 3) implements a restricted form of higher order
 unification and type reconstruction. We show how to exploit the
 previous quite common features to reduce the ``syntactic'' gap between
 pen and paper and formalised algebra. However, to reach our goal we need
 to propose unification and type reconstruction heuristics that are
 slightly different from the ones usually implemented. We have
 implemented them in Matita.",
 paper = "Coen07.pdf"
+ "We give general definitions of logical frameworks and
+ logics. Examples include the logical frameworks LF and Isabelle and
+ the logics represented in them. We apply this to give general
+ definitions for equivalence of logics, translation between logics and
+ combination of logics. We also establish general criteria for the
+ soundness and completeness of these. Our key messages are that the
+ syntax and proof systems of logics are theories; that both semantics
+ and translations are theory morphisms; and that combinations are
+ colimits. Our approach is based on the Mmt language, which lets us
+ combine formalist declarative representations (and thus the associated
+ tool support) with abstract categorical conceptualizations.",
+ paper = "Rabe17.pdf"
}
\end{chunk}
\index{Coquand, Thierry}
+\index{Halleck, John}
\begin{chunk}{axiom.bib}
@article{Coqu93,
 author = "Coquand, Thierry",
 title = {{Infinite Objects in Type Theory}},
 journal = "LNCS",
 volume = "806",
 year = "1993",
 pages = "6278",
 abstract =
 "We show that infinite objects can be constructively understood
 without the consideration of partial elements, or greatest fixed
 points, through the explicit consideration of proof objects. We
 present then a proof system based on these explanations. According to
 this analysis, the proof expressions should have the same structure
 as the program expressions of a pure functional lazy language:
 variable, constructor, application, abstraction, case expressions,
 and local let expressions.",
 paper = "Coqu93.pdf"
+@misc{Hall17,
+ author = "Halleck, John",
+ title = {{Logic System Interrelationships}},
+ year = "2017",
+ link = "\url{http://www.cc.utah.edu/~nahaj/logic/structures/index.html}"
}
\end{chunk}
\index{Barthe, Gilles}
+\index{Yang, Xiang}
+\index{Mittal, Rajat}
\begin{chunk}{axiom.bib}
@article{Bart95,
 author = "Barthe, Gilles",
 title = {{Implicit Coercions in Type Systems}},
 journal = "LNCS",
 volume = "1158",
 year = "1995",
 pages = "115",
 abstract =
 "We propose a notion of pure type system with implicit coercions. In
 our framework, judgements are extended with a context of coercions Δ
 and the application rule is modified so as to allow coercions to be
 left implicit. The setting supports multiple inheritance and can be
 applied to all type theories with $\Pi$types. One originality of our work
 is to propose a computational interpretation for implicit
 coercions. In this paper, we demonstrate how this interpretation
 allows a strict control on the logical properties of pure type systems
 with implicit coecions.",
 paper = "Bart95.pdf"
+@misc{Yang14,
+ author ="Yang, Xiang and Mittal, Rajat",
+ title = {{Acceleration of the Jacobi iterative method by factors exceeding
+ 100 using scheduled relation}},
+ link = "\url{http://engineering.jhu.edu/fsag/wpcontent/uploads/sites/23/2013/10/JCP_revised_WebPost.pdf}",
+ paper = "Yang14.pdf"
}
\end{chunk}
\index{Berger, U.}
\index{Schwichtenberg, H.}
+\index{Geller, Murray}
+\index{Ng, Edward W.}
\begin{chunk}{axiom.bib}
@article{Berg95,
 author = "Berger, U. and Schwichtenberg, H.",
 title = {{The Greatest Common Divisor: A Case Study for Program
 Extraction from Classical Proofs}},
 journal = "LNCS",
 volume = "1158",
 year = "1995",
 pages = "3646",
 paper = "Berg95.pdf"
+@misc{Gell69,
+ author = "Geller, Murray and Ng, Edward W.",
+ title = {{A Table of Integrals of the Exponential Integral}},
+ link =
+ "\url{http://nvlpubs.nist.gov/nistpubs/jres/73B/jresv73Bn3p191_A1b.pdf}",
+ abstract = "
+ This is a compendium of indefinite and definite integrals of products
+ of the Exponential Integral with elementary or transcendental functions.",
+ paper = "Gell69.pdf"
}
\end{chunk}
\index{Magaud, Nicolas}
\index{Bertot, Yves}
+\index{Piroi, Florina}
+\index{Kutsiz, Temur}
\begin{chunk}{axiom.bib}
@article{Maga00,
 author = "Magaud, Nicolas and Bertot, Yves",
 title = {{Changing Data Structures in Type Theory: A Study of
 Natural Numbers}},
 journal = "LNCS",
 volume = "2277",
 pages = "181196",
 year = "2000",
+@article{Piro05,
+ author = "Piroi, Florina and Kutsiz, Temur",
+ title = {{The Theorema Environment for Interactive Proof Development}},
+ journal = "LNAI",
+ volume = "3835",
+ pages = "261275",
+ year = "2005",
abstract =
 "In typetheory based proof systems that provide inductive
 structures, computation tools are automatically associated to
 inductive definitions. Choosing a particular representation for a
 given concept has a strong influence on proof structure. We
 propose a method to make the change from one representation to
 another easier, by systematically translating proofs from one
 context to another. We show how this method works by using it on
 natural numbers, for which a unary representation (based on Peano
 axioms) and abinary representation are available. This method
 leads to an automatic translation tool that we have implemented in
 Coq and successfully applied to several arithmetical theorems.",
 paper = "Maga00.pdf"
+ "We describe an environment that allows the users of the Theorema
+ system to flexibly control aspects of computersupported proof
+ development. The environment supports the display and manipulation of
+ proof trees and proof situations, logs the user activities (commands
+ communicated with the system during the proving session), and presents
+ (also unfinished) proofs in a humanoriented style. In particular, the
+ user can navigate through the proof object, expand/remove proof
+ branches, provide witness terms, develop several proofs concurrently,
+ proceed step by step or automatically and so on. The environment
+ enhances the effectiveness and flexibility of the reasoners of the
+ Theorema system.",
+ paper = "Piro05.pdf"
}
\end{chunk}
\index{Bailey, Anthony}
+\index{Priest, Graham}
\begin{chunk}{axiom.bib}
@article{Bail96,
 author = "Bailey, Anthony",
 title = {{Coercion Synthesis in Computer Implementations of
 TypeTheoretic Frameworks}},
 journal = "LNCS",
 year = "1996",
 pages = "927",
 abstract =
 "A coercion is a function that acts on a representation of some object
 in order to alter its type. The idea is that although applying a
 coercion to an object changes its type, the result still represents
 the ``same'' abject in some sense; perhaps it is some essential
 underlying part of the original object, or a different representation
 of that object. This paper examines some of the issues involved in
 the computer implementation of systems that allow a user to define
 coercions that may then be left implicit in the syntax of expressions
 and synthesised automatically. From a typetheoretic perspective,
 coercions are often left implicit in mathematical texts, so they can
 be used to improve the readability of a formalisation, and to
 implement other tricks of syntax if so desired.",
 paper = "Bail96.pdf"
+@book{Prie12,
+ author = "Priest, Graham",
+ title = {{An Introduction to NonClassical Logic}},
+ year = "2012",
+ publisher = "Cambridge University Press"
}
\end{chunk}
\index{Barras, Bruno}
+\index{Beeson, Michael J.}
\begin{chunk}{axiom.bib}
@article{Barr96,
 author = "Barras, Bruno",
 title = {{Verification of the Interface of a Small Proof System in Coq}},
 journal = "LNCS",
 volume = "1512",
 pages = "2845",
 year = "1996",
 abstract =
 "This article describes the formalization of the interface of a
 proofchecker. The latter is based on a kernel consisting of
 typechecking functions for the Calculus of Constructions, but it
 seems the ideas can generalize to other type systems, as fax as they
 axe based on the proofs asterms principle. We suppose that the
 metatheory of the corresponding type system is proved (up to type
 decidability). We specify and certify the toplevel loop, the system
 invariant, and the error messages.",
 paper = "Barr96.pdf"
+@article{Bees90,
+ author = "Beeson, Michael J.",
+ title = {{Review of Implementing Mathematics with the Nuprl Proof
+ Development System}},
+ journal = "J. of Symbolic Logic",
+ volume = "55",
+ number = "3",
+ pages = "12991302",
+ year = "1990",
+ link = "\url{http://www.jstor.org/stable/2274489}",
+ paper = "Bees90.pdf"
}
\end{chunk}
\index{Dowek, Gilles}
+\index{Beeson, Michael J.}
\begin{chunk}{axiom.bib}
@article{Dowe96,
 author = "Dowek, Gilles",
 title = {{A TypeFree Formalization of Mathematics Where Proofs are
 Objects}},
 journal = "LNCS",
 volume = "1512",
 year = "1996",
 pages = "88111",
 abstract =
 "We present a firstorder typefree axiomatization of mathematics
 where proofs are objects in the sense of HeytingKolmogorov functional
 interpretation. The consistency of this theory is open.",
 paper = "Dowe96.pdf"
+#InCollection{Bees89,
+ author = "Beeson, Michael J.",
+ title = {{Logic and Computation in MATHPERT: An Expert System for
+ Learning Mathematics}},
+ booktitle = "Computers and Mathematics",
+ publisher = "SpringerVerlag",
+ year = "1989",
+ pages = "299307",
+ isbn = "0387970193"
}
\end{chunk}
\index{Harrison, John}
\begin{chunk}{axiom.bib}
@article{Harr06,
+@misc{Harr06a,
author = "Harrison, John",
 title = {{Proof Style}},
 journal = "LNCS",
 volume = "1512",
+ title = {{Formal Verification of Floatingpoint Arithmetic at Intel}},
year = "2006",
 pages = "154172",
 abstract =
 "We are concerned with how computer theorem provers should expect
 users to communicate proofs to them. There are many stylistic choices
 that still allow the machine to generate a completely formal proof
 object. The most obvious choice is the amount of guidance required
 from the user, or from the machine perspective, the degree of
 automation provided. But another important consideration, which we
 consider particularly significant, is the bias towards a
 'procedural' or 'declarative' proof style. We will explore this
 choice in depth, and discuss the strengths and weaknesses of
 declarative and procedural styles for proofs in pure mathematics and
 for verification applications. We conclude with a brief summary of
 our own experiments in trying to combine both approaches.",
 paper = "Harr06.pdf"
}

\end{chunk}

\index{Jones, Alex}
\index{Luo, Zhaohui}
\index{Soloviev, Sergei}
\begin{chunk}{axiom.bib}
@article{Jone96,
 author = "Jones, Alex and Luo, Zhaohui and Soloviev, Sergei",
 title = {{Some Algorithmic and ProofTheoretical Aspects of
 Coercive Subtyping}},
 journal = "LNCS",
 volume = "1512",
 year = "1996",
 pages = "173195",
 abstract =
 "Coercive subtyping offers a conceptually simple but powerful
 framework to understand subtyping and subset relationships in type
 theory. In this paper we study some of its prooftheoretic and
 computational properties.",
 paper = "Jone96.pdf"
+ link = "\url{http://www.cl.cam.ac.uk/~jrh13/slides/jnao02jun06/slides.pdf}",
+ paper = "Harr06a.pdf"
}
\end{chunk}
\index{Naraschewski, Wolfgang}
\index{Nipkow, Tobias}
+\index{Beeson, Michael}
\begin{chunk}{axiom.bib}
@article{Nara99,
 author = "Naraschewski, Wolfgang and Nipkow, Tobias",
 title = {{Type Inference Verified: Algorithm W in Isabelle/HOL}},
+@article{Bees89a,
+ author = "Beeson, Michael",
+ title = {{Some Applications of Gentzen's Proof Theory in Automated
+ Deduction}},
journal = "LNCS",
 volume = "1512",
 year = "1999",
 pages = "317332",
 paper = "Nara99.pdf"
}

\end{chunk}

\index{Constable, R.L.}
\index{Knoblock, T.B.}
\index{Gates, J.L.}
\begin{chunk}{axiom.bib}
@article{Cons85a,
 author = "Constable, R.L. and Knoblock, T.B. and Gates, J.L.",
 title = {{Writing Programs that Construct Proofs}},
 journal = "J. of Automated Reasoning",
 volume = "1",
 number = "3",
 pages = "285326",
 year = "1985",
+ volume = "475",
+ pages = "101156",
+ year = "1989",
abstract =
 "When we learn mathematics, we learn more than definitions and
 theorems. We learn techniques of proof. In this paper, we describe
 a particular way to express these techniques and incorporate them
 into formal theories and into computer systems used to build such
 theories. We illustrate the methods as they were applied in the
 $\lambda$PRL system, essentially using the ML programming
 language from Edinburgh LCF [23] as the formalised
 metalanguage. We report our experience with such an approach
 emphasizing the ideas that go beyond the LCF work, such as
 transformation tactics and special purpose reasoners. We also show
 how the validity of tactics can be guaranteed. The introduction
 places the work in historical context and the conclusion briefly
 describes plans to carry the methods further. The majority of the
 paper presents the $\lambda$PRL approach in detail.",
 paper = "Cons85a.pdf"
+ "We show that Prolog is intimately connected with Gentzen's cutfree
+ sequent calculus G, analyzing Prolog computations as the construction
+ of certain cutfree derivations. We introduce a theoremproving
+ program GENTZEN based on Gentzen's sequent calculus, which
+ incorporates some features of Prolog's computation procedure. We show
+ that GENTZEN has the following properties: (1) It is
+ (nondeterministically) sound and complete for firstorder
+ intuitionistic predicate calculus; (2) Its successful computations
+ coincide with those of Prolog on the Horn clause fragment (both
+ deterministically and nondeterministically). The proofs of (1) and
+ (2) contain a new proof of the completeness of (nondeterministic)
+ Prolog for Horn clause logic, based on our analysis of Prolog in terms
+ of Gentzen sequents instead of on resolution. GENTZEN has been
+ implemented and tested on examples including some proofs by induction
+ in number theory, an example constructed by J. McCarthy to show the
+ limitations of Prolog, and ``Schubert's Steamroller.'' An extension of
+ GENTZEN also provides a decision procedure for intuitionistic
+ propositional calculus (but at some cost in efficiency).",
+ paper = "Bees89a.pdf"
}
\end{chunk}
\index{Trybulec, Zinaida}
\index{Swieczkowska, Halina}
\begin{chunk}{axiom.bib}
@article{Tryb92,
 author = "Trybulec, Zinaida and Swieczkowska, Halina",
 title = {{Some Remarks on The Language of Mathematical Texts}},
 journal = "Studies in Logic, Grammar and Rhetoric",
 volume = "10/11",
 pages = "103124",
 year = "1992",
 paper = "Tryb92.pdf"
}

\end{chunk}

\index{Traytel, Bmytro}
+\index{Restall, Greg}
\begin{chunk}{axiom.bib}
@misc{Tray10,
 author = "Traytel, Bmytro",
 title = {{Extensions of a Type Inference Algorithm with Coerce Subtyping}},
 school = "Der Technischen Universitat Munchen",
 year = "2010",
 abstract =
 "Subtyping with coercion semantics allows a type inference system to
 correct some illtyped programs by the automatic insertion of
 implicit type conversions at runtime. This simplifies programmer’s
 life but has its price: the general typability problem for given base
 type subtype dependencies is NPcomplete. Nevertheless, if the given
 coercions define an order on types with certain properties, the
 problem behaves in a sane way in terms of complexity. This thesis
 presents an algorithm that can be used to extend HindleyMilner type
 inference with coercive subtyping assuming a given partial order on
 base types. Especially, we discuss restrictions on the subtype
 dependencies that are necessary to achieve an efficient
 implementation. Examples of problems that occur if these restrictions
 are not met are given. The result of these considerations is that the
 algorithm is complete if the given base type poset is a disjoint union
 of lattices. Furthermore, the interaction of subtyping with type
 classes is addressed. The algorithm that is extended to deal with
 type classes requires even a stronger restriction to assure
 completeness. An MLimplementation of the presented algorithm is used
 in the generic proof assistant Isabelle.",
 paper = "Tray10.pdf"
+@book{Rest00,
+ author = "Restall, Greg",
+ title = {{An Introduction to Substructural Logics}},
+ year = "2000",
+ publisher = "Routledge",
+ isbn = "041521534X"
}
\end{chunk}
\index{Luo, Zhaohui}
\index{Soloviev, Sergei}
+\index{Font, Josep Marie}
\begin{chunk}{axiom.bib}
@article{Luox99,
 author = "Luo, Zhaohui and Soloviev, Sergei",
 title = {{Dependent Coercions}},
 journal = "Electr. Notes Theor. Comput. Sci.",
 volume = "29",
 year = "1999",
 pages = "152168",
 abstract =
 "A notion of dependent coercion is introduced and studied in the
 context of depen dent type theories. It extends our earlier work on
 coercive subtyping into a uniform framework which increases the
 expressive power with new applications. A dependent coercion
 introduces a subtyping relation between a type and a family of types
 in that an object of the type is mapped into one of the types in the
 family. We present the formal framework, discuss its metatheory, and
 consider applications such as its use in functional programming with
 dependent types.",
 paper = "Luox99.pdf"
+@book{Font16,
+ author = "Font, Josep Marie",
+ title = {{Abstract Algebraic Logic: An Introductory Textbook}},
+ year = "2016",
+ publisher = "College Publications, Kings College",
+ isbn = "9781848902077"
}
\end{chunk}
+\end{chunk}
\ No newline at end of file
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 54ebd7c..bff9781 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5864,6 +5864,8 @@ books/bookvolbib add references
books/bookvolbib add references
20171206.01.tpd.patch
books/bookvolbib add references
+20171215.01.tpd.patch
+books/bookvolbib add references

1.9.1