From 3e35e31c9d1e85733fcc97bf5879c898e31c2e5c Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Thu, 16 Nov 2017 06:30:06 0500
Subject: [PATCH] books/bookvolbib add references
MIMEVersion: 1.0
ContentType: text/plain; charset=UTF8
ContentTransferEncoding: 8bit
Goal: Proving Axiom Correct
\index{Brown, W.S.}
\begin{chunk}{axiom.bib}
@article{Brow69,
author = "Brown, W.S.",
title = {{Rational Exponential Expressions and a Conjecture Concerning
$\pi$ and $e$}},
journal = "The American Mathematical Monthly",
volume = "76",
number = "1",
year = "1969",
pages = "2834",
abstract =
"One of the most controversial and least well defined of mathematical
problems is the problem of simplification. The recent upsurge
of interest in mechanized mathematics has lent new urgency to this
problem, but so far very little has been accomplished. This paper
attempts to shed light on the situation by introducing the class of
rational exponential expressions, defining simplification within
this class, and showing constructively how to achieve it. It is shown
that the only simplified rational exponential expression equivalent to
0 is 0 itself, provided that an easily stated conjecture is true.
However the conjecture, if true, will surely be difficult to prove,
since it asserts as a special case that $\pi$ and $e$ are algebraically
independent, and no one has yet been able to prove even the much
weaker conjecture that $\pi+e$ is irrational.",
paper = "Brow69.pdf"
}
\end{chunk}
\index{Bogen, Richard}
\begin{chunk}{axiom.bib}
@book{Boge77,
author = "Bogen, Richard",
title = {{MACSYMA Reference Manual, Version 9}},
publisher = "MIT",
year = "1977",
link = "\url{http://bitsavers.informatik.unistuttgart.de/pdf/mit/macsyma/MACSYMA_RefMan_V9_Dec77.pdf}",
paper = "Boge77.pdf"
}
\end{chunk}
\index{Schelter, William F.}
\begin{chunk}{axiom.bib}
@book{Sche01,
author = "Schelter, William F.",
title = {{Maxima Manual Version 5.41.0}},
year = "2001",
publisher = "Sourceforge",
paper = "Sche01.pdf"
}
\end{chunk}
\index{Farmer, William M.}
\index{Guttman, J.D.}
\index{Thayer, F.J.}
\begin{chunk}{axiom.bib}
@article{Farm95,
author = "Farmer, William M. and Guttman, J.D. and Thayer, F.J.",
title = {{Contexts in Mathematical Reasoning and Computation}},
journal = "J. of Symbolic Computation",
volume = "19",
pages = "201216",
year = "1995",
abstract =
"Contexts are sets of formulas used to manage the assumptions that
arise in the course of a mathematical deduction or
calculation. Although contextdependent reasoning is commonplace in
informal mathematics, most contemporary symbolic computation systems
do not utilize contexts in sophisticated ways. This paper describes
some contextbased techniques for symbolic computation, including
techniques for reasoning about definedness, simplifying abstract
algebraic expressions, and computing with theorems. All of these
techniques are implemented in the IMPS Interactive Mathematical Proof
System. The paper also proposes a general mathematics laboratory that
combines the functionality of current symbolic computation systems
with the facilities of a theorem proving system like IMPS.",
paper = "Farm95.pdf"
}
\end{chunk}
\index{Farmer, William M.}
\begin{chunk}{axiom.bib}
@article{Farm93b,
author = "Farmer, William M.",
title = {{A simple type theory with partial functions and subtypes}},
journal = "Annals of Pure and Applied Logic",
volume = "64",
pages = "211240",
year = "1993",
abstract =
"Simple type theory is a higherorder predicate logic for reasoning
about truth values, individuals, and simply typed total functions. We
present in this paper a version of simple type theory, called PF*, in
which functions may be partial and types may have subtypes. We define
both a Henkinstyle general models semantics and an axiomatic system
for PF*, and we prove that the axiomatic system is complete with
respect to the general models semantics. We also define a notion of
an interpretation of one PF* theory in another. PF* is intended as a
foundation for mechanized mathematics. It is the basis for the logic
of IMPS, an Interactive Mathematical Proof System developed at The
MITRE Corporation.",
paper = "Farm93b.pdf"
}
\end{chunk}
\index{Farmer, William H.}
\begin{chunk}{axiom.bib}
@article{Farm92,
author = "Farmer, William H.",
title = {{Little Theories}},
journal = "LNCS",
volume = "607",
year = "1992",
pages = "567581",
abstract =
"In the ``little theories'' version of the axiomatic method, different
portions of mathematics are developed in various different formal
axiomatic theories. Axiomatic theories may be related by inclusion or
by theory interpretation. We argue that the little theories approach
is a desirable way to formalize mathematics, and we describe how IMPS,
an Interactive Mathematical Proof System, supports it.",
paper = "Farm92.pdf"
}
\end{chunk}
\index{Owre, S.}
\index{Rushby, J.M.}
\index{Shankar, N.}
\begin{chunk}{axiom.bib}
@article{Owre92,
author = "Owre, S. and Rushby, J.M. and Shankar, N.",
title = {{PVS: A Prototype Verification System}},
journal = "Lecture Notes in Computer Science",
volume = "687",
pages = "748752",
year = "1992",
abstract =
"This brief paper introduces the main ideas of PVS",
paper = "Owre92.pdf"
}
\end{chunk}
\index{Farmer, William H.}
\begin{chunk}{axiom.bib}
@article{Farm92a,
author = "Farmer, William H.",
title = {{IMPS: System Description}},
journal = "Lecture Notes in Computer Science",
volume = "607",
pages = "701705",
year = "1992",
paper = "Farm92a.pdf"
}
\end{chunk}
\index{Wos, Larry}
\begin{chunk}{axiom.bib}
@article{Wosx92,
author = "Wos, Larry",
title = {{The Impossibility of the Automation of Logical Reasoning}},
journal = "Lecture Notes in Computer Science",
volume = "607",
year = "1992",
pages = "13",
paper = "Wosx92.pdf"
}
\end{chunk}
\index{Craigen, Dan}
\index{Kromodimoeljo, Sentot}
\index{Meisels, Irwin}
\index{Pase, Bill}
\index{Saaltink, Mark}
\begin{chunk}{axiom.bib}
@article{Crai92,
author = "Craigen, Dan and Kromodimoeljo, Sentot and Meisels, Irwin
and Pase, Bill",
title = {{Eves System Description}},
journal = "Lecture Notes in Computer Science",
volume = "607"
pages = "771775",
year = "1992",
paper = "Crai92.pdf"
}
\end{chunk}
\index{Pfenning, Frank}
\index{Rohwedder, Ekkehard}
\begin{chunk}{axiom.bib}
@article{Pfen92b,
author = "Pfenning, Frank and Rohwedder, Ekkehard",
title = {{Implementing the MetaTheory of Deductive Systems}},
journal = "Lecture Notes in Computer Science",
volume = "607"
pages = "771775",
year = "1992",
abstract =
"We exhibit a methodology for formulating and verifying meta theorems
about deductive systems in the Elf language, an implementation of the
LF Logical Framework with an operational semantics in the spirit of
logic programming. It is based on the mechanical verification of
properties of transformations between deductions, which relies on type
reconstruction and schemachecking. The latter is justified by
induction principles for closed LF objects, which can be constructed
over a given signature. We illustrate our technique through several
examples, the most extensive of which is an interpre tation of
classical logic in minimal logic through a continuationpassingstyle
transformation on proofs.",
paper = "Pfen92b.pdf"
}
\end{chunk}
\index{Guttman, J.D.}
\begin{chunk}{axiom.bib}
@techreport{Gutt91,
author = "Guttman, J.D.",
title = {{A Propoed Interface Logic for Verification Environments}},
type = "technical report",
number = "M9119",
institution = "The MITRE Corporation",
year = "1991"
}
\end{chunk}
\begin{chunk}{axiom.bib}
@misc{Open11,
author = "Dos Reis, G.",
title = {{OpenAxiom}},
link = "\url{http://www.openaxiom.org}",
year = "2011"
}
\end{chunk}
\index{Matthews, David C.J.}
\index{Wenzel, Makarius}
\begin{chunk}{axiom.bib}
@inproceedings{Matt10,
author = "Matthews, David C.J. and Wenzel, Makarius",
title = {{Efficient Parallel Programming in Poly/ML and Isabelle/ML}},
booktitle = "Proc. 5th ACM SIGPLAN workshop on Declarative aspects of
multicore programming",
pages = "5362",
year = "2010",
publisher = "ACM",
isbn = "9781605588599",
abstract =
"The ML family of languages and LCFstyle interactive theorem proving
have been closely related from their beginnings about 30 years
ago. Here we report on a recent project to adapt both the Poly/ML
compiler and the Isabelle theorem prover to current multicore
hardware. Checking theories and proofs in typical Isabelle application
takes minutes or hours, and users expect to make efficient use of
``home machines'' with 28 cores, or more.
Poly/ML and Isabelle are big and complex software systems that have
evolved over more than two decades. Faced with the requirement to
deliver a stable and efficient parallel programming environment, many
infrastructure layers had to be reworked: from lowlevel system
threads to highlevel principles of valueoriented programming. At
each stage we carefully selected from the many existing concepts for
parallelism, and integrated them in a way that fits smoothly into the
idea of purely functional ML with the addition of synchronous
exceptions and asynchronous interrupts.
From the Isabelle/ML perspective, the main concept to manage parallel
evaluation is that of ``future values''. Scheduling is implicit, but it
is also possible to specify dependencies and priorities. In addition,
blockstructured groups of futures with propagation of exceptions
allow for alternative functional evaluation (such as parallel search),
without requiring user code to tackle concurrency. Our library also
provides the usual parallel combinators for functions on lists, and
analogous versions on prover tactics.
Despite substantial reorganization in the background, only minimal
changes are occasionally required in user ML code, and none at the
Isabelle application level (where parallel theory and proof processing
is fully implicit). The present implementation is able to address more
than 8 cores effectively, while the earlier version of the official
Isabelle2009 release works best for 24 cores. Scalability beyond 16
cores still poses some extra challenges, and will require further
improvements of the Poly/ML runtime system (heap management and
garbage collection), and additional parallelization of Isabelle
application logic.",
paper = "Matt10.pdf"
}
\end{chunk}
\begin{chunk}{axiom.bib}
@misc{Poly11a,
author = "Unknown",
title = {{Poly/ML}},
link = "\url{http://www.polyml.org}",
year = "2011"
}
\end{chunk}
\begin{chunk}{axiom.bib}
@misc{Isab11,
author = "Unknown",
title = {{Isabell}},
link = "\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html}",
year = "2011"
}
\end{chunk}
\index{Boulm\'e, Sylvain}
\begin{chunk}{axiom.bib}
@techreport{Boul00a,
author = "Boulme. Sylvain",
title = {{Specifying in Coq inheritance used in Computer Algebra
Libraries}},
year = "2000",
institution = "LIP6, Paris",
number = "2000.013",
abstract =
"This paper is part of FOC[3], a project for developing Computer
Algebra libraries, certified in Coq[2]. FOC has developed a
methodology for programming Computer Algebra libraries, using modules
and objects in Ocaml. In order to specify modularity features used by
FOC in Ocaml, we are coding in Coq a theory for extensible records
with dependent fields. This theory intends to express especially the
kind of inheritance with method redefinition and late binding, that
FOC uses in its Ocaml programs.
The unit of FOC are coded as records. As we want to encode sematic
information on units, the fields of our records may be proofs. Thus,
our fields may depend on each others. We call the
{\sl Drecords}. Then, we introduce a new datatype, called
{\sl mixDrec}, to represent FOC classes. Actually, mixDrecs are useful
for describing a hierarchy of Drecords in an incremental way. In
mixDrecs, fields can be only declared or they can be
redefined. MixDrecs can be extended by inheritance.",
paper = "Boul00a.pdf"
}
\end{chunk}
\index{Dennis, Louise A.}
\index{Collins, Graham}
\index{Norrish, Michael}
\index{Boulton, Richard}
\index{Slind, Konrad}
\index{Robinson, Graham}
\index{Gordon, Mike}
\index{Melham, Tom}
\begin{chunk}{axiom.bib}
@article{Denn00,
author = "Dennis, Louise A. and Collins, Graham and Norrish, Michael
and Boulton, Richard and Slind, Konrad and
Robinson, Graham and Gordon, Mike and Melham, Tom",
title = {{The PROSPER Toolkit}},
journal = "LNCS",
volume = "1785",
publisher = "SpringerVerlag",
pages = "7892",
year = "2000",
link =
"\url{https://link.springer.com/content/pdf/10.1007/3540464190_7.pdf}",
abstract =
"The PROSPER (Proof and Specification Assisted Design Environments)
project advocates the use of toolkits which allow existing
verification tools to be adapted to a more flexible format so that
they may be treated as components. A system incorporating such tools
becomes another component that can be embedded in an application. This
paper describes the PROSPER Toolkit which enables this. The nature of
communication between components is specified in a
languageindependent way. It is implemented in several common
programming languages to allow a wide variety of tools to have access
to the toolkit.",
paper = "Denn00.pdf"
}
\end{chunk}
\index{Dewar, Mike}
\begin{chunk}{axiom.bib}
@misc{Dewa00,
author = "Dewar, Mike",
title = {{Special Issue on OPENMATH}},
publisher = "ACM SIGPLAN Bulletin",
volume = "34",
number = "2",
year = "2000"
}
\end{chunk}
\index{Gray, Simon}
\index{Kajler, Norbert}
\index{Wang, Paul S.}
\begin{chunk}{axiom.bib}
@article{Gray98,
author = "Gray, Simon and Kajler, Norbert and Wang, Paul S.",
title = {{Design and Implementation of MP, a Protocol for
Efficient Exchange of Mathematical Expressions}},
journal = "J. Symboic Computation",
volume = "25",
pages = "213237",
year = "1998",
abstract =
"The Multi Project is an ongoing research e ort at Kent State
University aimed at providing an environment for distributed scientific
computing. An integral part of this environment is the Multi
Protocol (MP) which is designed to support ecientific communication of
mathematical data between scientificallyoriented software tools. MP
exchanges data in the form of linearized annotated syntax
trees. Syntax trees provide a simple, flexible and toolindependent
way to represent and exchange data, and annotations provide a powerful
and generic expressive facility for transmitting additional
information. At a level above the data exchange protocol,
dictionaries provide definitions for operators and constants, providing
shared semantics across heterogeneous packages. A clear distinction
between MPdefined and userdefined entities is enforced. Binary
encodings are used for efficiency. Commonly used values and blocks of
homogeneous data are further optimized. The protocol is independent of
the underlying communication paradigm and can support parallel
computation, distributed problemsolving environments, and the
coupling of tools for speci c applications.",
paper = "Gray98.pdf"
}
\end{chunk}
\index{Harrison, John}
\index{Th\'ery, Laurent}
\begin{chunk}{axiom.bib}
@incollection{Harr93,
author = "Harrison, John and Thery, Laurent",
title = {{Reasoning about the Reals: The Marriage of HOL and
Maple}},
booktitle = "Logic Programming and Automated Reasoning",
publisher = "SpringerVerlag",
year = "1993",
pages = "351353",
link =
"\url{https://link.springer.com/content/pdf/10.1007/3540569448_68.pdf}",
abstract =
"Computer algebra systems are extremely powerful and flexible, but
often give results which require careful interpretation or are
downright incorrect. By contrast, theorem provers are very reliable
but lack the powerful specialized decision procedures and heuristics
of computer algebra systems. In this paper we try to get the best of
both worlds by careful exploitation of a link between a theorem prover
and a computer algebra system.",
paper = "Harr93.pdf"
}
\end{chunk}
\index{Richardson, Daniel}
\begin{chunk}{axiom.bib}
@article{Rich69,
author = "Richardson, Daniel",
title = {{Some Undecidable Problems involving Elementar Functions of
a Real Variable}},
journal = "J. Symbolic Logic",
volume = "33",
number = "4",
year = "1969",
pages = "514520",
abstract =
"Let $E$ be a set of expressions representing real, single valued,
partially defined functions of one real variable. $E^*$ will be the
set of functions represented by expressions in $E$. If $A$ is an
expression in $E$, $A(x)$ is the function denoted by $AA$. It is
assumed that $D^*$ contains the identity function and the rational
numbers as constant functions and that $E^*$ is closed under addition,
subtraction, multiplication, and composition"
}
\end{chunk}
\index{Rushby, John}
\begin{chunk}{axiom.bib}
@inproceedings{Rush00,
author = "Rushby, John",
title = {{Disappearing Formal Methods}},
booktitle = "High Assurance Systems Engineering, 5th Int. Symp.",
pages = "9596",
year = "2000",
publisher = "ACM",
paper = "Rush00.pdf"
}
\end{chunk}
\index{Buchberger, B.}
\index{Dupre, C.}
\index{Jebelean, T.}
\index{Kriftner, F.}
\index{Nakagawa, K.}
\index{Vasaru, D.}
\index{Windsteiger, W.}
\begin{chunk}{axiom.bib}
@misc{Buch00,
author = "Buchberger, B. and Dupre, C. and Jebelean, T. and Kriftner, F.
and Nakagawa, K. and Vasaru, D. and Windsteiger, W.",
title = {{The Theorema Project: A Progress Report}},
year = "2000",
abstract =
"The THEOREMA project aims at supporting, within one consistent logic
and one coherent software system, the entire mathematical exploration
cycle including the phase of proving. In this paper we report on some
of the new features of THEOREMA that have been designed and
implemented since the first expository version of THEOREMA in
1997. These features are:  the THEOREMA formal text language  the
THEOREMA computational sessions  the ProveComputeSolve (PCS) prover
of THEOREMA  the THEOREMA set theory prover  special provers within
THEOREMA  the cascademetastrategy for THEOREMA provers  proof
simplification in THEOREMA. In the conclusion, we formulate design
goals for the next version of THEOREMA",
paper = "Buch00.pdf"
}
\end{chunk}
\index{Boyer, Robert S.}
\index{Moore, J Strother}
\begin{chunk}{axiom.bib}
@techreport{Boye85,
author = "Boyer, Robert S. and Moore, J Strother",
title = {{Integrating Decision Procedures into Heuristic Theorem Provers}},
type = "technical report",
institution = "Inst. for Comp. Sci. University of Texas at Austin",
number = "ICSCACMP44",
year = "1985",
abstract =
"We discuss the problem of incorporating into a heuristic theorem
prover a decision procedure for a fragment of the logic. An obvious
goal when incorporating such a procedure is to reduce the search space
explored by the heuristic component of the system, as would be
achieved by eliminating from the system’s data base some explicitly
stated axioms. For example, if a decision procedure for linear
inequalities is added, one would hope to eliminate the explicit
consideration of the transitivity axioms. However, the decision
procedure must then be used in all the ways the eliminated axioms
might have been. The difficulty of achieving this degree of
integration is more dependent upon the complexity of the heuristic
component than upon that of the decision procedure. The view of the
decision procedure as a ``black box'' is frequently destroyed by the
need pass large amounts of search strategic information back and forth
between the two components. Finally, the efficiency of the decision
procedure may be virtually irrelevant; the efficiency of the final
system may depend most heavily on how easy it is to communicate
between the two components. This paper is a case study of how we
integrated a linear arithmetic procedure into a heuristic theorem
prover. By linear arithmetic here we mean the decidable subset of
number theory dealing with universally quantified formulas composed of
the logical connectives, the identity relation, the Peano ``less than''
relation, the Peano addition and subtraction functions, Peano
constants, and variables taking on natural values. We describe our
system as it originally stood, and then describe chronologically the
evolution of our linear arithmetic procedure and its interface to the
heuristic theorem prover. We also provide a detailed description of
our final linear arithmetic procedure and the use we make of it. This
description graphically illustrates the difference between a
standalone decision procedure and one that is of use to a more
powerful theorem prover.",
paper = "Boye85.pdf"
}
\end{chunk}
\index{Farmer, William M.}
\index{Guttman, Joshua D.}
\index{Fabrega, F. Javier Thayer}
\begin{chunk}{axiom.bib}
@article{Farm96,
author = "Farmer, William M. and Guttman, Joshua D. and
Fabrega, F. Javier Thayer",
title = {{IMPS: An Updated System Description}},
journal = "LNCS",
volume = "1104",
pages = "298302",
year = "1996",
paper = "Farm96.pdf"
}
\end{chunk}
\index{Gordon, M.}
\index{Milner, R.}
\index{Wadsworth, C.P.}
\begin{chunk}{axiom.bib}
@book{Gord79,
author = "Gordon, M. and Milner, R. and Wadsworth, C.P.",
title = {{Edinburgh LCF: A Mechanised Logic of Computation}},
comment = "Lecture Notes in Computer Science Volume 78",
publisher = "SpringerVerlag",
year = "1979"
}
\end{chunk}
\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@misc{Pfen17,
author = "Pfenning, Frank",
title = {{Logical Frameworks}},
link = "\url{http://www.cs.cmu.edu/afs/cs.cmu.edu/user/fp/www/lfs.html}",
year = "2017"
}
\end{chunk}
\begin{chunk}{axiom.bib}
@misc{Theo17,
author = "Unknown",
title = {{Theorema Project}},
link = "\url{http://www.theorema.org}",
year = "2017"
}
\end{chunk}

books/axiom.bib  572 +++++++++++++++
books/bookvolbib.pamphlet  747 +++++++++++++++++++
changelog  2 +
patch  1460 ++++++++++++++
src/axiomwebsite/patches.html  2 +
5 files changed, 1774 insertions(+), 1009 deletions()
diff git a/books/axiom.bib b/books/axiom.bib
index 449bd1a..45a0383 100644
 a/books/axiom.bib
+++ b/books/axiom.bib
@@ 901,6 +901,37 @@ paper = "Brea89.pdf"
paper = "Farm90.pdf"
}
+@article{Farm95,
+ author = "Farmer, William M. and Guttman, J.D. and Thayer, F.J.",
+ title = {{Contexts in Mathematical Reasoning and Computation}},
+ journal = "J. of Symbolic Computation",
+ volume = "19",
+ pages = "201216",
+ year = "1995",
+ abstract =
+ "Contexts are sets of formulas used to manage the assumptions that
+ arise in the course of a mathematical deduction or
+ calculation. Although contextdependent reasoning is commonplace in
+ informal mathematics, most contemporary symbolic computation systems
+ do not utilize contexts in sophisticated ways. This paper describes
+ some contextbased techniques for symbolic computation, including
+ techniques for reasoning about definedness, simplifying abstract
+ algebraic expressions, and computing with theorems. All of these
+ techniques are implemented in the IMPS Interactive Mathematical Proof
+ System. The paper also proposes a general mathematics laboratory that
+ combines the functionality of current symbolic computation systems
+ with the facilities of a theorem proving system like IMPS.",
+ paper = "Farm95.pdf"
+}
+
+@misc{Farm95a,
+ author = "Farmer, William M. and Guttman, Joshua D. and
+ F. Javier Thayer",
+ title = {{The IMPS User's Manual}},
+ link = "\url{http://imps.mcmaster.ca/manual/manual.html}",
+ year = "1995"
+}
+
@article{Faxe02,
author = "Faxen, KarlFilip",
title = "A Static Sematics for Haskell",
@@ 1118,6 +1149,14 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@book{Gord79,
+ author = "Gordon, M. and Milner, R. and Wadsworth, C.P.",
+ title = {{Edinburgh LCF: A Mechanised Logic of Computation}},
+ comment = "Lecture Notes in Computer Science Volume 78",
+ publisher = "SpringerVerlag",
+ year = "1979"
+}
+
@article{Gons71,
author = "Gonshor, H.",
title = "Contributions to Genetic Algebras",
@@ 1317,6 +1356,13 @@ paper = "Brea89.pdf"
year = "1991"
}
+@misc{Isab11,
+ author = "Unknown",
+ title = {{Isabell}},
+ link = "\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html}",
+ year = "2011"
+}
+
@article{Jame81,
author = "James, G. and Kerber, A.",
title = "The Representation Theory of the Symmetric Group",
@@ 2093,6 +2139,13 @@ paper = "Brea89.pdf"
year = "1985"
}
+@misc{Poly11a,
+ author = "Unknown",
+ title = {{Poly/ML}},
+ link = "\url{http://www.polyml.org}",
+ year = "2011"
+}
+
@misc{QED94,
author = "Anonymous",
title = {{The QED Manifesto}},
@@ 6503,6 +6556,32 @@ paper = "Brea89.pdf"
paper = "Bert94.pdf"
}
+@article{Brow69,
+ author = "Brown, W.S.",
+ title = {{Rational Exponential Expressions and a Conjecture Concerning
+ $\pi$ and $e$}},
+ journal = "The American Mathematical Monthly",
+ volume = "76",
+ number = "1",
+ year = "1969",
+ pages = "2834",
+ abstract =
+ "One of the most controversial and least well defined of mathematical
+ problems is the problem of simplification. The recent upsurge
+ of interest in mechanized mathematics has lent new urgency to this
+ problem, but so far very little has been accomplished. This paper
+ attempts to shed light on the situation by introducing the class of
+ rational exponential expressions, defining simplification within
+ this class, and showing constructively how to achieve it. It is shown
+ that the only simplified rational exponential expression equivalent to
+ 0 is 0 itself, provided that an easily stated conjecture is true.
+ However the conjecture, if true, will surely be difficult to prove,
+ since it asserts as a special case that $\pi$ and $e$ are algebraically
+ independent, and no one has yet been able to prove even the much
+ weaker conjecture that $\pi+e$ is irrational.",
+ paper = "Brow69.pdf"
+}
+
@article{Clar89,
author = "Clarkson, M.",
title = {{MACSYMA's inverse Laplace transform}},
@@ 7464,6 +7543,26 @@ paper = "Brea89.pdf"
paper = "Benk03.pdf"
}
+@inproceedings{Benz01,
+ author = "Benzmuller, Christoph and Jamnik, Mateja and Kerber, Manfred
+ and Sorge, Volker",
+ title = {{An Agentoriented Approach to Reasoning}},
+ booktitle = "Proc. Calculemus Workshop 2001",
+ pages = "4863",
+ link = "\url{http://christoph.benzmueller.di/papers/W11.pdf}",
+ year = "2001",
+ abstract =
+ "This paper discusses experiments with an agent oriented approach to
+ automated and interactive reasoning. The approach combines ideas from
+ two subfields of AI (theorem proving/proof planning and multiagent
+ systems) and makes use of state of the art distribution techniques to
+ decentralise and spread its reasoning agents over the internet. It
+ particularly supports cooperative proofs between reasoning systems
+ which are strong in different application areas, e.g., higherorder
+ and firstorder theorem provers and computer algebra systems.",
+ paper = "Benz01.pdf"
+}
+
@book{Bert04,
author = {Bertot, Yves Cast\'eran, Pierre},
title = {{Interactive Theorem Proving and Program Development}},
@@ 7645,6 +7744,34 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@techreport{Boul00a,
+ author = "Boulme. Sylvain",
+ title = {{Specifying in Coq inheritance used in Computer Algebra
+ Libraries}},
+ year = "2000",
+ institution = "LIP6, Paris",
+ number = "2000.013",
+ abstract =
+ "This paper is part of FOC[3], a project for developing Computer
+ Algebra libraries, certified in Coq[2]. FOC has developed a
+ methodology for programming Computer Algebra libraries, using modules
+ and objects in Ocaml. In order to specify modularity features used by
+ FOC in Ocaml, we are coding in Coq a theory for extensible records
+ with dependent fields. This theory intends to express especially the
+ kind of inheritance with method redefinition and late binding, that
+ FOC uses in its Ocaml programs.
+
+ The unit of FOC are coded as records. As we want to encode sematic
+ information on units, the fields of our records may be proofs. Thus,
+ our fields may depend on each others. We call the
+ {\sl Drecords}. Then, we introduce a new datatype, called
+ {\sl mixDrec}, to represent FOC classes. Actually, mixDrecs are useful
+ for describing a hierarchy of Drecords in an incremental way. In
+ mixDrecs, fields can be only declared or they can be
+ redefined. MixDrecs can be extended by inheritance.",
+ paper = "Boul00a.pdf"
+}
+
@InProceedings{Boul99,
author = "Boulme, S. and Hardin, T. and Hirschkoff, D. and Rioboo, Renaud",
title = {{On the way to certify Computer Algebra Systems}},
@@ 7755,6 +7882,48 @@ paper = "Brea89.pdf"
year = "1981"
}
+@techreport{Boye85,
+ author = "Boyer, Robert S. and Moore, J Strother",
+ title = {{Integrating Decision Procedures into Heuristic Theorem Provers}},
+ type = "technical report",
+ institution = "Inst. for Comp. Sci. University of Texas at Austin",
+ number = "ICSCACMP44",
+ year = "1985",
+ abstract =
+ "We discuss the problem of incorporating into a heuristic theorem
+ prover a decision procedure for a fragment of the logic. An obvious
+ goal when incorporating such a procedure is to reduce the search space
+ explored by the heuristic component of the system, as would be
+ achieved by eliminating from the system’s data base some explicitly
+ stated axioms. For example, if a decision procedure for linear
+ inequalities is added, one would hope to eliminate the explicit
+ consideration of the transitivity axioms. However, the decision
+ procedure must then be used in all the ways the eliminated axioms
+ might have been. The difficulty of achieving this degree of
+ integration is more dependent upon the complexity of the heuristic
+ component than upon that of the decision procedure. The view of the
+ decision procedure as a ``black box'' is frequently destroyed by the
+ need pass large amounts of search strategic information back and forth
+ between the two components. Finally, the efficiency of the decision
+ procedure may be virtually irrelevant; the efficiency of the final
+ system may depend most heavily on how easy it is to communicate
+ between the two components. This paper is a case study of how we
+ integrated a linear arithmetic procedure into a heuristic theorem
+ prover. By linear arithmetic here we mean the decidable subset of
+ number theory dealing with universally quantified formulas composed of
+ the logical connectives, the identity relation, the Peano ``less than''
+ relation, the Peano addition and subtraction functions, Peano
+ constants, and variables taking on natural values. We describe our
+ system as it originally stood, and then describe chronologically the
+ evolution of our linear arithmetic procedure and its interface to the
+ heuristic theorem prover. We also provide a detailed description of
+ our final linear arithmetic procedure and the use we make of it. This
+ description graphically illustrates the difference between a
+ standalone decision procedure and one that is of use to a more
+ powerful theorem prover.",
+ paper = "Boye85.pdf"
+}
+
@book{Boye88,
author = "Boyer, R.S. and Moore, J.S.",
title = {{A Computational Logic Handbook}},
@@ 7858,6 +8027,26 @@ paper = "Brea89.pdf"
paper = "Buch01.pdf"
}
+@misc{Buch00,
+ author = "Buchberger, B. and Dupre, C. and Jebelean, T. and Kriftner, F.
+ and Nakagawa, K. and Vasaru, D. and Windsteiger, W.",
+ title = {{The Theorema Project: A Progress Report}},
+ year = "2000",
+ abstract =
+ "The THEOREMA project aims at supporting, within one consistent logic
+ and one coherent software system, the entire mathematical exploration
+ cycle including the phase of proving. In this paper we report on some
+ of the new features of THEOREMA that have been designed and
+ implemented since the first expository version of THEOREMA in
+ 1997. These features are:  the THEOREMA formal text language  the
+ THEOREMA computational sessions  the ProveComputeSolve (PCS) prover
+ of THEOREMA  the THEOREMA set theory prover  special provers within
+ THEOREMA  the cascademetastrategy for THEOREMA provers  proof
+ simplification in THEOREMA. In the conclusion, we formulate design
+ goals for the next version of THEOREMA",
+ paper = "Buch00.pdf"
+}
+
@article{Buch06,
author = "Buchberger,B and Craciun, A. and Jebelean, T. and
Kovacs, L. and Kutsia, T. and Nakagawa, K. and Piroi, F.
@@ 8589,6 +8778,32 @@ paper = "Brea89.pdf"
paper = "Demi79.pdf"
}
+@article{Denn00,
+ author = "Dennis, Louise A. and Collins, Graham and Norrish, Michael
+ and Boulton, Richard and Slind, Konrad and
+ Robinson, Graham and Gordon, Mike and Melham, Tom",
+ title = {{The PROSPER Toolkit}},
+ journal = "LNCS",
+ volume = "1785",
+ publisher = "SpringerVerlag",
+ pages = "7892",
+ year = "2000",
+ link =
+ "\url{https://link.springer.com/content/pdf/10.1007/3540464190_7.pdf}",
+ abstract =
+ "The PROSPER (Proof and Specification Assisted Design Environments)
+ project advocates the use of toolkits which allow existing
+ verification tools to be adapted to a more flexible format so that
+ they may be treated as components. A system incorporating such tools
+ becomes another component that can be embedded in an application. This
+ paper describes the PROSPER Toolkit which enables this. The nature of
+ communication between components is specified in a
+ languageindependent way. It is implemented in several common
+ programming languages to allow a wide variety of tools to have access
+ to the toolkit.",
+ paper = "Denn00.pdf"
+}
+
@book{Devl79,
author = "Devlin, Keith J.",
title = {{Fundamentals of Contemporary Set Theory}},
@@ 8783,6 +8998,66 @@ paper = "Brea89.pdf"
keywords = "axiomref, CASProof"
}
+@article{Farm92a,
+ author = "Farmer, William H.",
+ title = {{IMPS: System Description}},
+ journal = "Lecture Notes in Computer Science",
+ volume = "607",
+ pages = "701705",
+ year = "1992",
+ paper = "Farm92a.pdf"
+}
+
+@article{Farm96,
+ author = "Farmer, William M. and Guttman, Joshua D. and
+ Fabrega, F. Javier Thayer",
+ title = {{IMPS: An Updated System Description}},
+ journal = "LNCS",
+ volume = "1104",
+ pages = "298302",
+ year = "1996",
+ paper = "Farm96.pdf"
+}
+
+@article{Farm92,
+ author = "Farmer, William H.",
+ title = {{Little Theories}},
+ journal = "LNCS",
+ volume = "607",
+ year = "1992",
+ pages = "567581",
+ abstract =
+ "In the ``little theories'' version of the axiomatic method, different
+ portions of mathematics are developed in various different formal
+ axiomatic theories. Axiomatic theories may be related by inclusion or
+ by theory interpretation. We argue that the little theories approach
+ is a desirable way to formalize mathematics, and we describe how IMPS,
+ an Interactive Mathematical Proof System, supports it.",
+ paper = "Farm92.pdf"
+}
+
+@article{Farm93b,
+ author = "Farmer, William M.",
+ title = {{A simple type theory with partial functions and subtypes}},
+ journal = "Annals of Pure and Applied Logic",
+ volume = "64",
+ pages = "211240",
+ year = "1993",
+ abstract =
+ "Simple type theory is a higherorder predicate logic for reasoning
+ about truth values, individuals, and simply typed total functions. We
+ present in this paper a version of simple type theory, called PF*, in
+ which functions may be partial and types may have subtypes. We define
+ both a Henkinstyle general models semantics and an axiomatic system
+ for PF*, and we prove that the axiomatic system is complete with
+ respect to the general models semantics. We also define a notion of
+ an interpretation of one PF* theory in another. PF* is intended as a
+ foundation for mechanized mathematics. It is the basis for the logic
+ of IMPS, an Interactive Mathematical Proof System developed at The
+ MITRE Corporation.",
+ paper = "Farm93b.pdf"
+}
+
@article{Farm93a,
author = "Farmer, William M. and Guttman, Joshua D. and Thayer, Javier",
title = {{IMPS: An Interactive Mathematical Proof Systems}},
@@ 8821,6 +9096,20 @@ paper = "Brea89.pdf"
paper = "Farm93.pdf"
}
+@article{Farm94,
+ author = "Farmer, William M. and Guttman, Joshua D. and Nadel, Mark E.
+ and Fabrega, F. Javier Thayer",
+ title = {{Proof Script Pragmatics in IMPS}},
+ journal = "LNCS",
+ volume = "814",
+ pages = "356370",
+ year = "1994",
+ abstract =
+ "This paper instroduces the IMPS proof script mechanism and some
+ practical methods for exploiting it.",
+ paper = "Farm94.pdf"
+}
+
@misc{Fate02a,
author = "Fateman, Richard J.",
title = {{Symbolic Execution Merges Construction, Debugging and Proving}},
@@ 9259,6 +9548,27 @@ paper = "Brea89.pdf"
year = "2013"
}
+@incollection{Harr93,
+ author = "Harrison, John and Thery, Laurent",
+ title = {{Reasoning about the Reals: The Marriage of HOL and
+ Maple}},
+ booktitle = "Logic Programming and Automated Reasoning",
+ publisher = "SpringerVerlag",
+ year = "1993",
+ pages = "351353",
+ link =
+ "\url{https://link.springer.com/content/pdf/10.1007/3540569448_68.pdf}",
+ abstract =
+ "Computer algebra systems are extremely powerful and flexible, but
+ often give results which require careful interpretation or are
+ downright incorrect. By contrast, theorem provers are very reliable
+ but lack the powerful specialized decision procedures and heuristics
+ of computer algebra systems. In this paper we try to get the best of
+ both worlds by careful exploitation of a link between a theorem prover
+ and a computer algebra system.",
+ paper = "Harr93.pdf"
+}
+
@inproceedings{Harr94,
author = "Harrison, John and Thery, Laurent",
title = {{Extending the HOL Thoerem Prover with a Computer Algebra System
@@ 9278,7 +9588,7 @@ paper = "Brea89.pdf"
@techreport{Harr95,
author = "Harrison, John",
 title = {{Methatheory and Reflection in Theorem Proving: A Survey
+ title = {{Metatheory and Reflection in Theorem Proving: A Survey
and Critique}},
institution = "SRI Cambridge",
year = "1995",
@@ 9434,6 +9744,7 @@ paper = "Brea89.pdf"
author = "Homann, Karsten",
title = {{Symbolisches L\"osen mathematischer Probleme durch
Kooperation algorithmischer und logischer Systeme}},
+ comment = {{Symboic Mathematical Problem Solving by Cooperation of Algorithmic and Logical Services (in German)}},
year = "1996",
school = {Universit\"at Karlsruhe},
paper = "Homa96a.pdf"
@@ 10819,6 +11130,18 @@ paper = "Brea89.pdf"
compilers."
}
+@article{Owre92,
+ author = "Owre, S. and Rushby, J.M. and Shankar, N.",
+ title = {{PVS: A Prototype Verification System}},
+ journal = "Lecture Notes in Computer Science",
+ volume = "687",
+ pages = "748752",
+ year = "1992",
+ abstract =
+ "This brief paper introduces the main ideas of PVS",
+ paper = "Owre92.pdf"
+}
+
@article{Pada80,
author = "Padawitz, Peter",
title = {{New results on completeness and consistency of abstract data
@@ 11066,13 +11389,21 @@ paper = "Brea89.pdf"
paper = "Pfen89.pdf"
}
\incollection{Pfen92,
+@misc{Pfen17,
+ author = "Pfenning, Frank",
+ title = {{Logical Frameworks}},
+ link = "\url{http://www.cs.cmu.edu/afs/cs.cmu.edu/user/fp/www/lfs.html}",
+ year = "2017"
+}
+
+@incollection{Pfen92a,
author = "Pfenning, Frank",
title = {{Dependent Types in Logic Programming}},
booktitle = "Types in Logic Programming",
isbn = "9780262161312",
publisher = "MIT Press",
 year = "1992"
+ year = "1992",
+ paper = "Pfen92a.pdf"
}
@book{Pier00,
@@ 11535,6 +11866,13 @@ paper = "Brea89.pdf"
year = "1995",
}
+@misc{Theo17,
+ author = "Unknown",
+ title = {{Theorema Project}},
+ link = "\url{http://www.theorema.org}",
+ year = "2017"
+}
+
@article{Ther01,
author = "Th\'ery, Laurent",
title = {{A MachineChecked Implementation of Buchberger's Algorithm}},
@@ 17509,6 +17847,13 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@misc{Open11,
+ author = "Dos Reis, G.",
+ title = {{OpenAxiom}},
+ link = "\url{http://www.openaxiom.org}",
+ year = "2011"
+}
+
@misc{West95,
author = "Wester, Michael J.",
title = {{A Review of CAS Mathematical Capabilities}},
@@ 23152,27 +23497,6 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
@article{Reis11,
 author = "Dos Reis, Gabriel",
 title = {{Retargeting OpenAxiom to Poly/ML: towards an integrated proof
 assistants and computer algebra system framework}},
 journal = "Intelligent computer mathematics (MKM 2011)",
 year = "2011",
 isbn = "9783642226724",
 link = "\url{https://www.semanticscholar.org/paper/RetargetingOpenAxiomtoPolyMLTowardsanReisMatthews/4ce5d85ea8424ced82d}",
 abstract =
 "This paper presents an ongoing effort to integrate the AXIOM family
 of computer algebra systems with Poly/MLbased proof assistants in the
 same framework. A longterm goal is to make a large set of efficient
 implementations of algebraic algorithms available to popular proof
 assistants, and also to bring the power of mechanized formal
 verification to a family of strongly typed computer algebra systems at
 a modest cost. Our approach is based on retargeting the code generator
 of the OpenAxiom compiler to the Poly/ML abstract machine.",
 paper = "Reis11.pdf",
 keywords = "axiomref"
}

@article{Reis06,
author = "Dos Reis, Gabriel and Stroustrup, Bjarne",
title = {{Specifying C++ Concepts}},
@@ 31629,6 +31953,15 @@ paper = "Brea89.pdf"
paper = "Bitt94.pdf"
}
+@book{Boge77,
+ author = "Bogen, Richard",
+ title = {{MACSYMA Reference Manual, Version 9}},
+ publisher = "MIT",
+ year = "1977",
+ link = "\url{http://bitsavers.informatik.unistuttgart.de/pdf/mit/macsyma/MACSYMA_RefMan_V9_Dec77.pdf}",
+ paper = "Boge77.pdf"
+}
+
@inproceedings{Brad86,
author = "Bradford, Russell J. and Hearn, Anthony C. and Padget, Julian and
Schrufer, Eberhard",
@@ 32001,6 +32334,17 @@ paper = "Brea89.pdf"
pages = "95101",
}
+@article{Cher80,
+ author = "Cherlin, Gregory",
+ title = {{Rings of Continuous Functions: Decision Problems}},
+ journal = "Lecture Notes in Mathematics",
+ volume = "834",
+ pages = "4491",
+ year = "1980",
+ link = "\url{https://link.springer.com/content/pdf/10.1007/BFb0090160.pdf}",
+ paper = "Cher80.pdf"
+}
+
@misc{Chew95,
author = "Chew, Paul and Constable, Robert L. and Pingali, Keshav and
Vavasis, Steve and Zippel, Richard",
@@ 32139,6 +32483,17 @@ paper = "Brea89.pdf"
paper = "Corl92.pdf"
}
+@article{Crai92,
+ author = "Craigen, Dan and Kromodimoeljo, Sentot and Meisels, Irwin
+ and Pase, Bill",
+ title = {{Eves System Description}},
+ journal = "Lecture Notes in Computer Science",
+ volume = "607",
+ pages = "771775",
+ year = "1992",
+ paper = "Crai92.pdf"
+}
+
@article{Cunn85,
author = "Cunningham, R.J. and Dick, A.J.J",
title = {{Rewrite Systems on a Lattice of Types}},
@@ 32219,6 +32574,15 @@ paper = "Brea89.pdf"
paper = "Denz94.pdf"
}
+@misc{Dewa00,
+ author = "Dewar, Mike",
+ title = {{Special Issue on OPENMATH}},
+ publisher = "ACM SIGPLAN Bulletin",
+ volume = "34",
+ number = "2",
+ year = "2000"
+}
+
@misc{Dolz96,
author = "Dolzmann, Andreas and Sturm, Thomas",
title = {{Redlog User Manual Edition 1.0}},
@@ 32697,6 +33061,36 @@ paper = "Brea89.pdf"
year = "1991"
}
+@article{Gray98,
+ author = "Gray, Simon and Kajler, Norbert and Wang, Paul S.",
+ title = {{Design and Implementation of MP, a Protocol for
+ Efficient Exchange of Mathematical Expressions}},
+ journal = "J. Symboic Computation",
+ volume = "25",
+ pages = "213237",
+ year = "1998",
+ abstract =
+ "The Multi Project is an ongoing research e ort at Kent State
+ University aimed at providing an environment for distributed scientific
+ computing. An integral part of this environment is the Multi
+ Protocol (MP) which is designed to support ecientific communication of
+ mathematical data between scientificallyoriented software tools. MP
+ exchanges data in the form of linearized annotated syntax
+ trees. Syntax trees provide a simple, flexible and toolindependent
+ way to represent and exchange data, and annotations provide a powerful
+ and generic expressive facility for transmitting additional
+ information. At a level above the data exchange protocol,
+ dictionaries provide definitions for operators and constants, providing
+ shared semantics across heterogeneous packages. A clear distinction
+ between MPdefined and userdefined entities is enforced. Binary
+ encodings are used for efficiency. Commonly used values and blocks of
+ homogeneous data are further optimized. The protocol is independent of
+ the underlying communication paradigm and can support parallel
+ computation, distributed problemsolving environments, and the
+ coupling of tools for speci c applications.",
+ paper = "Gray98.pdf"
+}
+
@inproceedings{Gris76,
author = "Griss, Martin L.",
title = {{The Definition and Use of Data Structures in REDUCE}},
@@ 32733,6 +33127,15 @@ paper = "Brea89.pdf"
paper = "Gues87.pdf"
}
+@techreport{Gutt91,
+ author = "Guttman, J.D.",
+ title = {{A Propoed Interface Logic for Verification Environments}},
+ type = "technical report",
+ number = "M9119",
+ institution = "The MITRE Corporation",
+ year = "1991"
+}
+
@article{Hach95,
author = "Hach\'e, G. and Le Brigand, D.",
title = {{Effective construction of algebraic geometry codes}},
@@ 33778,13 +34181,63 @@ paper = "Brea89.pdf"
link = "\url{http://commonlisp.net/project/htajax/htajax.html}"
}
+@inproceedings{Matt10,
+ author = "Matthews, David C.J. and Wenzel, Makarius",
+ title = {{Efficient Parallel Programming in Poly/ML and Isabelle/ML}},
+ booktitle = "Proc. 5th ACM SIGPLAN workshop on Declarative aspects of
+ multicore programming",
+ pages = "5362",
+ year = "2010",
+ publisher = "ACM",
+ isbn = "9781605588599",
+ abstract =
+ "The ML family of languages and LCFstyle interactive theorem proving
+ have been closely related from their beginnings about 30 years
+ ago. Here we report on a recent project to adapt both the Poly/ML
+ compiler and the Isabelle theorem prover to current multicore
+ hardware. Checking theories and proofs in typical Isabelle application
+ takes minutes or hours, and users expect to make efficient use of
+ ``home machines'' with 28 cores, or more.
+
+ Poly/ML and Isabelle are big and complex software systems that have
+ evolved over more than two decades. Faced with the requirement to
+ deliver a stable and efficient parallel programming environment, many
+ infrastructure layers had to be reworked: from lowlevel system
+ threads to highlevel principles of valueoriented programming. At
+ each stage we carefully selected from the many existing concepts for
+ parallelism, and integrated them in a way that fits smoothly into the
+ idea of purely functional ML with the addition of synchronous
+ exceptions and asynchronous interrupts.
+
+ From the Isabelle/ML perspective, the main concept to manage parallel
+ evaluation is that of ``future values''. Scheduling is implicit, but it
+ is also possible to specify dependencies and priorities. In addition,
+ blockstructured groups of futures with propagation of exceptions
+ allow for alternative functional evaluation (such as parallel search),
+ without requiring user code to tackle concurrency. Our library also
+ provides the usual parallel combinators for functions on lists, and
+ analogous versions on prover tactics.
+
+ Despite substantial reorganization in the background, only minimal
+ changes are occasionally required in user ML code, and none at the
+ Isabelle application level (where parallel theory and proof processing
+ is fully implicit). The present implementation is able to address more
+ than 8 cores effectively, while the earlier version of the official
+ Isabelle2009 release works best for 24 cores. Scalability beyond 16
+ cores still poses some extra challenges, and will require further
+ improvements of the Poly/ML runtime system (heap management and
+ garbage collection), and additional parallelization of Isabelle
+ application logic.",
+ paper = "Matt10.pdf"
+}
+
@misc{Maxi16a,
author = "Maxima",
title = {{Symbolic Integration: The Algorithms}},
link = "\url{http://maxima.sourceforge.net/docs/tutorial/en/gaertnertutorialrevision/Pages/SI001.htm}"
}
@phdthsis{Mayr09,
+@phdthesis{Mayr09,
author = "Mayrhofer, Gunther",
title = {{Symbolic COmputation Prover with Induction}},
year = "2009",
@@ 34222,6 +34675,28 @@ paper = "Brea89.pdf"
paper = "Pfen89a.pdf"
}
+@article{Pfen92b,
+ author = "Pfenning, Frank and Rohwedder, Ekkehard",
+ title = {{Implementing the MetaTheory of Deductive Systems}},
+ journal = "Lecture Notes in Computer Science",
+ volume = "607",
+ pages = "771775",
+ year = "1992",
+ abstract =
+ "We exhibit a methodology for formulating and verifying meta theorems
+ about deductive systems in the Elf language, an implementation of the
+ LF Logical Framework with an operational semantics in the spirit of
+ logic programming. It is based on the mechanical verification of
+ properties of transformations between deductions, which relies on type
+ reconstruction and schemachecking. The latter is justified by
+ induction principles for closed LF objects, which can be constructed
+ over a given signature. We illustrate our technique through several
+ examples, the most extensive of which is an interpre tation of
+ classical logic in minimal logic through a continuationpassingstyle
+ transformation on proofs.",
+ paper = "Pfen92b.pdf"
+}
+
@misc{Pfen97,
author = "Pfenning, Frank",
title = {{Computation and Deduction}},
@@ 34383,6 +34858,25 @@ paper = "Brea89.pdf"
pages = "433455"
}
+@article{Rich69,
+ author = "Richardson, Daniel",
+ title = {{Some Undecidable Problems involving Elementar Functions of
+ a Real Variable}},
+ journal = "J. Symbolic Logic",
+ volume = "33",
+ number = "4",
+ year = "1969",
+ pages = "514520",
+ abstract =
+ "Let $E$ be a set of expressions representing real, single valued,
+ partially defined functions of one real variable. $E^*$ will be the
+ set of functions represented by expressions in $E$. If $A$ is an
+ expression in $E$, $A(x)$ is the function denoted by $AA$. It is
+ assumed that $D^*$ contains the identity function and the rational
+ numbers as constant functions and that $E^*$ is closed under addition,
+ subtraction, multiplication, and composition"
+}
+
@inproceedings{Rich94,
author = "Richardson, Dan and Fitch, John P.",
title = {{The identity problem for elementary functions and constants}},
@@ 34462,6 +34956,16 @@ paper = "Brea89.pdf"
paper = "Rump88.pdf"
}
+@inproceedings{Rush00,
+ author = "Rushby, John",
+ title = {{Disappearing Formal Methods}},
+ booktitle = "High Assurance Systems Engineering, 5th Int. Symp.",
+ pages = "9596",
+ year = "2000",
+ publisher = "ACM",
+ paper = "Rush00.pdf"
+}
+
@book{Saun79,
author = "MacLane, Saunders and Birkhoff, Garrett",
title = {{Algebra, Second Edition}},
@@ 34538,6 +35042,14 @@ paper = "Brea89.pdf"
the subject for the first time."
}
+@book{Sche01,
+ author = "Schelter, William F.",
+ title = {{Maxima Manual Version 5.41.0}},
+ year = "2001",
+ publisher = "Sourceforge",
+ paper = "Sche01.pdf"
+}
+
@techreport{Schr09,
author = "Schreiner, Wolfgang",
title = {{How to Write Postconditions with Nultiple Cases}},
@@ 34902,6 +35414,16 @@ paper = "Brea89.pdf"
paper = "Wink95.pdf"
}
+@article{Wosx92,
+ author = "Wos, Larry",
+ title = {{The Impossibility of the Automation of Logical Reasoning}},
+ journal = "Lecture Notes in Computer Science",
+ volume = "607",
+ year = "1992",
+ pages = "13",
+ paper = "Wosx92.pdf"
+}
+
@book{Wuxx94,
author = "Wu, Wentsun",
title = {{Mechanical Theorem Proving in Geometries}},
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 15dc9e5..ee0dca5 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 1386,6 +1386,7 @@ paper = "Brea89.pdf"
\subsection{F} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
\index{Farmer, William M.}
\begin{chunk}{axiom.bib}
@article{Farm90,
@@ 1412,6 +1413,49 @@ paper = "Brea89.pdf"
\end{chunk}
+\index{Farmer, William M.}
+\index{Guttman, J.D.}
+\index{Thayer, F.J.}
+\begin{chunk}{axiom.bib}
+@article{Farm95,
+ author = "Farmer, William M. and Guttman, J.D. and Thayer, F.J.",
+ title = {{Contexts in Mathematical Reasoning and Computation}},
+ journal = "J. of Symbolic Computation",
+ volume = "19",
+ pages = "201216",
+ year = "1995",
+ abstract =
+ "Contexts are sets of formulas used to manage the assumptions that
+ arise in the course of a mathematical deduction or
+ calculation. Although contextdependent reasoning is commonplace in
+ informal mathematics, most contemporary symbolic computation systems
+ do not utilize contexts in sophisticated ways. This paper describes
+ some contextbased techniques for symbolic computation, including
+ techniques for reasoning about definedness, simplifying abstract
+ algebraic expressions, and computing with theorems. All of these
+ techniques are implemented in the IMPS Interactive Mathematical Proof
+ System. The paper also proposes a general mathematics laboratory that
+ combines the functionality of current symbolic computation systems
+ with the facilities of a theorem proving system like IMPS.",
+ paper = "Farm95.pdf"
+}
+
+\end{chunk}
+
+\index{Farmer, William M.}
+\index{Guttman, Joshua D.}
+\index{F. Javier Thayer}
+\begin{chunk}{axiom.bib}
+@misc{Farm95a,
+ author = "Farmer, William M. and Guttman, Joshua D. and
+ F. Javier Thayer",
+ title = {{The IMPS User's Manual}},
+ link = "\url{http://imps.mcmaster.ca/manual/manual.html}",
+ year = "1995"
+}
+
+\end{chunk}
+
\index{Faxen, KarlFilip}
\begin{chunk}{axiom.bib}
@article{Faxe02,
@@ 1697,6 +1741,20 @@ paper = "Brea89.pdf"
\end{chunk}
+\index{Gordon, M.}
+\index{Milner, R.}
+\index{Wadsworth, C.P.}
+\begin{chunk}{axiom.bib}
+@book{Gord79,
+ author = "Gordon, M. and Milner, R. and Wadsworth, C.P.",
+ title = {{Edinburgh LCF: A Mechanised Logic of Computation}},
+ comment = "Lecture Notes in Computer Science Volume 78",
+ publisher = "SpringerVerlag",
+ year = "1979"
+}
+
+\end{chunk}
+
\index{Gonshor, H.}
\index{AlgebraGivenByStructuralConstants}
\begin{chunk}{axiom.bib}
@@ 1968,6 +2026,16 @@ paper = "Brea89.pdf"
\subsection{I} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{chunk}{axiom.bib}
+@misc{Isab11,
+ author = "Unknown",
+ title = {{Isabell}},
+ link = "\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html}",
+ year = "2011"
+}
+
+\end{chunk}
+
\subsection{J} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{James, G.}
@@ 2965,6 +3033,16 @@ paper = "Brea89.pdf"
\end{chunk}
+\begin{chunk}{axiom.bib}
+@misc{Poly11a,
+ author = "Unknown",
+ title = {{Poly/ML}},
+ link = "\url{http://www.polyml.org}",
+ year = "2011"
+}
+
+\end{chunk}
+
\subsection{Q} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{chunk}{axiom.bib}
@@ 8877,6 +8955,36 @@ when shown in factored form.
\end{chunk}
+\index{Brown, W.S.}
+\begin{chunk}{axiom.bib}
+@article{Brow69,
+ author = "Brown, W.S.",
+ title = {{Rational Exponential Expressions and a Conjecture Concerning
+ $\pi$ and $e$}},
+ journal = "The American Mathematical Monthly",
+ volume = "76",
+ number = "1",
+ year = "1969",
+ pages = "2834",
+ abstract =
+ "One of the most controversial and least well defined of mathematical
+ problems is the problem of simplification. The recent upsurge
+ of interest in mechanized mathematics has lent new urgency to this
+ problem, but so far very little has been accomplished. This paper
+ attempts to shed light on the situation by introducing the class of
+ rational exponential expressions, defining simplification within
+ this class, and showing constructively how to achieve it. It is shown
+ that the only simplified rational exponential expression equivalent to
+ 0 is 0 itself, provided that an easily stated conjecture is true.
+ However the conjecture, if true, will surely be difficult to prove,
+ since it asserts as a special case that $\pi$ and $e$ are algebraically
+ independent, and no one has yet been able to prove even the much
+ weaker conjecture that $\pi+e$ is irrational.",
+ paper = "Brow69.pdf"
+}
+
+\end{chunk}
+
\index{Clarkson, M.}
\begin{chunk}{axiom.bib}
@article{Clar89,
@@ 10135,6 +10243,33 @@ when shown in factored form.
\end{chunk}
+\index{Benzmuller, Christoph}
+\index{Jamnik, Mateja}
+\index{Kerber, Manfred}
+\index{Sorge, Volker}
+\begin{chunk}{axiom.bib}
+@inproceedings{Benz01,
+ author = "Benzmuller, Christoph and Jamnik, Mateja and Kerber, Manfred
+ and Sorge, Volker",
+ title = {{An Agentoriented Approach to Reasoning}},
+ booktitle = "Proc. Calculemus Workshop 2001",
+ pages = "4863",
+ link = "\url{http://christoph.benzmueller.di/papers/W11.pdf}",
+ year = "2001",
+ abstract =
+ "This paper discusses experiments with an agent oriented approach to
+ automated and interactive reasoning. The approach combines ideas from
+ two subfields of AI (theorem proving/proof planning and multiagent
+ systems) and makes use of state of the art distribution techniques to
+ decentralise and spread its reasoning agents over the internet. It
+ particularly supports cooperative proofs between reasoning systems
+ which are strong in different application areas, e.g., higherorder
+ and firstorder theorem provers and computer algebra systems.",
+ paper = "Benz01.pdf"
+}
+
+\end{chunk}
+
\index{Bertot, Yves}
\index{Cast\'eran, Pierre}
\begin{chunk}{axiom.bib}
@@ 10375,6 +10510,38 @@ when shown in factored form.
\end{chunk}
\index{Boulm\'e, Sylvain}
+\begin{chunk}{axiom.bib}
+@techreport{Boul00a,
+ author = "Boulme. Sylvain",
+ title = {{Specifying in Coq inheritance used in Computer Algebra
+ Libraries}},
+ year = "2000",
+ institution = "LIP6, Paris",
+ number = "2000.013",
+ abstract =
+ "This paper is part of FOC[3], a project for developing Computer
+ Algebra libraries, certified in Coq[2]. FOC has developed a
+ methodology for programming Computer Algebra libraries, using modules
+ and objects in Ocaml. In order to specify modularity features used by
+ FOC in Ocaml, we are coding in Coq a theory for extensible records
+ with dependent fields. This theory intends to express especially the
+ kind of inheritance with method redefinition and late binding, that
+ FOC uses in its Ocaml programs.
+
+ The unit of FOC are coded as records. As we want to encode sematic
+ information on units, the fields of our records may be proofs. Thus,
+ our fields may depend on each others. We call the
+ {\sl Drecords}. Then, we introduce a new datatype, called
+ {\sl mixDrec}, to represent FOC classes. Actually, mixDrecs are useful
+ for describing a hierarchy of Drecords in an incremental way. In
+ mixDrecs, fields can be only declared or they can be
+ redefined. MixDrecs can be extended by inheritance.",
+ paper = "Boul00a.pdf"
+}
+
+\end{chunk}
+
+\index{Boulm\'e, Sylvain}
\index{Hardin, Therese}
\index{Hirschkoff, Daniel}
\index{Rioboo, Renaud}
@@ 10508,6 +10675,53 @@ when shown in factored form.
\end{chunk}
+\index{Boyer, Robert S.}
+\index{Moore, J Strother}
+\begin{chunk}{axiom.bib}
+@techreport{Boye85,
+ author = "Boyer, Robert S. and Moore, J Strother",
+ title = {{Integrating Decision Procedures into Heuristic Theorem Provers}},
+ type = "technical report",
+ institution = "Inst. for Comp. Sci. University of Texas at Austin",
+ number = "ICSCACMP44",
+ year = "1985",
+ abstract =
+ "We discuss the problem of incorporating into a heuristic theorem
+ prover a decision procedure for a fragment of the logic. An obvious
+ goal when incorporating such a procedure is to reduce the search space
+ explored by the heuristic component of the system, as would be
+ achieved by eliminating from the system’s data base some explicitly
+ stated axioms. For example, if a decision procedure for linear
+ inequalities is added, one would hope to eliminate the explicit
+ consideration of the transitivity axioms. However, the decision
+ procedure must then be used in all the ways the eliminated axioms
+ might have been. The difficulty of achieving this degree of
+ integration is more dependent upon the complexity of the heuristic
+ component than upon that of the decision procedure. The view of the
+ decision procedure as a ``black box'' is frequently destroyed by the
+ need pass large amounts of search strategic information back and forth
+ between the two components. Finally, the efficiency of the decision
+ procedure may be virtually irrelevant; the efficiency of the final
+ system may depend most heavily on how easy it is to communicate
+ between the two components. This paper is a case study of how we
+ integrated a linear arithmetic procedure into a heuristic theorem
+ prover. By linear arithmetic here we mean the decidable subset of
+ number theory dealing with universally quantified formulas composed of
+ the logical connectives, the identity relation, the Peano ``less than''
+ relation, the Peano addition and subtraction functions, Peano
+ constants, and variables taking on natural values. We describe our
+ system as it originally stood, and then describe chronologically the
+ evolution of our linear arithmetic procedure and its interface to the
+ heuristic theorem prover. We also provide a detailed description of
+ our final linear arithmetic procedure and the use we make of it. This
+ description graphically illustrates the difference between a
+ standalone decision procedure and one that is of use to a more
+ powerful theorem prover.",
+ paper = "Boye85.pdf"
+}
+
+\end{chunk}
+
\index{Boyer, R.S.}
\index{Moore, J.S.}
\begin{chunk}{axiom.bib}
@@ 10645,6 +10859,36 @@ when shown in factored form.
\end{chunk}
+\index{Buchberger, B.}
+\index{Dupre, C.}
+\index{Jebelean, T.}
+\index{Kriftner, F.}
+\index{Nakagawa, K.}
+\index{Vasaru, D.}
+\index{Windsteiger, W.}
+\begin{chunk}{axiom.bib}
+@misc{Buch00,
+ author = "Buchberger, B. and Dupre, C. and Jebelean, T. and Kriftner, F.
+ and Nakagawa, K. and Vasaru, D. and Windsteiger, W.",
+ title = {{The Theorema Project: A Progress Report}},
+ year = "2000",
+ abstract =
+ "The THEOREMA project aims at supporting, within one consistent logic
+ and one coherent software system, the entire mathematical exploration
+ cycle including the phase of proving. In this paper we report on some
+ of the new features of THEOREMA that have been designed and
+ implemented since the first expository version of THEOREMA in
+ 1997. These features are:  the THEOREMA formal text language  the
+ THEOREMA computational sessions  the ProveComputeSolve (PCS) prover
+ of THEOREMA  the THEOREMA set theory prover  special provers within
+ THEOREMA  the cascademetastrategy for THEOREMA provers  proof
+ simplification in THEOREMA. In the conclusion, we formulate design
+ goals for the next version of THEOREMA",
+ paper = "Buch00.pdf"
+}
+
+\end{chunk}
+
\index{Buchberger,B}
\index{Craciun, A.}
\index{Jebelean, T.}
@@ 11639,6 +11883,43 @@ when shown in factored form.
\end{chunk}
+\index{Dennis, Louise A.}
+\index{Collins, Graham}
+\index{Norrish, Michael}
+\index{Boulton, Richard}
+\index{Slind, Konrad}
+\index{Robinson, Graham}
+\index{Gordon, Mike}
+\index{Melham, Tom}
+\begin{chunk}{axiom.bib}
+@article{Denn00,
+ author = "Dennis, Louise A. and Collins, Graham and Norrish, Michael
+ and Boulton, Richard and Slind, Konrad and
+ Robinson, Graham and Gordon, Mike and Melham, Tom",
+ title = {{The PROSPER Toolkit}},
+ journal = "LNCS",
+ volume = "1785",
+ publisher = "SpringerVerlag",
+ pages = "7892",
+ year = "2000",
+ link =
+ "\url{https://link.springer.com/content/pdf/10.1007/3540464190_7.pdf}",
+ abstract =
+ "The PROSPER (Proof and Specification Assisted Design Environments)
+ project advocates the use of toolkits which allow existing
+ verification tools to be adapted to a more flexible format so that
+ they may be treated as components. A system incorporating such tools
+ becomes another component that can be embedded in an application. This
+ paper describes the PROSPER Toolkit which enables this. The nature of
+ communication between components is specified in a
+ languageindependent way. It is implemented in several common
+ programming languages to allow a wide variety of tools to have access
+ to the toolkit.",
+ paper = "Denn00.pdf"
+}
+
+\end{chunk}
+
\index{Devlin, Keith J.}
\begin{chunk}{axiom.bib}
@book{Devl79,
@@ 11891,6 +12172,85 @@ when shown in factored form.
\subsection{F} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\index{Farmer, William H.}
+\begin{chunk}{axiom.bib}
+@article{Farm92a,
+ author = "Farmer, William H.",
+ title = {{IMPS: System Description}},
+ journal = "Lecture Notes in Computer Science",
+ volume = "607",
+ pages = "701705",
+ year = "1992",
+ paper = "Farm92a.pdf"
+}
+
+\end{chunk}
+
+\index{Farmer, William M.}
+\index{Guttman, Joshua D.}
+\index{Fabrega, F. Javier Thayer}
+\begin{chunk}{axiom.bib}
+@article{Farm96,
+ author = "Farmer, William M. and Guttman, Joshua D. and
+ Fabrega, F. Javier Thayer",
+ title = {{IMPS: An Updated System Description}},
+ journal = "LNCS",
+ volume = "1104",
+ pages = "298302",
+ year = "1996",
+ paper = "Farm96.pdf"
+}
+
+\end{chunk}
+
+\index{Farmer, William H.}
+\begin{chunk}{axiom.bib}
+@article{Farm92,
+ author = "Farmer, William H.",
+ title = {{Little Theories}},
+ journal = "LNCS",
+ volume = "607",
+ year = "1992",
+ pages = "567581",
+ abstract =
+ "In the ``little theories'' version of the axiomatic method, different
+ portions of mathematics are developed in various different formal
+ axiomatic theories. Axiomatic theories may be related by inclusion or
+ by theory interpretation. We argue that the little theories approach
+ is a desirable way to formalize mathematics, and we describe how IMPS,
+ an Interactive Mathematical Proof System, supports it.",
+ paper = "Farm92.pdf"
+}
+
+\end{chunk}
+
+\index{Farmer, William M.}
+\begin{chunk}{axiom.bib}
+@article{Farm93b,
+ author = "Farmer, William M.",
+ title = {{A simple type theory with partial functions and subtypes}},
+ journal = "Annals of Pure and Applied Logic",
+ volume = "64",
+ pages = "211240",
+ year = "1993",
+ abstract =
+ "Simple type theory is a higherorder predicate logic for reasoning
+ about truth values, individuals, and simply typed total functions. We
+ present in this paper a version of simple type theory, called PF*, in
+ which functions may be partial and types may have subtypes. We define
+ both a Henkinstyle general models semantics and an axiomatic system
+ for PF*, and we prove that the axiomatic system is complete with
+ respect to the general models semantics. We also define a notion of
+ an interpretation of one PF* theory in another. PF* is intended as a
+ foundation for mechanized mathematics. It is the basis for the logic
+ of IMPS, an Interactive Mathematical Proof System developed at The
+ MITRE Corporation.",
+ paper = "Farm93b.pdf"
+}
+
+\end{chunk}
+
\index{Farmer, William M.}
\index{Guttman, Joshua D.}
\index{Thayer, Javier}
@@ 11941,6 +12301,27 @@ when shown in factored form.
\end{chunk}
+\index{Farmer, William M.}
+\index{Guttman, Joshua D.}
+\index{Nadel, Mark E.}
+\index{Fabrega, F. Javier Thayer}
+\begin{chunk}{axiom.bib}
+@article{Farm94,
+ author = "Farmer, William M. and Guttman, Joshua D. and Nadel, Mark E.
+ and Fabrega, F. Javier Thayer",
+ title = {{Proof Script Pragmatics in IMPS}},
+ journal = "LNCS",
+ volume = "814",
+ pages = "356370",
+ year = "1994",
+ abstract =
+ "This paper instroduces the IMPS proof script mechanism and some
+ practical methods for exploiting it.",
+ paper = "Farm94.pdf"
+}
+
+\end{chunk}
+
\index{Fateman, Richard J.}
\begin{chunk}{axiom.bib}
@misc{Fate02a,
@@ 12526,6 +12907,32 @@ when shown in factored form.
\index{Harrison, John}
\index{Th\'ery, Laurent}
\begin{chunk}{axiom.bib}
+@incollection{Harr93,
+ author = "Harrison, John and Thery, Laurent",
+ title = {{Reasoning about the Reals: The Marriage of HOL and
+ Maple}},
+ booktitle = "Logic Programming and Automated Reasoning",
+ publisher = "SpringerVerlag",
+ year = "1993",
+ pages = "351353",
+ link =
+ "\url{https://link.springer.com/content/pdf/10.1007/3540569448_68.pdf}",
+ abstract =
+ "Computer algebra systems are extremely powerful and flexible, but
+ often give results which require careful interpretation or are
+ downright incorrect. By contrast, theorem provers are very reliable
+ but lack the powerful specialized decision procedures and heuristics
+ of computer algebra systems. In this paper we try to get the best of
+ both worlds by careful exploitation of a link between a theorem prover
+ and a computer algebra system.",
+ paper = "Harr93.pdf"
+}
+
+\end{chunk}
+
+\index{Harrison, John}
+\index{Th\'ery, Laurent}
+\begin{chunk}{axiom.bib}
@inproceedings{Harr94,
author = "Harrison, John and Thery, Laurent",
title = {{Extending the HOL Thoerem Prover with a Computer Algebra System
@@ 12549,7 +12956,7 @@ when shown in factored form.
\begin{chunk}{axiom.bib}
@techreport{Harr95,
author = "Harrison, John",
 title = {{Methatheory and Reflection in Theorem Proving: A Survey
+ title = {{Metatheory and Reflection in Theorem Proving: A Survey
and Critique}},
institution = "SRI Cambridge",
year = "1995",
@@ 12731,6 +13138,7 @@ when shown in factored form.
author = "Homann, Karsten",
title = {{Symbolisches L\"osen mathematischer Probleme durch
Kooperation algorithmischer und logischer Systeme}},
+ comment = {{Symboic Mathematical Problem Solving by Cooperation of Algorithmic and Logical Services (in German)}},
year = "1996",
school = {Universit\"at Karlsruhe},
paper = "Homa96a.pdf"
@@ 14463,6 +14871,24 @@ when shown in factored form.
\end{chunk}
+\index{Owre, S.}
+\index{Rushby, J.M.}
+\index{Shankar, N.}
+\begin{chunk}{axiom.bib}
+@article{Owre92,
+ author = "Owre, S. and Rushby, J.M. and Shankar, N.",
+ title = {{PVS: A Prototype Verification System}},
+ journal = "Lecture Notes in Computer Science",
+ volume = "687",
+ pages = "748752",
+ year = "1992",
+ abstract =
+ "This brief paper introduces the main ideas of PVS",
+ paper = "Owre92.pdf"
+}
+
+\end{chunk}
+
\subsection{P} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Padawitz, Peter}
@@ 14764,13 +15190,25 @@ when shown in factored form.
\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
\incollection{Pfen92,
+@misc{Pfen17,
+ author = "Pfenning, Frank",
+ title = {{Logical Frameworks}},
+ link = "\url{http://www.cs.cmu.edu/afs/cs.cmu.edu/user/fp/www/lfs.html}",
+ year = "2017"
+}
+
+\end{chunk}
+
+\index{Pfenning, Frank}
+\begin{chunk}{axiom.bib}
+@incollection{Pfen92a,
author = "Pfenning, Frank",
title = {{Dependent Types in Logic Programming}},
booktitle = "Types in Logic Programming",
isbn = "9780262161312",
publisher = "MIT Press",
 year = "1992"
+ year = "1992",
+ paper = "Pfen92a.pdf"
}
\end{chunk}
@@ 15360,6 +15798,16 @@ when shown in factored form.
\subsection{T} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{chunk}{axiom.bib}
+@misc{Theo17,
+ author = "Unknown",
+ title = {{Theorema Project}},
+ link = "\url{http://www.theorema.org}",
+ year = "2017"
+}
+
+\end{chunk}
+
\index{Th\'ery, Laurent}
\begin{chunk}{axiom.bib}
@article{Ther01,
@@ 24225,6 +24673,16 @@ Proc ISSAC 97 pp172175 (1997)
\end{chunk}
+\begin{chunk}{axiom.bib}
+@misc{Open11,
+ author = "Dos Reis, G.",
+ title = {{OpenAxiom}},
+ link = "\url{http://www.openaxiom.org}",
+ year = "2011"
+}
+
+\end{chunk}
+
\index{Wester, Michael J.}
\begin{chunk}{axiom.bib}
@misc{West95,
@@ 32686,33 +33144,6 @@ ISBN 1581130732 LCCN QA76.95.I57 1999
\end{chunk}
\index{Dos Reis, Gabriel}
\index{Matthews, David}
\index{Li, Yue}
\begin{chunk}{axiom.bib}
@article{Reis11,
 author = "Dos Reis, Gabriel",
 title = {{Retargeting OpenAxiom to Poly/ML: towards an integrated proof
 assistants and computer algebra system framework}},
 journal = "Intelligent computer mathematics (MKM 2011)",
 year = "2011",
 isbn = "9783642226724",
 link = "\url{https://www.semanticscholar.org/paper/RetargetingOpenAxiomtoPolyMLTowardsanReisMatthews/4ce5d85ea8424ced82d}",
 abstract =
 "This paper presents an ongoing effort to integrate the AXIOM family
 of computer algebra systems with Poly/MLbased proof assistants in the
 same framework. A longterm goal is to make a large set of efficient
 implementations of algebraic algorithms available to popular proof
 assistants, and also to bring the power of mechanized formal
 verification to a family of strongly typed computer algebra systems at
 a modest cost. Our approach is based on retargeting the code generator
 of the OpenAxiom compiler to the Poly/ML abstract machine.",
 paper = "Reis11.pdf",
 keywords = "axiomref"
}

\end{chunk}

\index{Dos Reis, Gabriel}
\index{Stroustrup, Bjarne}
\begin{chunk}{axiom.bib}
@article{Reis06,
@@ 46641,6 +47072,19 @@ Ginn \& Co., Boston and New York. (1962)
\end{chunk}
+\index{Bogen, Richard}
+\begin{chunk}{axiom.bib}
+@book{Boge77,
+ author = "Bogen, Richard",
+ title = {{MACSYMA Reference Manual, Version 9}},
+ publisher = "MIT",
+ year = "1977",
+ link = "\url{http://bitsavers.informatik.unistuttgart.de/pdf/mit/macsyma/MACSYMA_RefMan_V9_Dec77.pdf}",
+ paper = "Boge77.pdf"
+}
+
+\end{chunk}
+
\index{Boyd, David W.}
\begin{chunk}{ignore}
\bibitem[Boyd9 3a]{Boyd93a} Boyd, David W.
@@ 47242,6 +47686,21 @@ GauthierVillars, Paris, 1891).
\end{chunk}
+\index{Cherlin, Gregory}
+\begin{chunk}{axiom.bib}
+@article{Cher80,
+ author = "Cherlin, Gregory",
+ title = {{Rings of Continuous Functions: Decision Problems}},
+ journal = "Lecture Notes in Mathematics",
+ volume = "834",
+ pages = "4491",
+ year = "1980",
+ link = "\url{https://link.springer.com/content/pdf/10.1007/BFb0090160.pdf}",
+ paper = "Cher80.pdf"
+}
+
+\end{chunk}
+
\index{Chew, Paul}
\index{Constable, Robert L.}
\index{Pingali, Keshav}
@@ 47581,6 +48040,25 @@ J. Inst. Math. Appl. 21 135143. (1978)
\end{chunk}
+\index{Craigen, Dan}
+\index{Kromodimoeljo, Sentot}
+\index{Meisels, Irwin}
+\index{Pase, Bill}
+\index{Saaltink, Mark}
+\begin{chunk}{axiom.bib}
+@article{Crai92,
+ author = "Craigen, Dan and Kromodimoeljo, Sentot and Meisels, Irwin
+ and Pase, Bill",
+ title = {{Eves System Description}},
+ journal = "Lecture Notes in Computer Science",
+ volume = "607",
+ pages = "771775",
+ year = "1992",
+ paper = "Crai92.pdf"
+}
+
+\end{chunk}
+
\index{Cunningham, R.J.}
\index{Dick, A.J.J}
\begin{chunk}{axiom.bib}
@@ 47813,6 +48291,19 @@ PrenticeHall.(1983)
\end{chunk}
+\index{Dewar, Mike}
+\begin{chunk}{axiom.bib}
+@misc{Dewa00,
+ author = "Dewar, Mike",
+ title = {{Special Issue on OPENMATH}},
+ publisher = "ACM SIGPLAN Bulletin",
+ volume = "34",
+ number = "2",
+ year = "2000"
+}
+
+\end{chunk}
+
\index{Dierckx, P.}
\begin{chunk}{ignore}
\bibitem[Dierckx 75]{Die75} Dierckx P
@@ 48976,6 +49467,42 @@ Grove, IL, USA and Oxford, UK, 1992
\end{chunk}
+\index{Gray, Simon}
+\index{Kajler, Norbert}
+\index{Wang, Paul S.}
+\begin{chunk}{axiom.bib}
+@article{Gray98,
+ author = "Gray, Simon and Kajler, Norbert and Wang, Paul S.",
+ title = {{Design and Implementation of MP, a Protocol for
+ Efficient Exchange of Mathematical Expressions}},
+ journal = "J. Symboic Computation",
+ volume = "25",
+ pages = "213237",
+ year = "1998",
+ abstract =
+ "The Multi Project is an ongoing research e ort at Kent State
+ University aimed at providing an environment for distributed scientific
+ computing. An integral part of this environment is the Multi
+ Protocol (MP) which is designed to support ecientific communication of
+ mathematical data between scientificallyoriented software tools. MP
+ exchanges data in the form of linearized annotated syntax
+ trees. Syntax trees provide a simple, flexible and toolindependent
+ way to represent and exchange data, and annotations provide a powerful
+ and generic expressive facility for transmitting additional
+ information. At a level above the data exchange protocol,
+ dictionaries provide definitions for operators and constants, providing
+ shared semantics across heterogeneous packages. A clear distinction
+ between MPdefined and userdefined entities is enforced. Binary
+ encodings are used for efficiency. Commonly used values and blocks of
+ homogeneous data are further optimized. The protocol is independent of
+ the underlying communication paradigm and can support parallel
+ computation, distributed problemsolving environments, and the
+ coupling of tools for speci c applications.",
+ paper = "Gray98.pdf"
+}
+
+\end{chunk}
+
\index{Griss, Martin L.}
\begin{chunk}{axiom.bib}
@inproceedings{Gris76,
@@ 49049,6 +49576,19 @@ Grove, IL, USA and Oxford, UK, 1992
\end{chunk}
+\index{Guttman, J.D.}
+\begin{chunk}{axiom.bib}
+@techreport{Gutt91,
+ author = "Guttman, J.D.",
+ title = {{A Propoed Interface Logic for Verification Environments}},
+ type = "technical report",
+ number = "M9119",
+ institution = "The MITRE Corporation",
+ year = "1991"
+}
+
+\end{chunk}
+
\subsection{H} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{GeneralPackageForAlgebraicFunctionField}
@@ 50789,6 +51329,61 @@ Mathematical Surveys. 3 Am. Math. Soc., Providence, RI. (1966)
\end{chunk}
+\index{Matthews, David C.J.}
+\index{Wenzel, Makarius}
+\begin{chunk}{axiom.bib}
+@inproceedings{Matt10,
+ author = "Matthews, David C.J. and Wenzel, Makarius",
+ title = {{Efficient Parallel Programming in Poly/ML and Isabelle/ML}},
+ booktitle = "Proc. 5th ACM SIGPLAN workshop on Declarative aspects of
+ multicore programming",
+ pages = "5362",
+ year = "2010",
+ publisher = "ACM",
+ isbn = "9781605588599",
+ abstract =
+ "The ML family of languages and LCFstyle interactive theorem proving
+ have been closely related from their beginnings about 30 years
+ ago. Here we report on a recent project to adapt both the Poly/ML
+ compiler and the Isabelle theorem prover to current multicore
+ hardware. Checking theories and proofs in typical Isabelle application
+ takes minutes or hours, and users expect to make efficient use of
+ ``home machines'' with 28 cores, or more.
+
+ Poly/ML and Isabelle are big and complex software systems that have
+ evolved over more than two decades. Faced with the requirement to
+ deliver a stable and efficient parallel programming environment, many
+ infrastructure layers had to be reworked: from lowlevel system
+ threads to highlevel principles of valueoriented programming. At
+ each stage we carefully selected from the many existing concepts for
+ parallelism, and integrated them in a way that fits smoothly into the
+ idea of purely functional ML with the addition of synchronous
+ exceptions and asynchronous interrupts.
+
+ From the Isabelle/ML perspective, the main concept to manage parallel
+ evaluation is that of ``future values''. Scheduling is implicit, but it
+ is also possible to specify dependencies and priorities. In addition,
+ blockstructured groups of futures with propagation of exceptions
+ allow for alternative functional evaluation (such as parallel search),
+ without requiring user code to tackle concurrency. Our library also
+ provides the usual parallel combinators for functions on lists, and
+ analogous versions on prover tactics.
+
+ Despite substantial reorganization in the background, only minimal
+ changes are occasionally required in user ML code, and none at the
+ Isabelle application level (where parallel theory and proof processing
+ is fully implicit). The present implementation is able to address more
+ than 8 cores effectively, while the earlier version of the official
+ Isabelle2009 release works best for 24 cores. Scalability beyond 16
+ cores still poses some extra challenges, and will require further
+ improvements of the Poly/ML runtime system (heap management and
+ garbage collection), and additional parallelization of Isabelle
+ application logic.",
+ paper = "Matt10.pdf"
+}
+
+\end{chunk}
+
\begin{chunk}{axiom.bib}
@misc{Maxi16a,
author = "Maxima",
@@ 50800,7 +51395,7 @@ Mathematical Surveys. 3 Am. Math. Soc., Providence, RI. (1966)
\index{Mayrhofer, Gunther}
\begin{chunk}{axiom.bib}
@phdthsis{Mayr09,
+@phdthesis{Mayr09,
author = "Mayrhofer, Gunther",
title = {{Symbolic COmputation Prover with Induction}},
year = "2009",
@@ 51618,6 +52213,33 @@ J. Inst. Maths Applics. 8 1635. (1971)
\end{chunk}
\index{Pfenning, Frank}
+\index{Rohwedder, Ekkehard}
+\begin{chunk}{axiom.bib}
+@article{Pfen92b,
+ author = "Pfenning, Frank and Rohwedder, Ekkehard",
+ title = {{Implementing the MetaTheory of Deductive Systems}},
+ journal = "Lecture Notes in Computer Science",
+ volume = "607",
+ pages = "771775",
+ year = "1992",
+ abstract =
+ "We exhibit a methodology for formulating and verifying meta theorems
+ about deductive systems in the Elf language, an implementation of the
+ LF Logical Framework with an operational semantics in the spirit of
+ logic programming. It is based on the mechanical verification of
+ properties of transformations between deductions, which relies on type
+ reconstruction and schemachecking. The latter is justified by
+ induction principles for closed LF objects, which can be constructed
+ over a given signature. We illustrate our technique through several
+ examples, the most extensive of which is an interpre tation of
+ classical logic in minimal logic through a continuationpassingstyle
+ transformation on proofs.",
+ paper = "Pfen92b.pdf"
+}
+
+\end{chunk}
+
+\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@misc{Pfen97,
author = "Pfenning, Frank",
@@ 52059,6 +52681,29 @@ Proc. AMS Vol 117 No 4 April 1993
\end{chunk}
+\index{Richardson, Daniel}
+\begin{chunk}{axiom.bib}
+@article{Rich69,
+ author = "Richardson, Daniel",
+ title = {{Some Undecidable Problems involving Elementar Functions of
+ a Real Variable}},
+ journal = "J. Symbolic Logic",
+ volume = "33",
+ number = "4",
+ year = "1969",
+ pages = "514520",
+ abstract =
+ "Let $E$ be a set of expressions representing real, single valued,
+ partially defined functions of one real variable. $E^*$ will be the
+ set of functions represented by expressions in $E$. If $A$ is an
+ expression in $E$, $A(x)$ is the function denoted by $AA$. It is
+ assumed that $D^*$ contains the identity function and the rational
+ numbers as constant functions and that $E^*$ is closed under addition,
+ subtraction, multiplication, and composition"
+}
+
+\end{chunk}
+
\index{Richardson, Dan}
\index{Fitch, John P.}
\begin{chunk}{axiom.bib}
@@ 52209,6 +52854,20 @@ April 2007
\end{chunk}
+\index{Rushby, John}
+\begin{chunk}{axiom.bib}
+@inproceedings{Rush00,
+ author = "Rushby, John",
+ title = {{Disappearing Formal Methods}},
+ booktitle = "High Assurance Systems Engineering, 5th Int. Symp.",
+ pages = "9596",
+ year = "2000",
+ publisher = "ACM",
+ paper = "Rush00.pdf"
+}
+
+\end{chunk}
+
\index{Rutishauser, H.}
\begin{chunk}{ignore}
\bibitem[Rutishauser 69]{Rut69} Rutishauser H.
@@ 52336,6 +52995,18 @@ Num. Math. 16 205223. (1970)
\end{chunk}
+\index{Schelter, William F.}
+\begin{chunk}{axiom.bib}
+@book{Sche01,
+ author = "Schelter, William F.",
+ title = {{Maxima Manual Version 5.41.0}},
+ year = "2001",
+ publisher = "Sourceforge",
+ paper = "Sche01.pdf"
+}
+
+\end{chunk}
+
\index{Schreiner, Wolfgang}
\begin{chunk}{axiom.bib}
@techreport{Schr09,
@@ 53205,6 +53876,20 @@ Van Nostrand. (1967)
\end{chunk}
+\index{Wos, Larry}
+\begin{chunk}{axiom.bib}
+@article{Wosx92,
+ author = "Wos, Larry",
+ title = {{The Impossibility of the Automation of Logical Reasoning}},
+ journal = "Lecture Notes in Computer Science",
+ volume = "607",
+ year = "1992",
+ pages = "13",
+ paper = "Wosx92.pdf"
+}
+
+\end{chunk}
+
\index{Wu, Wentsun}
\begin{chunk}{axiom.bib}
@book{Wuxx94,
diff git a/changelog b/changelog
index 70c7924..73dd774 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20171115 tpd src/axiomwebsite/patches.html 20171115.01.tpd.patch
+20171113 tpd books/bookvolbib add references
20171113 tpd src/axiomwebsite/patches.html 20171113.01.tpd.patch
20171113 tpd books/bookvolbib add references
20171109 tpd src/axiomwebsite/patches.html 20171109.01.tpd.patch
diff git a/patch b/patch
index be5dc91..0024a85 100644
 a/patch
+++ b/patch
@@ 2,1080 +2,634 @@ books/bookvolbib add references
Goal: Proving Axiom Correct
\begin{chunk}{axiom.bib}
@misc{SCSCP,
 author = "The SCSCP development team",
 title = {{Symbolic Computation Software Composability Protocol}},
 link = "\url{https://gappackages.github.io/scscp/}",
 year = "2017"
}

\end{chunk}

\index{Gonthier, Georges}
\index{Mahboubi, Assia}
\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@techreport{Gont09,
 author = "Gonthier, Georges and Mahboubi, Assia and Tassi, Enrico",
 title = {{A Small Scale Reflection Extension for the Coq System}},
 type = "technical report",
 institution = "Inria Microsoft",
 number = "RR6455",
 year = "2009",
 abstract =
 "This is the user manual de SSReflect , a set of extensions to the
 proof scripting language of the Coq proof assistant. While these
 extensions were developed to support a particular proof methodology 
 smallscale reflection  most of them actually are of a quite general
 nature, improving the functionality of Coq in basic areas such as
 script layout and structuring, proof context management, and
 rewriting. Consequently, and in spite of the title of this document,
 most of the extensions described here should be of interest for all
 Coq users, whether they embrace smallscale reflection or not.",
 paper = "Gont09.pdf"

}

\end{chunk}

\index{Garillot, Francois}
\index{Gonthier, Georges}
\index{Mahboubi, Assia}
\index{Rideau, Laurence}
\begin{chunk}{axiom.bib}
@misc{Gari09,
 author = "Garillot, Francois and Gonthier, Georges and Mahboubi, Assia and
 Rideau, Laurence",
 title = {{Packaging Mathematical Structures}},
 year = "2009",
 abstract =
 "This paper proposes generic design patterns to define and combine
 algebraic structures, using dependent records, coercions and type
 inference, inside the Coq system. This alternative to telescopes in
 particular allows multiple inheritance, maximal sharing of notations
 and theories, and automated structure inference. Our methodology is
 robust enough to support a hierarchy comprising a broad variety of
 algebraic structures, from types with a choice operator to algebraically
 closed fields. Interfaces for the structures enjoy the handiness of a
 classi cal setting, without requiring any axiom. Finally, we show how
 externally extensible some of these instances are by discussing a
 lemma seminal in defining the discrete logarithm, and a matrix
 decomposition problem.",
 paper = "Gari09.pdf"
}

\end{chunk}

\begin{chunk}{axiom.bib}
@misc{GAPx17,
 author = "The GAP Team",
 title = {{GAP  Groups, Algorithms, Programming}},
 year = "2017",
 link = "\url{https://www.gapsystem.org/}"
}

\end{chunk}

\index{Meindl, Diana}
\begin{chunk}{axiom.bib}
@mastersthesis{Mein13,
 author = "Meindl, Diana",
 title = {{Implementation of an Algorithm Computing the Greatest
 Common Divisor for Multivariate Polynomials}},
 year = "2013",
 school = "RISC Linz"
}

\end{chunk}

\index{Neuper, Walther}
\begin{chunk}{axiom.bib}
@article{Meup13a,
 author = "Neuper, Walther",
 title = {{On the Emergence of TPbased Educational Math
 Assistants}},
 journal = "The Electronic Journal of Mathematics and Technology",
 volume = "1",
+\index{Brown, W.S.}
+\begin{chunk}{axiom.bib}
+@article{Brow69,
+ author = "Brown, W.S.",
+ title = {{Rational Exponential Expressions and a Conjecture Concerning
+ $\pi$ and $e$}},
+ journal = "The American Mathematical Monthly",
+ volume = "76",
number = "1",
 year = "2013",
 link = "\url{http://www.ist.tugraz.at/projects/isac/publ/newgen.pdf}",
 abstract =
 "Presently Computer Algebra Systems, Dynamic Geometry Systems and
 Spreadsheets cover most of elearning in highschool mathematics and
 as well are used for education in formal parts of science. Recently
 and largely unnoticed in public, the academic discipline of
 interactive and automated Theorem Proving (TP) has become of major
 importance for mathematics and computer science.

 This paper considers the promises of TP technology for education in
 science, technology, engineering and mathematics at the full range of
 levels from highschool to university.

 Starting from prototypes of TPbased educational mathematics systems,
 conceptual founda tions are considered: TPbased software which
 implements reasoning as an essential part of math ematical thinking
 technology. Educational objectives for the development of TPbased
 systems are discussed and concluded with some predictions on possible
 impact of TPbased educational mathematics assistants.

 The final conclusion suggests to announce the emergence of a new,
 TPbased generation of educational mathematics software.",
 paper = "Neup13a.pdf"
}

\end{chunk}

\index{Maletzky, Alexander}
\begin{chunk}{axiom.bib}
@techreport{Male17,
 author = "Maletzky, Alexander",
 title = {{A New Reasoning Framework for Theorema 2.0}},
 year = "2017",
 institution = "RISC Linz",
+ year = "1969",
+ pages = "2834",
abstract =
 "We present a new addon for the Theorema 2.0 proof assistant,
 consisting of a reasoning framework in the spirit of (though not
 exactly as) the wellknown LCF approach to theorem proving: a small,
 trusted kernel of basic inferences complemented by an extensive
 collection of automatic and interactive proof methods that construct
 proofs solely in terms of the basic inferences. We explain why such an
 approach is desirable in the first place in Theorema (at least as a
 possible alternative to the existing paradigm), how it fits together
 with the current default setup of the system, and how proofchecking
 with the inference kernel of the new framework proceeds. Since all
 this is heavily inspired by the Isabelle proof assistant, we in
 particular also highlight the differences between Isabelle and our
 approach.",
 paper = "Male17.pdf"
+ "One of the most controversial and least well defined of mathematical
+ problems is the problem of simplification. The recent upsurge
+ of interest in mechanized mathematics has lent new urgency to this
+ problem, but so far very little has been accomplished. This paper
+ attempts to shed light on the situation by introducing the class of
+ rational exponential expressions, defining simplification within
+ this class, and showing constructively how to achieve it. It is shown
+ that the only simplified rational exponential expression equivalent to
+ 0 is 0 itself, provided that an easily stated conjecture is true.
+ However the conjecture, if true, will surely be difficult to prove,
+ since it asserts as a special case that $\pi$ and $e$ are algebraically
+ independent, and no one has yet been able to prove even the much
+ weaker conjecture that $\pi+e$ is irrational.",
+ paper = "Brow69.pdf"
}
\end{chunk}
\index{Neuper, Walther}
+\index{Bogen, Richard}
\begin{chunk}{axiom.bib}
@misc{Neup12,
 author = "Neuper, Walther",
 title = {{Automated Generation of User Guidance by Combining
 Computation and Deduction}},
 year = "2012",
 publisher = "Open Publishing Association",
 pages = "82101",
 abstract =
 "Herewith, a fairly old concept is published for the first time and
 named ”Lucas Interpretation”. This has been implemented in a
 prototype, which has been proved useful in educational practice and
 has gained academic relevance with an emerging generation of
 educational mathematics assistants (EMA) based on Computer Theorem
 Proving (CTP).

 Automated Theorem Proving (ATP), i.e. deduction, is
 the most reliable technology used to check user input. However ATP is
 inherently weak in automatically generating solutions for arbitrary
 problems in applied mathematics. This weakness is crucial for EMAs:
 when ATP checks user input as incorrect and the learner gets stuck
 then the system should be able to suggest possible next steps.

 The key idea of Lucas Interpretation is to compute the steps of a
 calculation following a pro gram written in a novel CTPbased
 programming language, i.e. computation provides the next steps. User
 guidance is generated by combining deduction and computation: the
 latter is performed by a specific language interpreter, which works
 like a debugger and hands over control to the learner at breakpoints,
 i.e. tactics generating the steps of calculation. The interpreter
 also builds up logical contexts providing ATP with the data required
 for checking user input, thus combining computation and deduction.

 The paper describes the concepts underlying Lucas Interpretation so
 that open questions can adequately be addressed, and prerequisites for
 further work are provided.",
 paper = "Neup12.pdf"
+@book{Boge77,
+ author = "Bogen, Richard",
+ title = {{MACSYMA Reference Manual, Version 9}},
+ publisher = "MIT",
+ year = "1977",
+ link = "\url{http://bitsavers.informatik.unistuttgart.de/pdf/mit/macsyma/MACSYMA_RefMan_V9_Dec77.pdf}",
+ paper = "Boge77.pdf"
}
\end{chunk}
\index{Buchberger, Bruno}
+\index{Schelter, William F.}
\begin{chunk}{axiom.bib}
@article{Buch01,
 author = "Buchberger, Bruno",
 title = {{Theorema: A Proving System Based on Mathematica}},
 journal = "The Mathematica Journal",
 volume = "8",
 number = "2",
 pages = "247252",
+@book{Sche01,
+ author = "Schelter, William F.",
+ title = {{Maxima Manual Version 5.41.0}},
year = "2001",
 paper = "Buch01.pdf"
}

\end{chunk}

\index{Giese, Martin}
\begin{chunk}{axiom.bib}
@inproceedings{Gies05,
 author = "Giese, Martin",
 title = {{A Calculus for Type Predicates and Type Coercion}},
 booktitle = "A Calculus for Type Predicates and Type Coercion",
 series = "LNAI",
 volume = "3702",
 pages = "123137",
 isbn = "3540289313",
 abstract =
 "We extend classical firstorder logic with subtyping by type
 predicates and type coercion. Type predicates assert that the value of
 a term belongs to a more special type than the signature guarantees,
 while type coercion allows using terms of a more general type where
 the signature calls for a more special one. These operations are
 important e.g. in the specification and verification of
 objectoriented programs. We present a tableau calculus for this logic
 and prove its completeness.",
 paper = "Gies05.pdf"
}

\end{chunk}

\index{Buchberger, Bruno}
\index{Aigner, K.}
\index{Dupre, C.}
\index{Jebelean, T.}
\index{Kriftner, F.}
\index{Marin, M.}
\index{Nakagawa, K.}
\index{Podisor, O.}
\index{Tomuta, E.}
\index{Usenko, Y.}
\index{Vasaru, D.}
\index{Windsteiger, W.}
\begin{chunk}{axiom.bib}
@misc{Buch03,
 author = "Buchberger, Bruno",
 title = {{Theorema: An Integrated System for Computation and
 Deduction in Natural Style}},
 abstract =
 "The Theorema project aims at integrating computation and deduction in
 a system that can be used by the working scientist for build ing and
 checking mathematical models, including the design and verica tion of
 new algorithms. Currently, the system uses the rewrite engine of the
 computer algebra system Mathematica for building and combining a
 number of automatic/interactive provers (highorder predicatelogic,
 in duction for lists/tuples and natural numbers, etc.) in natural
 deduction style and in natural language presentation. These provers
 can be used for dening and proving properties of mathematical models
 and algorithms, while a specially provided \computing engine" can
 execute directly the logical description of these algorithms.",
 paper = "Buch03.pdf"
}

\end{chunk}

\index{Nilsson, Nils J.}
\begin{chunk}{axiom.bib}
@book{Nils76,
 author = "Nilsson, Nils J.",
 title = {{Principles of Artificial Intelligence}},
 publisher = "Morgan Kaufmann",
 year = "1976",
 abstract =
 "A classic introduction to artificial intelligence intended to bridge
 the gap between theory and practice, Principles of Artificial
 Intelligence describes fundamental AI ideas that underlie applications
 such as natural language processing, automatic programming, robotics,
 machine vision, automatic theorem proving, and intelligent data
 retrieval. Rather than focusing on the subject matter of the
 applications, the book is organized around general computational
 concepts involving the kinds of data structures used, the types of
 operations performed on the data structures, and the properties of the
 control strategies used. Principles of Artificial Intelligenceevolved
 from the author's courses and seminars at Stanford University and
 University of Massachusetts, Amherst, and is suitable for text use in
 a senior or graduate AI course, or for individual study."
}

\end{chunk}

\index{Tomuta, E.}
\begin{chunk}{axiom.bib}
@phdthesis{Tomu98,
 author = "Tomuta, E.",
 title = {{Proof Control in the Theorema Project}},
 year = "1998",
 school = "RISC Linz"
}

\end{chunk}

\index{Markov, A.A.}
\begin{chunk}{axiom.bib}
@incollection{Mark62,
 author = "Markov, A.A.",
 title = {{On Constructive Mathematics}},
 booktitle = "Problems of the Constructive Direction in Mathematics:
 Part 2  Constructive Mathematical Analysis",
 publisher = "Academy of Science USSR",
 comment = "In Russian",
 link = "\url{http://www.mathnet.ru/links/4fe363fcbbf9aeaad8dc9baed1c7d1c8/tm1756.pdf}",
 year = "1962"
+ publisher = "Sourceforge",
+ paper = "Sche01.pdf"
}
\end{chunk}
\index{Kreinovich, Vladik}
+\index{Farmer, William M.}
+\index{Guttman, J.D.}
+\index{Thayer, F.J.}
\begin{chunk}{axiom.bib}
@misc{Krei14,
 author = "Kreinovich, Vladik",
 title = {{Constructive Mathematics in St. Petersburg, Russia:
 A (Somewhat Subjective) View from Within}},
 link = "\url{}",
 abstract =
 "In the 1970 and 1980s, logic and constructive mathematics were an
 important part of my life; it’s what I defended in my Master’s thesis,
 it was an important part of my PhD dissertation. I was privileged to
 work with the giants. I visited them in their homes. They were who I
 went to for advice. And this is my story.",
 paper = "Krei14.pdf"
}

\end{chunk}

\index{Windsteiger, Wolfgang}
\begin{chunk}{axiom.bib}
@article{Wind06,
 author = "Windsteiger, Wolfgang",
 title = {{An automated prover for ZermeloFraenkel set theory in
 Theorema}},
+@article{Farm95,
+ author = "Farmer, William M. and Guttman, J.D. and Thayer, F.J.",
+ title = {{Contexts in Mathematical Reasoning and Computation}},
journal = "J. of Symbolic Computation",
 volume = "41",
 pages = "435470",
 year = "2006",
 abstract =
 "This paper presents some fundamental aspects of the design and
 implementation of an automated prover for ZermeloFraenkel set theory
 within the Theorema system. The method applies the
 ``ProveComputeSolve'' paradigm as its major strategy for generating
 proofs in a natural style for statements involving constructs from set
 theroy.",
 paper = "Wind06.pdf"
}

\end{chunk}

\index{Schreiner, Wolfgang}
\begin{chunk}{axiom.bib}
@techreport{Schr14,
 author = "Schreiner, Wolfgang",
 title = {{Some Lessons Learned on Writing Predicate Logic Proofs in
 Isabelle/Isar}},
 year = "2014",
 institution = "RISC Linz",
 abstract =
 "We describe our experience with the use of the proving assistant
 Isabelle and its proof development language Isar for formulating and
 proving formal mathematical statements. Our focus is on how to use
 classical predicate logic and well established proof principles for
 this purpose, bypassing Isabelle’s metalogic and related technical
 aspects as much as possible. By a small experiment on the proof of
 (part of a) verification condition for a program, we were able to
 identify a number of important patterns that arise in such proofs
 yielding to a workflow with which we feel personally comfortable; the
 resulting guidelines may serve as a starting point for a the
 application of Isabelle / Isar for the “average” mathematical user
 (i.e, a mathematical user who is not interested in Isabelle / Isar per
 se but just wants to use it as a tool for computersupported formal
 theory development).",
 paper = "Schr14.pdf"
}
+ volume = "19",
+ pages = "201216",
+ year = "1995",
+ abstract =
+ "Contexts are sets of formulas used to manage the assumptions that
+ arise in the course of a mathematical deduction or
+ calculation. Although contextdependent reasoning is commonplace in
+ informal mathematics, most contemporary symbolic computation systems
+ do not utilize contexts in sophisticated ways. This paper describes
+ some contextbased techniques for symbolic computation, including
+ techniques for reasoning about definedness, simplifying abstract
+ algebraic expressions, and computing with theorems. All of these
+ techniques are implemented in the IMPS Interactive Mathematical Proof
+ System. The paper also proposes a general mathematics laboratory that
+ combines the functionality of current symbolic computation systems
+ with the facilities of a theorem proving system like IMPS.",
+ paper = "Farm95.pdf"
+}
+
+\end{chunk}
+
+\index{Farmer, William M.}
+\begin{chunk}{axiom.bib}
+@article{Farm93b,
+ author = "Farmer, William M.",
+ title = {{A simple type theory with partial functions and subtypes}},
+ journal = "Annals of Pure and Applied Logic",
+ volume = "64",
+ pages = "211240",
+ year = "1993",
+ abstract =
+ "Simple type theory is a higherorder predicate logic for reasoning
+ about truth values, individuals, and simply typed total functions. We
+ present in this paper a version of simple type theory, called PF*, in
+ which functions may be partial and types may have subtypes. We define
+ both a Henkinstyle general models semantics and an axiomatic system
+ for PF*, and we prove that the axiomatic system is complete with
+ respect to the general models semantics. We also define a notion of
+ an interpretation of one PF* theory in another. PF* is intended as a
+ foundation for mechanized mathematics. It is the basis for the logic
+ of IMPS, an Interactive Mathematical Proof System developed at The
+ MITRE Corporation.",
+ paper = "Farm93b.pdf"
+}
+
+\end{chunk}
+
+\index{Farmer, William H.}
+\begin{chunk}{axiom.bib}
+@article{Farm92,
+ author = "Farmer, William H.",
+ title = {{Little Theories}},
+ journal = "LNCS",
+ volume = "607",
+ year = "1992",
+ pages = "567581",
+ abstract =
+ "In the ``little theories'' version of the axiomatic method, different
+ portions of mathematics are developed in various different formal
+ axiomatic theories. Axiomatic theories may be related by inclusion or
+ by theory interpretation. We argue that the little theories approach
+ is a desirable way to formalize mathematics, and we describe how IMPS,
+ an Interactive Mathematical Proof System, supports it.",
+ paper = "Farm92.pdf"
+}
\end{chunk}
\index{Paule, Peter}
+\index{Owre, S.}
+\index{Rushby, J.M.}
+\index{Shankar, N.}
\begin{chunk}{axiom.bib}
@phdthesis{Paul14,
 author = "Paule, Peter",
 title = {{Complex Variables Visualized}},
 school = "RISC Linz",
 year = "2014",
 link =
 "\url{http://www.risc.jku.at/publications/download/risc_5011/DiplomaThesisPonweiser.pdf}",
+@article{Owre92,
+ author = "Owre, S. and Rushby, J.M. and Shankar, N.",
+ title = {{PVS: A Prototype Verification System}},
+ journal = "Lecture Notes in Computer Science",
+ volume = "687",
+ pages = "748752",
+ year = "1992",
abstract =
 "The aim of this diploma thesis is the visualization of some
 fundamental results in the context of the theory of the modular group
 and modular functions. For this purpose the computer algebra software
 Mathematica is utilized.

 The thesis is structured in three parts. In
 Chapter 1, we summarize some important basic concepts of group theory
 which are relevant to this work. Moreover, we introduce obius
 transformations and study their geometric mapping properties.

 Chapter 2 is devoted to the study of the modular group from an
 algebraic and geometric point of view. We introduce the canonical
 fundamental region which gives rise to the modular tessellation of
 the upper halfplane. Additionally, we present a general method
 for nding fundamental regions with respect to subgroups of the
 modular group based on the concepts of 2dimensional hyperbolic
 geometry.

 In Chapter 3 we give some concrete examples how the developed results and
 methods can be exploited for the visualization of certain mathematical
 results. Besides the visualization of function graphs of modular
 functions, a particularly nice result is the connection between
 modular transformations and continued fraction expansions.",
 paper = "Paul14.pdf"
+ "This brief paper introduces the main ideas of PVS",
+ paper = "Owre92.pdf"
}
\end{chunk}
\index{Khan, Muhammad Taimoor}
\begin{chunk}{axiom.bib}
@techreport{Khan13,
 author = "Khan, Muhammad Taimoor",
 title = {{On the Formal Verification of Maple Programs}},
 year = "2013",
 type = "technical report",
 number = "1307",
 institution = "RISC Linz",
 abstract =
 "In this paper, we present an examplebased demonstration of our
 recent results on the formal verification of programs written in the
 computer algebra language (Mini)Maple (a slightly modified subset of
 Maple). The main goal of this work is to develop a verification
 framework for behavioral analysis of MiniMaple programs. For
 verification, we translate an annotated MiniMaple program into the
 language Why3ML of the intermediate verification tool Why3 developed
 at LRI, France. We generate verification conditions by the
 corresponding component of Why3 and later prove the correctness of
 these conditions by various supported by the Why3 backend automatic
 and interactive theorem provers. We have used the verification
 framework to verify some parts of the main test example of our
 verification framework, the Maple package DifferenceDifferential
 developed at our institute to compute bivariate differencedifferential
 polynomials using relative Gr ̈obner bases.",
 paper = "Khan13.pdf"
}

\end{chunk}

\index{Kryvolap, Andrii}
\index{Nikitchenko, Mykola}
\index{Schreiner, Wolfgang}
\begin{chunk}{axiom.bib}
@inproceedings{Kryv13,
 author = "Kryvolap, Andrii and Nikitchenko, Mykola and Schreiner,
 Wolfgang",
 title = {{Extending FloydHoare Logic for Partial Pre and
 Postconditions}},
 booktitle = "ICTERI 2013: 9th Int. Conf. on ICT in Education,
 Research and Industrial Applications",
 pages = "023",
 publisher = "Springer",
 isbn = "9783319039978",
 year = "2014",
 abstract =
 "Traditional (classical) FloydHoare logic is defined for a case of
 total pre and postconditions while programs can be partial. In the
 chapter we propose to extend this logic for partial conditions. To
 do this we first construct and investigate special program algebras of
 partial predicates, functions, and programs. In such algebras
 program correctness assertions are presented with the help of a
 special composition called FloydHoare composition. This composition
 is monotone and continuous. Considering the class of constructed
 algebras as a semantic base we then define an extended logic – Partial
 FloydHoare Logic – and investigate its properties. This logic has
 rather complicated soundness constraints for inference rules,
 therefore simpler sufficient constraints are proposed. The logic
 constructed can be used for program verification.",
 paper = "Kryv13.pdf"
}

\end{chunk}

\index{Khan, Muhammad Taimoor}
+\index{Farmer, William H.}
\begin{chunk}{axiom.bib}
@techreport{Khan12,
 author = "Khan, Muhammad Taimoor",
 title = {{Formal Semantics of MiniMaple}},
 year = "2012",
 type = "technical report",
 number = "1204",
 institution = "RISC Linz",
 abstract =
 "In this paper, we give the complete definition of a formal
 denotational) semantics of a subset of the language of the
 computer algebra systems Maple which we call MiniMaple . As a
 next step we will develop a verification calculus for this
 language. The verification conditions generated by the calculus
 must be sound with respect to the formal semantics.",
 paper = "Khan12.pdf"
+@article{Farm92a,
+ author = "Farmer, William H.",
+ title = {{IMPS: System Description}},
+ journal = "Lecture Notes in Computer Science",
+ volume = "607",
+ pages = "701705",
+ year = "1992",
+ paper = "Farm92a.pdf"
}
\end{chunk}
\index{Khan, Muhammad Taimoor}
+\index{Wos, Larry}
\begin{chunk}{axiom.bib}
@techreport{Khan12a,
 author = "Khan, Muhammad Taimoor",
 title = {{Formal Semantics of a Specification Language MiniMaple}},
 year = "2012",
 type = "technical report",
 number = "1205",
 institution = "RISC Linz",
 abstract =
 "In this paper, we give the complete definition of a formal semantics
 of a specification language for MiniMaple. This paper is an update
 of the previously reported formal (denotational) semantics of
 MiniMaple. As a next step we will develop a verification calculus
 for MiniMaple and its specification language. The verification
 conditions generated by the calculus must be sound with respect to
 both the formal semantics of MiniMaple and its corresponding
 specification language.",
 paper = "Khan12a.pdf"
+@article{Wosx92,
+ author = "Wos, Larry",
+ title = {{The Impossibility of the Automation of Logical Reasoning}},
+ journal = "Lecture Notes in Computer Science",
+ volume = "607",
+ year = "1992",
+ pages = "13",
+ paper = "Wosx92.pdf"
}
\end{chunk}
\index{Khan, Muhammad Taimoor}
+\index{Craigen, Dan}
+\index{Kromodimoeljo, Sentot}
+\index{Meisels, Irwin}
+\index{Pase, Bill}
+\index{Saaltink, Mark}
\begin{chunk}{axiom.bib}
@article{Khan12b,
 author = "Khan, Muhammad Taimoor",
 title = {{Towards the Formal Semantics and Verification of Maple
 Programs}},
 journal = "LNAI",
 volume = "7362",
 pages = "231247",
 year = "2012",
 isbn = "9783642313738",
 abstract =
 "In this paper, we present our ongoing work and initial results on the
 formal specification and verification of MiniMaple (a substantial
 subset of Maple with slight extensions) programs. The main goal of our
 work is to find behavioral errors in such programs w.r.t. their
 specifications by static analysis. This task is more complex for widely
 used computer algebra languages like Maple as these are fundamentally
 different from classical languages: they support nonstandard types
 of objects such as symbols, unevaluated expressions and polynomials
 and require abstract computer algebraic concepts and objects such as
 rings and orderings etc. As a starting point we have defined and
 formalized a syntax, semantics, type system and specification language
 for MiniMaple.",
 paper = "Khan12b.pdf"
+@article{Crai92,
+ author = "Craigen, Dan and Kromodimoeljo, Sentot and Meisels, Irwin
+ and Pase, Bill",
+ title = {{Eves System Description}},
+ journal = "Lecture Notes in Computer Science",
+ volume = "607"
+ pages = "771775",
+ year = "1992",
+ paper = "Crai92.pdf"
}
\end{chunk}
\index{Khan, Muhammad Taimoor}
\index{Schreiner, Wolfgang}
+\index{Pfenning, Frank}
+\index{Rohwedder, Ekkehard}
\begin{chunk}{axiom.bib}
@article{Khan12c,
 author = "Khan, Muhammad Taimoor and Schreiner, Wolfgang",
 title = {{On Formal Specification of Maple Programs}},
 journal = "LNAI",
 volume = "7362",
 pages = "442446",
 year = "2012",
 isbn = "9783642313738",
+@article{Pfen92b,
+ author = "Pfenning, Frank and Rohwedder, Ekkehard",
+ title = {{Implementing the MetaTheory of Deductive Systems}},
+ journal = "Lecture Notes in Computer Science",
+ volume = "607"
+ pages = "771775",
+ year = "1992",
abstract =
 "This paper is an examplebased demonstration of our initial results
 on the formal specification of programs written in the computer
 algebra language MiniMaple (a substantial subset of Maple with slight
 extensions). The main goal of this work is to define a verification
 framework for MiniMaple. Formal specification of MiniMaple programs
 is rather complex task as it supports nonstandard types of objects,
 e.g. symbols and unevaluated expressions, and additional functions
 and predicates, e.g. runtime type tests etc. We have used the
 specification language to specify various computer algebra concepts
 respective objects of the Maple package DifferenceDifferential
 developed at our institute.",
 paper = "Khan12c.pdf"
+ "We exhibit a methodology for formulating and verifying meta theorems
+ about deductive systems in the Elf language, an implementation of the
+ LF Logical Framework with an operational semantics in the spirit of
+ logic programming. It is based on the mechanical verification of
+ properties of transformations between deductions, which relies on type
+ reconstruction and schemachecking. The latter is justified by
+ induction principles for closed LF objects, which can be constructed
+ over a given signature. We illustrate our technique through several
+ examples, the most extensive of which is an interpre tation of
+ classical logic in minimal logic through a continuationpassingstyle
+ transformation on proofs.",
+ paper = "Pfen92b.pdf"
}
\end{chunk}
\index{Kutsia, Temur}
\index{Marin, Mircea}
+\index{Guttman, J.D.}
\begin{chunk}{axiom.bib}
@techreport{Kuts12,
 author = "Kutsia, Temur and Marin, Mircea",
 title = {{Solving, Reasoning, and Programming in Common Logic}},
+@techreport{Gutt91,
+ author = "Guttman, J.D.",
+ title = {{A Propoed Interface Logic for Verification Environments}},
type = "technical report",
 institution = "RISC Linz",
 year = "2012",
 abstract =
 "Common Logic (CL) is a recent ISO standard for exchanging logicbased
 information between disparate computer systems. Sharing and reasoning
 upon knowledge represented in CL require equation solving over terms
 of this language. We study computationally wellbehaved fragments of
 such solving problems and show how they can influence reasoning in CL
 and transformations of CL expressions.",
 paper = "Kuts12.pdf"
+ number = "M9119",
+ institution = "The MITRE Corporation",
+ year = "1991"
}
\end{chunk}
\index{Kutsia, Temur}
\index{Marin, Mircea}
\begin{chunk}{axiom.bib}
@inproceedings{Kuts12a,
 author = "Kutsia, Temur and Marin, Mircea",
 title = {{Solving, Reasoning, and Programming in Common Logic}},
 booktitle = "SYNASC '12",
 isbn = "9780769549347",
 pages = "119126",
 year = "2012",
 abstract =
 "Common Logic (CL) is a recent ISO standard for exchanging logicbased
 information between disparate computer systems. Sharing and reasoning
 upon knowledge represented in CL require equation solving over terms
 of this language. We study computationally wellbehaved fragments of
 such solving problems and show how they can influence reasoning in CL
 and transformations of CL expressions.",
 paper = "Kuts12a.pdf"
+@misc{Open11,
+ author = "Dos Reis, G.",
+ title = {{OpenAxiom}},
+ link = "\url{http://www.openaxiom.org}",
+ year = "2011"
}
\end{chunk}
\index{Erascu, Madalina}
+\index{Matthews, David C.J.}
+\index{Wenzel, Makarius}
\begin{chunk}{axiom.bib}
@techreport{Eras11,
 author = "Erascu, Madalina",
 title = {{Symbolic Computation and Program Verification. Proving
 Partial Correctness and Synthesizing Optimal Algorithms}},
 type = "technical report",
 number = "1115",
 institution = "RISC Linz",
 year = "2011",
 abstract =
 "We present methods for checking the partial correctness of,
 respectively to optimize, imperative programs, using polynomial
 algebra methods, namely resultant computation and quantifier
 elimination (QE) by cylindrical algebraic decomposition (CAD). The
 result are very promising but also show that there is room for
 improvement of algebraic algorithms.",
 paper = "Eras11.pdf"
+@inproceedings{Matt10,
+ author = "Matthews, David C.J. and Wenzel, Makarius",
+ title = {{Efficient Parallel Programming in Poly/ML and Isabelle/ML}},
+ booktitle = "Proc. 5th ACM SIGPLAN workshop on Declarative aspects of
+ multicore programming",
+ pages = "5362",
+ year = "2010",
+ publisher = "ACM",
+ isbn = "9781605588599",
+ abstract =
+ "The ML family of languages and LCFstyle interactive theorem proving
+ have been closely related from their beginnings about 30 years
+ ago. Here we report on a recent project to adapt both the Poly/ML
+ compiler and the Isabelle theorem prover to current multicore
+ hardware. Checking theories and proofs in typical Isabelle application
+ takes minutes or hours, and users expect to make efficient use of
+ ``home machines'' with 28 cores, or more.
+
+ Poly/ML and Isabelle are big and complex software systems that have
+ evolved over more than two decades. Faced with the requirement to
+ deliver a stable and efficient parallel programming environment, many
+ infrastructure layers had to be reworked: from lowlevel system
+ threads to highlevel principles of valueoriented programming. At
+ each stage we carefully selected from the many existing concepts for
+ parallelism, and integrated them in a way that fits smoothly into the
+ idea of purely functional ML with the addition of synchronous
+ exceptions and asynchronous interrupts.
+
+ From the Isabelle/ML perspective, the main concept to manage parallel
+ evaluation is that of ``future values''. Scheduling is implicit, but it
+ is also possible to specify dependencies and priorities. In addition,
+ blockstructured groups of futures with propagation of exceptions
+ allow for alternative functional evaluation (such as parallel search),
+ without requiring user code to tackle concurrency. Our library also
+ provides the usual parallel combinators for functions on lists, and
+ analogous versions on prover tactics.
+
+ Despite substantial reorganization in the background, only minimal
+ changes are occasionally required in user ML code, and none at the
+ Isabelle application level (where parallel theory and proof processing
+ is fully implicit). The present implementation is able to address more
+ than 8 cores effectively, while the earlier version of the official
+ Isabelle2009 release works best for 24 cores. Scalability beyond 16
+ cores still poses some extra challenges, and will require further
+ improvements of the Poly/ML runtime system (heap management and
+ garbage collection), and additional parallelization of Isabelle
+ application logic.",
+ paper = "Matt10.pdf"
}
\end{chunk}
\index{Khan, Muhammad Taimoor}
\begin{chunk}{axiom.bib}
@techreport{Khan11,
 author = "Khan, Muhammad Taimoor",
 title = {{A Type Checker for MiniMaple}},
 type = "technical report",
 number = "1105",
 year = "2011",
 abstract =
 "In this paper, we present the syntactic definition and the formal type
 system for a substantial subset of the language of the computer
 algebra system Maple, which we call MiniMaple . The goal of the type
 system is to prevent runtime typing errors by static analysis of the
 source code of MiniMaple programs. The type system is implemented
 by a type checker, which veries the type correctness of MiniMaple
 programs respectively reports typing errors.",
 paper = "Khan11.pdf"
+@misc{Poly11a,
+ author = "Unknown",
+ title = {{Poly/ML}},
+ link = "\url{http://www.polyml.org}",
+ year = "2011"
}
\end{chunk}
\index{Khan, Muhammad Taimoor}
\index{Schreiner, Wolfgang}
\begin{chunk}{axiom.bib}
@inproceedings{Khan11a,
 author = "Khan, Muhammad Taimoor and Schreiner, Wolfgang",
 title = {{Towards a Behavioral Analysis of Computer Algebra
 Programs}},
 booktitle = "NWPT'11",
 pages = "4244",
 year = "2011",
 paper = "Khan11a.pdf"
+@misc{Isab11,
+ author = "Unknown",
+ title = {{Isabell}},
+ link = "\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html}",
+ year = "2011"
}
\end{chunk}
\index{Khan, Muhammad Taimoor}
+\index{Boulm\'e, Sylvain}
\begin{chunk}{axiom.bib}
@techreport{Khan11b,
 author = "Khan, Muhammad Taimoor",
 title = {{Towards a Behavioral Analysis of Computer Algebra
 Programs}},
 type = "technical report",
 number = "1113",
 year = "2011",
+@techreport{Boul00a,
+ author = "Boulme. Sylvain",
+ title = {{Specifying in Coq inheritance used in Computer Algebra
+ Libraries}},
+ year = "2000",
+ institution = "LIP6, Paris",
+ number = "2000.013",
abstract =
 "In this paper, we present our initial results on the behavioral
 analysis of computer algebra programs. The main goal of our work is
 to find typing and behavioral errors in such programs by static
 analysis of the source code. This task is more complex for widely
 used computer algebra languages (Maple and Mathematica) as these are
 fundamentally different from classical languages: for example they
 support nonstandard types of objects, e.g. symbols, unevaluated
 expressions, polynomials etc.; moreover they use type information to
 direct the flow of control in the program and have no clear
 difference between declaration and assignment. For this purpose, we
 have defined the syntax and the formal type system for a substantial
 subset of the computer algebra language Maple, which we call MiniMaple.
 The type system is implemented by a type checker, which verifies
 the type correctness and respectively reports typing errors. We have
 applied the type checker to the Maple package DifferenceDifferential
 developed at our institute. Currently we are working on a formal
 specification language of MiniMaple and the specification of this
 package. The specification language will be used to find errors in
 computer algebra programs with respect to their specifications.",
 paper = "Khan11b.pdf"
}

\end{chunk}

\index{Erascu, Madalina}
\index{Jebelean, Tudor}
\begin{chunk}{axiom.bib}
@inproceedings{Eras10,
 author = "Erascu, Madalina and Jebelean, Tudor",
 title = {{A Purely Logical Approach to Program Termination}},
 booktitle = "11th Int. Workshop on Termination",
 year = "2010",
 comment = "Extended Abstract",
 link =
 "\url{http://www.risc.jku.at/publications/download/risc_4089/ErascuJebeleanWSTFinal.pdf}",
 paper = "Eras10.pdf"
}

\end{chunk}

\index{Erascu, Madalina}
\index{Jebelean, Tudor}
\begin{chunk}{axiom.bib}
@techreport{Eras10a,
 author = "Erascu, Madalina and Jebelean, Tudor",
 title = {{A Purely Logical Approach to Imperative Program Verification}},
 year = "2010",
 institution = "RISC Linz",
 type = "technical report",
 number = "1007",
+ "This paper is part of FOC[3], a project for developing Computer
+ Algebra libraries, certified in Coq[2]. FOC has developed a
+ methodology for programming Computer Algebra libraries, using modules
+ and objects in Ocaml. In order to specify modularity features used by
+ FOC in Ocaml, we are coding in Coq a theory for extensible records
+ with dependent fields. This theory intends to express especially the
+ kind of inheritance with method redefinition and late binding, that
+ FOC uses in its Ocaml programs.
+
+ The unit of FOC are coded as records. As we want to encode sematic
+ information on units, the fields of our records may be proofs. Thus,
+ our fields may depend on each others. We call the
+ {\sl Drecords}. Then, we introduce a new datatype, called
+ {\sl mixDrec}, to represent FOC classes. Actually, mixDrecs are useful
+ for describing a hierarchy of Drecords in an incremental way. In
+ mixDrecs, fields can be only declared or they can be
+ redefined. MixDrecs can be extended by inheritance.",
+ paper = "Boul00a.pdf"
+}
+
+\end{chunk}
+
+\index{Dennis, Louise A.}
+\index{Collins, Graham}
+\index{Norrish, Michael}
+\index{Boulton, Richard}
+\index{Slind, Konrad}
+\index{Robinson, Graham}
+\index{Gordon, Mike}
+\index{Melham, Tom}
+\begin{chunk}{axiom.bib}
+@article{Denn00,
+ author = "Dennis, Louise A. and Collins, Graham and Norrish, Michael
+ and Boulton, Richard and Slind, Konrad and
+ Robinson, Graham and Gordon, Mike and Melham, Tom",
+ title = {{The PROSPER Toolkit}},
+ journal = "LNCS",
+ volume = "1785",
+ publisher = "SpringerVerlag",
+ pages = "7892",
+ year = "2000",
link =
 "\url{http://www.risc.jku.at/publications/download/risc_4088/techRep.pdf}",
 paper = "Eras10a.pdf"
}

\end{chunk}

\index{Erascu, Madalina}
\index{Jebelean, Tudor}
\begin{chunk}{axiom.bib}
@inproceedings{Eras10b,
 author = "Erascu, Madalina and Jebelean, Tudor",
 title = {{A Purely Logical Approach to Termination of Imperative Loops}},
 booktitle = "Proc. 12th Int. Symp. on SYmbolic and Numeric
 Algorithms for Scientific Computing",
 pages = "142149",
 year = "2010",
 link = "\url{http://www.risc.jku.at/publications/download/risc_4181/synasc_postproceedings.pdf}",
+ "\url{https://link.springer.com/content/pdf/10.1007/3540464190_7.pdf}",
abstract =
 "We present and illustrate a method for the gen eration of the
 termination conditions for nested loops with abrupt termination
 statements. The conditions are (firstorder) formulae obtained by
 certain transformations of the program text. The loops are treated
 similarly to calls of recursively defined functions. The program text
 is analyzed on all possible execution paths by forward symbolic
 execution using certain metalevel functions which define the syntax,
 the semantics, the verification conditions for the partial
 correctness, and the termination conditions. The termination
 conditions are expressed as induction principles, however, still in
 firstorder logic.

 Our approach is simpler than others because we use
 neither an additional model for program execution, nor a fixpoint
 theory for the definition of program semantics. Because the
 metalevel functions are fully formalized in predicate logic, it is
 possible to prove in a purely logical way and at object level that the
 verification conditions are necessary and sufficient for the existence
 and uniqueness of the function implemented by the program.",
 paper = "Eras10b.pdf"
+ "The PROSPER (Proof and Specification Assisted Design Environments)
+ project advocates the use of toolkits which allow existing
+ verification tools to be adapted to a more flexible format so that
+ they may be treated as components. A system incorporating such tools
+ becomes another component that can be embedded in an application. This
+ paper describes the PROSPER Toolkit which enables this. The nature of
+ communication between components is specified in a
+ languageindependent way. It is implemented in several common
+ programming languages to allow a wide variety of tools to have access
+ to the toolkit.",
+ paper = "Denn00.pdf"
}
\end{chunk}
\index{Vajda, Robert}
\index{Jebelean, Tudor}
\index{Buchberger, Bruno}
+\index{Dewar, Mike}
\begin{chunk}{axiom.bib}
@article{Vajd09,
 author = "Vajda, Robert and Jebelean, Tudor and Buchberger, Bruno",
 title = {{Combining Logical and Algebraic Techniques for Matural
 Style Proving in Elementary Analysis}},
 journal = "Mathematics and Computers in SImulation",
 volume = "79",
 number = "8",
 pages = "23102316",
 year = "2009",
 link =
 "\url{http://www.risc.jku.at/publications/download/risc_3320/acafin3.pdf}",
 abstract =
 "PCS (ProvingComputingSolving) [Buchberber 2001] and SDecomposition
 [Jebelean 2001] are strategies for handling proof problems by
 combining logic inference steps (e.g. modus ponens, Skolemization,
 instantiation) with rewriting steps (application of definitions) and
 solving procedures based on algebraic techniques (e.g. Groebner Bases,
 Cylindrical Algebraic Decomposition).

 If one formalizes the main notions of elementary analysis like
 continuity, convergence, etc., usually a sequence of alternating
 quantifier blocks pops up in the quantifier prefix of the
 corresponding formula. This makes the proof problems involving these
 notions not easy. SDecomposition strategy is expecially suitable for
 propertypreserving problems like continuity of sum, becuase it is
 designed for handling problems where the goal and the main assumptions
 have a similar structure. During proof deduction, existentially
 quantified goals and universal assumptions are handled by introducing
 metavariables, if no suitable ground instance is known in
 adva=nce. For finalizing proof attempts, the metavariables should be
 instantiated in such a way that they satisfy the cumulated algebraic
 constraints collected during the proof attempt. The instantiation
 problem is considered to be difficult in the logical
 calculus. Appropriate instances can be often found using quantifier
 elimination (QE) over real closed fields. In order to obtain witness
 terms we utilize the QE method based on cylindrical algebraic
 decomposition (CAD) [Collins 1975]. However, the QE method alone is
 not sufficient. One needs to preprocess the (closed, quantified)
 conjectured formula and postprocess the resulting CADstructure after
 the call of the QE algorithm.",
 paper = "Vajd09.pdf"
+@misc{Dewa00,
+ author = "Dewar, Mike",
+ title = {{Special Issue on OPENMATH}},
+ publisher = "ACM SIGPLAN Bulletin",
+ volume = "34",
+ number = "2",
+ year = "2000"
}
\end{chunk}
\index{Mayrhofer, Gunther}
+\index{Gray, Simon}
+\index{Kajler, Norbert}
+\index{Wang, Paul S.}
\begin{chunk}{axiom.bib}
@phdthsis{Mayr09,
 author = "Mayrhofer, Gunther",
 title = {{Symbolic COmputation Prover with Induction}},
 year = "2009",
 link =
 "\url{http://www.risc.jku.at/publications/download/risc_3910/Thesis.pdf}",
 institution = "RISC Linz",
+@article{Gray98,
+ author = "Gray, Simon and Kajler, Norbert and Wang, Paul S.",
+ title = {{Design and Implementation of MP, a Protocol for
+ Efficient Exchange of Mathematical Expressions}},
+ journal = "J. Symboic Computation",
+ volume = "25",
+ pages = "213237",
+ year = "1998",
abstract =
 "An important task in automated theorem proving is computing with
 "arbitrary but fixed" constants. This kind of highschool proving
 occurs in the main part of most proofs. The current master's thesis
 presents an automated prover that focuses on such computations with
 symbols. The prover uses equalities and equivalences in the knowledge
 base to rewrite a goal formula. In all formulae there may be universal
 quantifiers and some selected logical connectives. Special syntax
 elements support case distinctions and sequence variables. The prover
 uses a specialized method for proving equalities and an important
 feature is proving by cases. An extension allows induction over some
 predefined domains. Additionally to the prover implementation in
 Mathematica, there is a tracer that prints a protocol of the proof
 flow. Since the code for this tracer is separated from the prover,
 there may be more than one tracer with different output. But more
 important is that a user can inspect the code of prover without being
 confused by technical details for generating some nice output. The
 main motivation for this prover is a new extension of the Theorema
 system. The aim is an environment for defining new prover in the same
 language as theorems. The advantage is clear, existing prover may
 prove facts of a new one, for example the correctness. Using this it
 is possible to build up a hierarchy of formally checked provers. For
 such reasoning about reasoners a starting point needs induction on the
 structure of terms and formulae. A first prover in the hierarchy will
 need computations with symbols in many proof branches. This may be
 done by the current Symbolic Computation Prover.",
 paper = "Mayr09.pdf",
}

\end{chunk}

\index{Popov, Nikolaj}
\index{Jebelean, Tudor}
\begin{chunk}{axiom.bib}
@inproceedings{Popo09,
 author = "Popov, Nikolaj and Jebelean, Tudor",
 title = {{Functional Program Verification in Theorema Soundness and
 Completeness}},
 booktitle = "Proc. 15th Biennial Workshop on Programmiersprachen und
 Grundlagen der Programmierung KPS'09",
 year = "2009",
 pages = "221229",
+ "The Multi Project is an ongoing research e ort at Kent State
+ University aimed at providing an environment for distributed scientific
+ computing. An integral part of this environment is the Multi
+ Protocol (MP) which is designed to support ecientific communication of
+ mathematical data between scientificallyoriented software tools. MP
+ exchanges data in the form of linearized annotated syntax
+ trees. Syntax trees provide a simple, flexible and toolindependent
+ way to represent and exchange data, and annotations provide a powerful
+ and generic expressive facility for transmitting additional
+ information. At a level above the data exchange protocol,
+ dictionaries provide definitions for operators and constants, providing
+ shared semantics across heterogeneous packages. A clear distinction
+ between MPdefined and userdefined entities is enforced. Binary
+ encodings are used for efficiency. Commonly used values and blocks of
+ homogeneous data are further optimized. The protocol is independent of
+ the underlying communication paradigm and can support parallel
+ computation, distributed problemsolving environments, and the
+ coupling of tools for speci c applications.",
+ paper = "Gray98.pdf"
+}
+
+\end{chunk}
+
+\index{Harrison, John}
+\index{Th\'ery, Laurent}
+\begin{chunk}{axiom.bib}
+@incollection{Harr93,
+ author = "Harrison, John and Thery, Laurent",
+ title = {{Reasoning about the Reals: The Marriage of HOL and
+ Maple}},
+ booktitle = "Logic Programming and Automated Reasoning",
+ publisher = "SpringerVerlag",
+ year = "1993",
+ pages = "351353",
link =
 "\url{http://www.risc.jku.at/publications/download/risc_3913/PopJeb.pdf}",
+ "\url{https://link.springer.com/content/pdf/10.1007/3540569448_68.pdf}",
abstract =
 "We present a method for verifying recursive functional pro grams. We
 define a Verification Condition Generator (VCG) which covers the most
 frequent types of recursive programs. These programs may op erate on
 arbitrary domains. Soundness and Completeness of the VCG are proven on
 the meta level, and this provides a warranty that any system based on
 our results will be sound.",
 paper = "Popo09.pdf"
+ "Computer algebra systems are extremely powerful and flexible, but
+ often give results which require careful interpretation or are
+ downright incorrect. By contrast, theorem provers are very reliable
+ but lack the powerful specialized decision procedures and heuristics
+ of computer algebra systems. In this paper we try to get the best of
+ both worlds by careful exploitation of a link between a theorem prover
+ and a computer algebra system.",
+ paper = "Harr93.pdf"
}
\end{chunk}
\index{Popov, Nikolaj}
\index{Jebelean, Tudor}
+\index{Richardson, Daniel}
\begin{chunk}{axiom.bib}
@inproceedings{Popo09a,
 author = "Popov, Nikolaj and Jebelean, Tudor",
 title = {{A Complete Method for Algorithm Validation}},
 booktitle =
 "Proc. Workshop on Automated Math Theory Exploration AUTOMATHEO'09",
 pages = "2125",
 year = "2009",
 link = "\url{http://www.risc.jku.at/publications/download/risc_3915/PopJebAUTOMATHEO.pdf}",
+@article{Rich69,
+ author = "Richardson, Daniel",
+ title = {{Some Undecidable Problems involving Elementar Functions of
+ a Real Variable}},
+ journal = "J. Symbolic Logic",
+ volume = "33",
+ number = "4",
+ year = "1969",
+ pages = "514520",
abstract =
 "We present some novel ideas for proving total correctness of
 recursive functional programs and we discuss how they may be used for
 algorithm validation. As usual, correctness (validation) is
 transformed into a set of firstorder predicate logic
 formulae—verification conditions. As a distinctive feature of our
 method, these formulae are not only sufficient, but also necessary
 for the correctness. We demonstrate our method on the Nevilles
 algorithm for polynomial interpolation and show how it may be
 validated automatically. In fact, even if a small part of the
 specification is missing—in the literature this is often a case 
 the correctness cannot be proven. Furthermore, a relevant
 counterexample may be constructed automatically.",
 paper = "Popo99a.pdf"
+ "Let $E$ be a set of expressions representing real, single valued,
+ partially defined functions of one real variable. $E^*$ will be the
+ set of functions represented by expressions in $E$. If $A$ is an
+ expression in $E$, $A(x)$ is the function denoted by $AA$. It is
+ assumed that $D^*$ contains the identity function and the rational
+ numbers as constant functions and that $E^*$ is closed under addition,
+ subtraction, multiplication, and composition"
}
\end{chunk}
\index{Schreiner, Wolfgang}
+\index{Rushby, John}
\begin{chunk}{axiom.bib}
@techreport{Schr09,
 author = "Schreiner, Wolfgang",
 title = {{How to Write Postconditions with Nultiple Cases}},
 year = "2009",
 institution = "RISC Linz",
 abstract =
 "We investigate and compare the two major styles of writing program
 function postconditions with multiple cases: as conjunctions of
 implications or as disjunctions of conjunctions. We show that both
 styles not only have different syntax but also different semantics and
 pragmatics and give recommendations for their use.",
 paper = "Schr09.pdf"
}
+@inproceedings{Rush00,
+ author = "Rushby, John",
+ title = {{Disappearing Formal Methods}},
+ booktitle = "High Assurance Systems Engineering, 5th Int. Symp.",
+ pages = "9596",
+ year = "2000",
+ publisher = "ACM",
+ paper = "Rush00.pdf"
+}
\end{chunk}
\index{Buchberger,B}
\index{Craciun, A.}
+\index{Buchberger, B.}
+\index{Dupre, C.}
\index{Jebelean, T.}
\index{Kovacs, L.}
\index{Kutsia, T.}
+\index{Kriftner, F.}
\index{Nakagawa, K.}
\index{Piroi, F.}
\index{Popov, N.}
\index{Robu, J.}
\index{Rosenkranz, M.}
+\index{Vasaru, D.}
\index{Windsteiger, W.}
\begin{chunk}{axiom.bib}
@article{Buch06,
 author = "Buchberger,B and Craciun, A. and Jebelean, T. and
 Kovacs, L. and Kutsia, T. and Nakagawa, K. and Piroi, F.
 and Popov, N. and Robu, J. and Rosenkranz, M. and
 Windsteiger, W.",
 title = {{Theorema: Towards ComputerAided Mathematical Theory
 Exploration}},
 journal = "J. of Applied Logic",
 volume = "4",
 number = "4",
 pages = "470504",
 year = "2006",
+@misc{Buch00,
+ author = "Buchberger, B. and Dupre, C. and Jebelean, T. and Kriftner, F.
+ and Nakagawa, K. and Vasaru, D. and Windsteiger, W.",
+ title = {{The Theorema Project: A Progress Report}},
+ year = "2000",
abstract =
 "Theorema is a project that aims at supporting the entire process of
 mathematical theory exploration within one coherent logic and software
 system. This survey paper illustrates the style of Theoremasupported
 mathematical theory exploration by a case study (the automated
 synthesis of an algorithm for the construction of Groebner Bases) and
 gives an overview on some reasoners and organizational tools for
 theory exploration developed in the Theorema project.",
 paper = "Buch06.pdf"
+ "The THEOREMA project aims at supporting, within one consistent logic
+ and one coherent software system, the entire mathematical exploration
+ cycle including the phase of proving. In this paper we report on some
+ of the new features of THEOREMA that have been designed and
+ implemented since the first expository version of THEOREMA in
+ 1997. These features are:  the THEOREMA formal text language  the
+ THEOREMA computational sessions  the ProveComputeSolve (PCS) prover
+ of THEOREMA  the THEOREMA set theory prover  special provers within
+ THEOREMA  the cascademetastrategy for THEOREMA provers  proof
+ simplification in THEOREMA. In the conclusion, we formulate design
+ goals for the next version of THEOREMA",
+ paper = "Buch00.pdf"
}
\end{chunk}
\index{Abraham, Erika}
\index{Abbott, John}
\index{Becker, Bernd}
\index{Bigatti, Anna M.}
\index{Brain, Martin}
\index{Buchberger, Bruno}
\index{Cimatti, Alessandro}
\index{Davenport, James H.}
\index{England, Matthew}
\index{Fontaine, Pascal}
\index{Forrest, Stephen}
\index{Griggio, Alberto}
\index{Kroenig, Daniel}
\index{Seiler, Werner M.}
\index{Sturm, Thomas}
+\index{Boyer, Robert S.}
+\index{Moore, J Strother}
\begin{chunk}{axiom.bib}
@misc{Abra16,
 author = "Abraham, Erika and Abbott, John and Becker, Bernd and
 Bigatti, Anna M. and Brain, Martin and Buchberger, Bruno
 and Cimatti, Alessandro and Davenport, James H. and
 England, Matthew and Fontaine, Pascal and Forrest, Stephen
 and Griggio, Alberto and Kroenig, Daniel and
 Seiler, Werner M. and Sturm, Thomas",
 title = {{Satisfiability Checking meesg Symbolic Computation}},
 year = "2016",
 link = "\url{http://arxiv.org/abs/1607.08028}",
 abstract =
 "Symbolic Computation and Satisfiability Checking are two research
 areas, both having their individual scientific focus but sharing also
 common interests in the development, implementation and application of
 decision procedures for arithmetic theories. Despite their
 commonalities, the two communities are rather weakly connected. The
 aim of our newly accepted SCsquare project (H2020FETOPENCSA) is to
 strengthen the connection between these communities by creating common
 platforms, initiating interaction and exchange, identifying common
 challenges, and developing a common roadmap from theory along the way
 to tools and (industrial) applications. In this paper we report on the
 aims and on the first activities of this project, and formalise some
 relevant challenges for the unified SCsquare community.",
 paper = "Abra16.pdf"
+@techreport{Boye85,
+ author = "Boyer, Robert S. and Moore, J Strother",
+ title = {{Integrating Decision Procedures into Heuristic Theorem Provers}},
+ type = "technical report",
+ institution = "Inst. for Comp. Sci. University of Texas at Austin",
+ number = "ICSCACMP44",
+ year = "1985",
+ abstract =
+ "We discuss the problem of incorporating into a heuristic theorem
+ prover a decision procedure for a fragment of the logic. An obvious
+ goal when incorporating such a procedure is to reduce the search space
+ explored by the heuristic component of the system, as would be
+ achieved by eliminating from the system’s data base some explicitly
+ stated axioms. For example, if a decision procedure for linear
+ inequalities is added, one would hope to eliminate the explicit
+ consideration of the transitivity axioms. However, the decision
+ procedure must then be used in all the ways the eliminated axioms
+ might have been. The difficulty of achieving this degree of
+ integration is more dependent upon the complexity of the heuristic
+ component than upon that of the decision procedure. The view of the
+ decision procedure as a ``black box'' is frequently destroyed by the
+ need pass large amounts of search strategic information back and forth
+ between the two components. Finally, the efficiency of the decision
+ procedure may be virtually irrelevant; the efficiency of the final
+ system may depend most heavily on how easy it is to communicate
+ between the two components. This paper is a case study of how we
+ integrated a linear arithmetic procedure into a heuristic theorem
+ prover. By linear arithmetic here we mean the decidable subset of
+ number theory dealing with universally quantified formulas composed of
+ the logical connectives, the identity relation, the Peano ``less than''
+ relation, the Peano addition and subtraction functions, Peano
+ constants, and variables taking on natural values. We describe our
+ system as it originally stood, and then describe chronologically the
+ evolution of our linear arithmetic procedure and its interface to the
+ heuristic theorem prover. We also provide a detailed description of
+ our final linear arithmetic procedure and the use we make of it. This
+ description graphically illustrates the difference between a
+ standalone decision procedure and one that is of use to a more
+ powerful theorem prover.",
+ paper = "Boye85.pdf"
+}
+
+\end{chunk}
+
+\index{Farmer, William M.}
+\index{Guttman, Joshua D.}
+\index{Fabrega, F. Javier Thayer}
+\begin{chunk}{axiom.bib}
+@article{Farm96,
+ author = "Farmer, William M. and Guttman, Joshua D. and
+ Fabrega, F. Javier Thayer",
+ title = {{IMPS: An Updated System Description}},
+ journal = "LNCS",
+ volume = "1104",
+ pages = "298302",
+ year = "1996",
+ paper = "Farm96.pdf"
+}
+
+\end{chunk}
+
+\index{Gordon, M.}
+\index{Milner, R.}
+\index{Wadsworth, C.P.}
+\begin{chunk}{axiom.bib}
+@book{Gord79,
+ author = "Gordon, M. and Milner, R. and Wadsworth, C.P.",
+ title = {{Edinburgh LCF: A Mechanised Logic of Computation}},
+ comment = "Lecture Notes in Computer Science Volume 78",
+ publisher = "SpringerVerlag",
+ year = "1979"
+}
+
+\end{chunk}
+
+\index{Pfenning, Frank}
+\begin{chunk}{axiom.bib}
+@misc{Pfen17,
+ author = "Pfenning, Frank",
+ title = {{Logical Frameworks}},
+ link = "\url{http://www.cs.cmu.edu/afs/cs.cmu.edu/user/fp/www/lfs.html}",
+ year = "2017"
}
\end{chunk}
\index{Buchberger, Bruno}
\index{Jebelean, Tudor}
\index{Kutsia, Temur}
\index{Maletzky, Alexander}
\index{Windsteiger, Wolfgang}
\begin{chunk}{axiom.bib}
@article{Buch16,
 author = "Buchberger, Bruno and Jebelean, Tudor and Kutsia, Temur
 and Maletzky, Alexander and Windsteiger, Wolfgang",
 title = {{Theorema 2.0: ComputerAssisted NaturalStyle Mathematics}},
 journal = "J. of Formalized Reasoning",
 volume = "9",
 number = "1",
 pages = "149155",
 year = "2016",
 abstract =
 "The Theorema project aims at the development of a computer assistant
 for the working mathematician. Support should be given throughout all
 phases of mathematical activity, from introducing new mathematical
 concepts by definitions or axioms, through first (computational)
 experiments, the formulation of theorems, their justification by an
 exact proof, the application of a theorem as an algorithm, until to
 the dissemination of the results in form of a mathematical
 publication, the build up of bigger libraries of certified
 mathematical content and the like. This ambitious project is exactly
 along the lines of the QED manifesto issued in 1994 and it was
 initiated in the mid1990s by Bruno Buchberger. The Theorema system is
 a computer implementation of the ideas behind the Theorema
 project. One focus lies on the natural style of system input (in form
 of definitions, theorems, algorithms, etc.), system output (mainly in
 form of mathematical proofs) and user interaction. Another focus is
 theory exploration, i.e. the development of large consistent
 mathematical theories in a formal frame, in contrast to just proving
 single isolated theorems. When using the Theorema system, a user
 should not have to follow a certain style of mathematics enforced by
 the system (e.g. basing all of mathematics on set theory or certain
 variants of type theory), rather should the system support the user in
 her preferred flavour of doing math. The new implementation of the
 system, which we refer to as Theorema 2.0, is opensource and
 available through GitHub.",
 paper = "Buch16.pdf"
+@misc{Theo17,
+ author = "Unknown",
+ title = {{Theorema Project}},
+ link = "\url{http://www.theorema.org}",
+ year = "2017"
}
\end{chunk}
+
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index b440695..7afd180 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5856,6 +5856,8 @@ books/bookvolbib add references
books/bookvolbib add references
20171113.01.tpd.patch
books/bookvolbib add references
+20171115.01.tpd.patch
+books/bookvolbib add references

1.9.1