From c38f210b96e8e3316b960242783ba6965fb3c328 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Mon, 13 Nov 2017 19:54:01 0500
Subject: [PATCH] books/bookvolbib add references
MIMEVersion: 1.0
ContentType: text/plain; charset=UTF8
ContentTransferEncoding: 8bit
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",
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",
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"
}
\end{chunk}
\index{Neuper, Walther}
\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"
}
\end{chunk}
\index{Buchberger, Bruno}
\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",
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"
}
\end{chunk}
\index{Kreinovich, Vladik}
\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}},
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"
}
\end{chunk}
\index{Paule, Peter}
\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}",
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"
}
\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}
\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"
}
\end{chunk}
\index{Khan, Muhammad Taimoor}
\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"
}
\end{chunk}
\index{Khan, Muhammad Taimoor}
\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"
}
\end{chunk}
\index{Khan, Muhammad Taimoor}
\index{Schreiner, Wolfgang}
\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",
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"
}
\end{chunk}
\index{Kutsia, Temur}
\index{Marin, Mircea}
\begin{chunk}{axiom.bib}
@techreport{Kuts12,
author = "Kutsia, Temur and Marin, Mircea",
title = {{Solving, Reasoning, and Programming in Common Logic}},
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"
}
\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"
}
\end{chunk}
\index{Erascu, Madalina}
\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"
}
\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"
}
\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"
}
\end{chunk}
\index{Khan, Muhammad Taimoor}
\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",
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",
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}",
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"
}
\end{chunk}
\index{Vajda, Robert}
\index{Jebelean, Tudor}
\index{Buchberger, Bruno}
\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"
}
\end{chunk}
\index{Mayrhofer, Gunther}
\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",
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",
link =
"\url{http://www.risc.jku.at/publications/download/risc_3913/PopJeb.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"
}
\end{chunk}
\index{Popov, Nikolaj}
\index{Jebelean, Tudor}
\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}",
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"
}
\end{chunk}
\index{Schreiner, Wolfgang}
\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"
}
\end{chunk}
\index{Buchberger,B}
\index{Craciun, A.}
\index{Jebelean, T.}
\index{Kovacs, L.}
\index{Kutsia, T.}
\index{Nakagawa, K.}
\index{Piroi, F.}
\index{Popov, N.}
\index{Robu, J.}
\index{Rosenkranz, M.}
\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",
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"
}
\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}
\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"
}
\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"
}
\end{chunk}

books/axiom.bib  887 ++++++++++++++++++++++
books/bookvolbib.pamphlet  1115 ++++++++++++++++++++++++++++
changelog  2 +
patch  1539 +++++++++++++++++++++++++
src/axiomwebsite/patches.html  2 +
5 files changed, 2965 insertions(+), 580 deletions()
diff git a/books/axiom.bib b/books/axiom.bib
index b34c93e..449bd1a 100644
 a/books/axiom.bib
+++ b/books/axiom.bib
@@ 2562,6 +2562,49 @@ paper = "Brea89.pdf"
paper = "Turn86.pdf"
}
+@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"
+}
+
@techreport{Volp91,
author = "Volpano, Dennis M. and Geoffrey S.",
title = {{On the Complexity of ML Typability with Overloading}},
@@ 6852,7 +6895,7 @@ paper = "Brea89.pdf"
paper = "Abra15.pdf"
}
@inproceedings{Abra16,
+@inproceedings{Abra16a,
author = "Abraham, Erika",
title = {{Symbolic Computation Techniques in Satisfiability Checking}},
booktitle = "SYNASC 2016",
@@ 6872,6 +6915,32 @@ paper = "Brea89.pdf"
paper = "Abra17.pdf"
}
+@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"
+}
+
@misc{Abraxx,
author = "Abraham, Erika and Abbott, John and Becker, Bernd and
Bigatti, Anna M. and Brain, Martin and Cimatti, Alessandro and
@@ 7778,6 +7847,99 @@ paper = "Brea89.pdf"
paper = "Buch97.pdf"
}
+@article{Buch01,
+ author = "Buchberger, Bruno",
+ title = {{Theorema: A Proving System Based on Mathematica}},
+ journal = "The Mathematica Journal",
+ volume = "8",
+ number = "2",
+ pages = "247252",
+ year = "2001",
+ paper = "Buch01.pdf"
+}
+
+@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",
+ 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"
+}
+
+@misc{Buch03,
+ author = "Buchberger, Bruno and Aigner, K. and Dupre, C. and
+ Jebelean, T. and Kriftner, F. and Marin, M. and
+ Nakagawa, K. and Podisor, O. and Tomuta, E. and
+ Usenko, Y. and Vasaru, D. and Windsteiger, W.",
+ 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"
+}
+
+@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"
+}
+
@article{Bulo04,
author = {MedinaBulo, I. and PalomoLozano, F. and AlonsoJim\'enez, J.A.
and RuizReina, J.L.},
@@ 9959,6 +10121,28 @@ paper = "Brea89.pdf"
paper = "Mahb16.pdf"
}
+@techreport{Male17,
+ author = "Maletzky, Alexander",
+ title = {{A New Reasoning Framework for Theorema 2.0}},
+ year = "2017",
+ institution = "RISC Linz",
+ 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"
+}
+
@article{Male16,
author = "Maletzky, Alexander",
title = {{Interactive Proving, HigherOrder Rewriting, and Theory Analysis
@@ 10161,6 +10345,14 @@ paper = "Brea89.pdf"
paper = "Medi04.pdf"
}
+@mastersthesis{Mein13,
+ author = "Meindl, Diana",
+ title = {{Implementation of an Algorithm Computing the Greatest
+ Common Divisor for Multivariate Polynomials}},
+ year = "2013",
+ school = "RISC Linz"
+}
+
@article{Melq12,
author = "Melquiond, Guillaume",
title = {{Floatingpoint arithmetic in the Coq system}},
@@ 11371,6 +11563,13 @@ paper = "Brea89.pdf"
paper = "Ther98.pdf"
}
+@phdthesis{Tomu98,
+ author = "Tomuta, E.",
+ title = {{Proof Control in the Theorema Project}},
+ year = "1998",
+ school = "RISC Linz"
+}
+
@article{Tray11,
author = "Traytel, Dmitriy and Berghofer, Stefan and Nipkow, Tobias",
title = {{Extending HindleyMilner Type Inference with Coercive
@@ 11597,6 +11796,24 @@ paper = "Brea89.pdf"
paper = "Wind14.pdf"
}
+@article{Wind06,
+ author = "Windsteiger, Wolfgang",
+ title = {{An automated prover for ZermeloFraenkel set theory in
+ Theorema}},
+ 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
+ theory.",
+ paper = "Wind06.pdf"
+}
+
@book{Wins93,
author = "Winskel, Glynn",
title = {{The Formal Semantics of Programming Languages}},
@@ 18438,6 +18655,40 @@ paper = "Brea89.pdf"
paper = "Nore08.pdf"
}
+@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}",
+ 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"
+}
+
@article{Stou79,
author = "Stoutemyer, David R.",
title = {{LISP Based Symbolic Math Systems}},
@@ 26172,7 +26423,8 @@ paper = "Brea89.pdf"
year = "2008",
pages = "133140",
isbn = "978159593904",
 link = "\url{http://www.risc.jku.at/publications/download/risc_3427/Ka01.pdf}",
+ link =
+ "\url{http://www.risc.jku.at/publications/download/risc_3427/Ka01.pdf}",
abstract =
"A new method is proposed for finding the logarithmic part of an
integral over an algebraic function. The method uses Groebner bases
@@ 31967,6 +32219,23 @@ paper = "Brea89.pdf"
paper = "Denz94.pdf"
}
+@misc{Dolz96,
+ author = "Dolzmann, Andreas and Sturm, Thomas",
+ title = {{Redlog User Manual Edition 1.0}},
+ year = "1996",
+ abstract =
+ "REDLOG stands for REDUCE LOGIC system. It provides an extension
+ of the computer algebra system reduce to a ``computer logic system''
+ implementing symbolic algorithms on firstorder formulas wrt.
+ temporarily fixed firstorder languages and theories. Underlying
+ theories currently available are ordered fields and discretely
+ valued fields. Though the focus of the implemented algorithms is on
+ effective quantier elimination and simplication of quantierfree
+ formulas, REDLOG is intended and designed as an allpurpose system.
+ REDLOG is freely available to the scientic community.",
+ paper = "Dolz96.pdf"
+}
+
@article{Dolz97b,
author = "Dolzmann, Andreas and Sturm, Thomas",
title = {{REDLOG: Computer Algebra meets Computer Logic}},
@@ 32156,6 +32425,78 @@ paper = "Brea89.pdf"
publisher = "Spartan Books"
}
+@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"
+}
+
+@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",
+ link =
+ "\url{http://www.risc.jku.at/publications/download/risc_4088/techRep.pdf}",
+ paper = "Eras10a.pdf"
+}
+
+@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}",
+ 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"
+}
+
+@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"
+}
+
@misc{Fate08,
author = "Fateman, Richard J.",
title = {{Revisiting numeric/symbolic indefinite integration of rational
@@ 32252,6 +32593,27 @@ paper = "Brea89.pdf"
paper = "Fult08.pdf"
}
+@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"
+}
+
@book{Gath99,
author = {{von zur Gathen}, Joachim and Gerhard, J\"urgen},
title = {{Modern Computer Algebra}},
@@ 32261,6 +32623,26 @@ paper = "Brea89.pdf"
algebra = "\newline\refto{package PGCD PolynomialGcdPackage}"
}
+@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"
+}
+
@misc{Gode16,
author = "Godek, Panicz Maciej",
title = {{A Pamphlet Against R}},
@@ 32286,6 +32668,27 @@ paper = "Brea89.pdf"
}
+@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"
+
+}
+
@misc{Grab91a,
author = "Grabmeier, Johannes",
title = {{Groups, finite fields and algebras, constructions and
@@ 32704,6 +33107,173 @@ paper = "Brea89.pdf"
isbn = "0792377443"
}
+@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"
+}
+
+@techreport{Khan11b,
+ author = "Khan, Muhammad Taimoor",
+ title = {{Towards a Behavioral Analysis of Computer Algebra
+ Programs}},
+ type = "technical report",
+ number = "1113",
+ year = "2011",
+ 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"
+}
+
+@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"
+}
+
+@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"
+}
+
+@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{Khan12b,
+ author = "Khan, Muhammad Taimoor and Schreiner, Wolfgang",
+ 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{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",
+ 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"
+}
+
+@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"
+}
+
@phdthesis{Khan14,
author = "Khan, Muhammad Taimoor",
title = {{Formal Specification and Verification of Computer Algebra
@@ 32781,6 +33351,81 @@ paper = "Brea89.pdf"
keywords = "CASProof"
}
+@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"
+}
+
+@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"
+}
+
+@techreport{Kuts12,
+ author = "Kutsia, Temur and Marin, Mircea",
+ title = {{Solving, Reasoning, and Programming in Common Logic}},
+ 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"
+}
+
+@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{Lamp95,
author = "Lamport, Leslie",
title = {{Types Are Not Harmless}},
@@ 33115,6 +33760,17 @@ paper = "Brea89.pdf"
link = "\url{https://savannah.gnu.org/projects/gcl}"
}
+@incollection{Mark62,
+ author = "Markov, Andrei .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"
+}
+
@misc{Mars07,
author = "Marshak, U.",
title = {{HTAJAX  AJAX framework for Hunchentoot}},
@@ 33128,6 +33784,42 @@ paper = "Brea89.pdf"
link = "\url{http://maxima.sourceforge.net/docs/tutorial/en/gaertnertutorialrevision/Pages/SI001.htm}"
}
+@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",
+ 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"
+}
+
@misc{Maye17,
author = "Mayero, Micaela and Delahaye, David",
title = {{A Maple Mode for Coq}},
@@ 33342,6 +34034,98 @@ paper = "Brea89.pdf"
paper = "Naud98.pdf"
}
+@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"
+}
+
+@article{Meup13a,
+ author = "Neuper, Walther",
+ title = {{On the Emergence of TPbased Educational Math
+ Assistants}},
+ journal = "The Electronic Journal of Mathematics and Technology",
+ volume = "1",
+ 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"
+}
+
+@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."
+}
+
@misc{OCAM14,
author = "unknown",
title = {{The OCAML website}},
@@ 33478,6 +34262,50 @@ paper = "Brea89.pdf"
paper = "Phil02.pdf"
}
+@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",
+ link =
+ "\url{http://www.risc.jku.at/publications/download/risc_3913/PopJeb.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"
+}
+
+@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}",
+ 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"
+}
+
@inproceedings{Prat73,
author = "Pratt, Vaughan R.",
title = {{Top down operator precedence}},
@@ 33710,6 +34538,20 @@ paper = "Brea89.pdf"
the subject for the first time."
}
+@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{Schr00,
author = "Schreiner, Wolfgang and DanielczykLanderl, Werner and
Marin, Mircea and Stocher, Wolfgang",
@@ 33731,6 +34573,37 @@ paper = "Brea89.pdf"
paper = "Schr00.pdf"
}
+@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"
+}
+
+@misc{SCSCP,
+ author = "The SCSCP development team",
+ title = {{Symbolic Computation Software Composability Protocol}},
+ link = "\url{https://gappackages.github.io/scscp/}",
+ year = "2017"
+}
+
@book{Segg93,
author = "{von Seggern}, David Henry",
title = {{CRC Standard Curves and Surfaces}},
@@ 34019,6 +34892,16 @@ paper = "Brea89.pdf"
link = "\url{https://en.wikipedia.org/wiki/Levenshtein\_distance}"
}
+@misc{Wink95,
+ author = "Winkler, Franz",
+ title = {{Computer Algebra  Problems and Developments}},
+ year = "1995",
+ abstract =
+ "Recent developments in computer algebra are discussed using simple
+ but illustrative examples",
+ paper = "Wink95.pdf"
+}
+
@book{Wuxx94,
author = "Wu, Wentsun",
title = {{Mechanical Theorem Proving in Geometries}},
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 1c89504..15dc9e5 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 3577,6 +3577,55 @@ paper = "Brea89.pdf"
\subsection{V} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Vajda, Robert}
+\index{Jebelean, Tudor}
+\index{Buchberger, Bruno}
+\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"
+}
+
+\end{chunk}
+
\index{Volpano, Dennis M.}
\index{Geoffrey S.}
\begin{chunk}{axiom.bib}
@@ 9357,7 +9406,7 @@ when shown in factored form.
\index{Abraham, Erika}
\begin{chunk}{axiom.bib}
@inproceedings{Abra16,
+@inproceedings{Abra16a,
author = "Abraham, Erika",
title = {{Symbolic Computation Techniques in Satisfiability Checking}},
booktitle = "SYNASC 2016",
@@ 9389,6 +9438,50 @@ when shown in factored form.
\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}
+\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"
+}
+
+\end{chunk}
+
+\index{Abraham, Erika}
+\index{Abbott, John}
+\index{Becker, Bernd}
+\index{Bigatti, Anna M.}
+\index{Brain, Martin}
\index{Cimatti, Alessandro}
\index{Davenport, James H.}
\index{England, Matthew}
@@ 10537,6 +10630,141 @@ when shown in factored form.
\end{chunk}
+\index{Buchberger, Bruno}
+\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",
+ year = "2001",
+ paper = "Buch01.pdf"
+}
+
+\end{chunk}
+
+\index{Buchberger,B}
+\index{Craciun, A.}
+\index{Jebelean, T.}
+\index{Kovacs, L.}
+\index{Kutsia, T.}
+\index{Nakagawa, K.}
+\index{Piroi, F.}
+\index{Popov, N.}
+\index{Robu, J.}
+\index{Rosenkranz, M.}
+\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",
+ 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"
+}
+
+\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 and Aigner, K. and Dupre, C. and
+ Jebelean, T. and Kriftner, F. and Marin, M. and
+ Nakagawa, K. and Podisor, O. and Tomuta, E. and
+ Usenko, Y. and Vasaru, D. and Windsteiger, W.",
+ 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{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"
+}
+
+\end{chunk}
+
\index{MedinaBulo, I.}
\index{PalomoLozano, F.}
\index{AlonsoJim\'enez, J.A.}
@@ 10614,7 +10842,6 @@ when shown in factored form.
}
\end{chunk}

\index{Bundy, Alan}
\begin{chunk}{axiom.bib}
@@ 13363,6 +13590,32 @@ when shown in factored form.
\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",
+ 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"
+}
+
+\end{chunk}
+
+\index{Maletzky, Alexander}
+\begin{chunk}{axiom.bib}
@article{Male16,
author = "Maletzky, Alexander",
title = {{Interactive Proving, HigherOrder Rewriting, and Theory Analysis
@@ 13614,6 +13867,18 @@ when shown in factored form.
\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{Melquiond, Guillaume}
\begin{chunk}{axiom.bib}
@article{Melq12,
@@ 15131,6 +15396,17 @@ when shown in factored form.
\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{Traytel, Dmitriy}
\index{Berghofer, Stefan}
\index{Nipkow, Tobias}
@@ 15425,6 +15701,28 @@ when shown in factored form.
\end{chunk}
+\index{Windsteiger, Wolfgang}
+\begin{chunk}{axiom.bib}
+@article{Wind06,
+ author = "Windsteiger, Wolfgang",
+ title = {{An automated prover for ZermeloFraenkel set theory in
+ Theorema}},
+ 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
+ theory.",
+ paper = "Wind06.pdf"
+}
+
+\end{chunk}
+
\index{Winskel, Glynn}
\begin{chunk}{axiom.bib}
@book{Wins93,
@@ 25404,6 +25702,44 @@ Proc ISSAC 97 pp172175 (1997)
\end{chunk}
+\index{Paule, Peter}
+\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}",
+ 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"
+}
+
+\end{chunk}
+
\index{Stoutemyer, David R.}
\begin{chunk}{axiom.bib}
@article{Stou79,
@@ 37507,7 +37843,8 @@ SIGSAM Communications in Computer Algebra, 157 2006
year = "2008",
pages = "133140",
isbn = "978159593904",
 link = "\url{http://www.risc.jku.at/publications/download/risc_3427/Ka01.pdf}",
+ link =
+ "\url{http://www.risc.jku.at/publications/download/risc_3427/Ka01.pdf}",
abstract =
"A new method is proposed for finding the logarithmic part of an
integral over an algebraic function. The method uses Groebner bases
@@ 47505,6 +47842,28 @@ SIAM J. Numer. Anal. 19 12861304. (1982)
\index{Dolzmann, Andreas},
\index{Sturm, Thomas}
\begin{chunk}{axiom.bib}
+@misc{Dolz96,
+ author = "Dolzmann, Andreas and Sturm, Thomas",
+ title = {{Redlog User Manual Edition 1.0}},
+ year = "1996",
+ abstract =
+ "REDLOG stands for REDUCE LOGIC system. It provides an extension
+ of the computer algebra system reduce to a ``computer logic system''
+ implementing symbolic algorithms on firstorder formulas wrt.
+ temporarily fixed firstorder languages and theories. Underlying
+ theories currently available are ordered fields and discretely
+ valued fields. Though the focus of the implemented algorithms is on
+ effective quantier elimination and simplication of quantierfree
+ formulas, REDLOG is intended and designed as an allpurpose system.
+ REDLOG is freely available to the scientic community.",
+ paper = "Dolz96.pdf"
+}
+
+\end{chunk}
+
+\index{Dolzmann, Andreas},
+\index{Sturm, Thomas}
+\begin{chunk}{axiom.bib}
@article{Dolz97b,
author = "Dolzmann, Andreas and Sturm, Thomas",
title = {{REDLOG: Computer Algebra meets Computer Logic}},
@@ 47852,6 +48211,97 @@ A.E.R.E. Report R.8730. HMSO. (1977)
\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",
+ 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}",
+ 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"
+}
+
+\end{chunk}
+
+\index{Erascu, Madalina}
+\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"
+}
+
+\end{chunk}
+
\subsection{F} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Fateman, Richard J.}
@@ 48084,6 +48534,34 @@ Invent. Math., vol. 121, 1995, pp. 211222.
\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}
+
\index{von zur Gathen, Joachim}
\index{Giesbrecht, Mark}
\begin{chunk}{ignore}
@@ 48187,6 +48665,30 @@ J. Comput. Appl. Math. 6 295302. (1980)
\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{Gill, P. E.}
\index{Miller, G. F.}
\begin{chunk}{ignore}
@@ 48395,6 +48897,33 @@ J. of Pure and Applied Algebra, 45, 225240 (1987)
\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{Grabmeier, Johannes}
\begin{chunk}{axiom.bib}
@misc{Grab91a,
@@ 49205,6 +49734,208 @@ Springer Verlag Heidelberg, 1989, ISBN 0387969802
\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"
+}
+
+\end{chunk}
+
+\index{Khan, Muhammad Taimoor}
+\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",
+ 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{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"
+}
+
+\end{chunk}
+
+\index{Khan, Muhammad Taimoor}
+\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"
+}
+
+\end{chunk}
+
+\index{Khan, Muhammad Taimoor}
+\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"
+}
+
+\end{chunk}
+
+\index{Khan, Muhammad Taimoor}
+\index{Schreiner, Wolfgang}
+\begin{chunk}{axiom.bib}
+@article{Khan12b,
+ author = "Khan, Muhammad Taimoor and Schreiner, Wolfgang",
+ 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"
+}
+
+\end{chunk}
+
+\index{Khan, Muhammad Taimoor}
+\index{Schreiner, Wolfgang}
+\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",
+ 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"
+}
+
+\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{Khan, Muhammad Taimoor}
\begin{chunk}{axiom.bib}
@phdthesis{Khan14,
author = "Khan, Muhammad Taimoor",
@@ 49365,6 +50096,101 @@ Journal of Symbolic Computation (1989) 7, 445456
\end{chunk}
+\index{Kreinovich, Vladik}
+\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{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{Kutsia, Temur}
+\index{Marin, Mircea}
+\begin{chunk}{axiom.bib}
+@techreport{Kuts12,
+ author = "Kutsia, Temur and Marin, Mircea",
+ title = {{Solving, Reasoning, and Programming in Common Logic}},
+ 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"
+}
+
+\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"
+}
+
+\end{chunk}
+
\subsection{L} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Lamport, Leslie}
@@ 49937,6 +50763,21 @@ Mathematical Surveys. 3 Am. Math. Soc., Providence, RI. (1966)
\end{chunk}
+\index{Markov, Andrei A.}
+\begin{chunk}{axiom.bib}
+@incollection{Mark62,
+ author = "Markov, Andrei .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"
+}
+
+\end{chunk}
+
\index{Marshak, U.}
\begin{chunk}{axiom.bib}
@misc{Mars07,
@@ 49957,6 +50798,46 @@ Mathematical Surveys. 3 Am. Math. Soc., Providence, RI. (1966)
\end{chunk}
+\index{Mayrhofer, Gunther}
+\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",
+ 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{Mayero, Micaela}
\index{Delahaye, David}
\begin{chunk}{axiom.bib}
@@ 50345,6 +51226,85 @@ Journal of the ACM, Vol. 25, No. 2, April 1978, pp. 271282
\end{chunk}
+\index{Neuper, Walther}
+\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"
+}
+
+\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",
+ 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{Nijenhuis}
\index{Wilf}
\begin{chunk}{ignore}
@@ 50363,6 +51323,31 @@ ACM Trans. Math. Softw. 5 118125. (1979)
\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}
+
\subsection{O} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{chunk}{axiom.bib}
@@ 50745,6 +51730,60 @@ Acta Math. 68 (1937) 145254.
\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",
+ link =
+ "\url{http://www.risc.jku.at/publications/download/risc_3913/PopJeb.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"
+}
+
+\end{chunk}
+
+\index{Popov, Nikolaj}
+\index{Jebelean, Tudor}
+\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}",
+ 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"
+}
+
+\end{chunk}
+
\index{Powell, M. J. D.}
\begin{chunk}{ignore}
\bibitem[Powell 70]{Pow70} Powell M J D.
@@ 51298,6 +52337,24 @@ Num. Math. 16 205223. (1970)
\end{chunk}
\index{Schreiner, Wolfgang}
+\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"
+}
+
+\end{chunk}
+
+\index{Schreiner, Wolfgang}
\index{DanielczykLanderl, Werner}
\index{Marin, Mircea}
\index{St\"ocher, Wolfgang}
@@ 51325,6 +52382,34 @@ Num. Math. 16 205223. (1970)
\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"
+}
+
+\end{chunk}
+
\index{Schoenberg, I. J.}
\index{Whitney, A.}
\begin{chunk}{ignore}
@@ 51352,6 +52437,16 @@ Software Practice and Experience. 6(1) (1976)
\end{chunk}
+\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{von Seggern, David Henry}
\begin{chunk}{axiom.bib}
@book{Segg93,
@@ 52066,6 +53161,20 @@ Linear Algebra and Appl. 28 285303. 1979
\end{chunk}
+\index{Winkler, Franz}
+\begin{chunk}{axiom.bib}
+@misc{Wink95,
+ author = "Winkler, Franz",
+ title = {{Computer Algebra  Problems and Developments}},
+ year = "1995",
+ abstract =
+ "Recent developments in computer algebra are discussed using simple
+ but illustrative examples",
+ paper = "Wink95.pdf"
+}
+
+\end{chunk}
+
\index{Wisbauer, R.}
\begin{chunk}{ignore}
\bibitem[Wisbauer 91]{Wis91} Wisbauer, R.
diff git a/changelog b/changelog
index 382520f..70c7924 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+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
20171109 tpd books/bookvolbib add references
20171031 tpd src/axiomwebsite/patches.html 20171031.03.tpd.patch
diff git a/patch b/patch
index b3912fb..be5dc91 100644
 a/patch
+++ b/patch
@@ 2,691 +2,1080 @@ books/bookvolbib add references
Goal: Proving Axiom Correct
\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
@misc{Mesh05,
 author = "Meshveliani, Sergei D.",
 title = {{Term rewriting, Equationional Reasoning, Automatic proofs}},
 link = "\url{ftp://ftp.botik.ru/pub/local/Mechveliani/dumatel/1.02/}",
 year = "2005",
 paper = "Mesh05.pdf"
+@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{Davenport, James H.}
+\index{Gonthier, Georges}
+\index{Mahboubi, Assia}
+\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@misc{Dave98,
 author = "Davenport, James H.",
 title = {{Is Computer Algebra the same as Computer Mathematics?}},
 year = "1998",
 comment = "Talk for British Colloquium for Theoretical Computer Science"
+@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",
+ 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",
+ 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"
+}
+
+\end{chunk}
+
+\index{Neuper, Walther}
+\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"
}
\end{chunk}
\index{Th\'ery, Laurent}
+\index{Buchberger, Bruno}
\begin{chunk}{axiom.bib}
@article{Ther98,
 author = "Thery, Laurent",
 title = {{A Certified Version of Buchberger's Algorithm}},
 journal = "LNCS",
 volume = "1421",
 pages = "349364",
+@article{Buch01,
+ author = "Buchberger, Bruno",
+ title = {{Theorema: A Proving System Based on Mathematica}},
+ journal = "The Mathematica Journal",
+ volume = "8",
+ number = "2",
+ pages = "247252",
+ 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"
+}
+
+\end{chunk}
+
+\index{Kreinovich, Vladik}
+\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 =
 "We present a proof of Buchberger's algorithm that has been developed
 in the Coq proof assistant. The formulation of the algorithm in Coq
 can be efficiently compiled and used to do computation",
 paper = "Ther98.pdf"
+ "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{Cooley, James W.}
\index{Tukey, John W.}
+\index{Windsteiger, Wolfgang}
\begin{chunk}{axiom.bib}
@article{Cool65,
 author = "Cooley, James W. and Tukey, John W.",
 title = {{An Algorithm for the Machine Calculation of Complex Fourier
 Series}},
 journal = "Mathematics of Computation",
 volume = "19",
 number = "04",
 year = "1965"
+@article{Wind06,
+ author = "Windsteiger, Wolfgang",
+ title = {{An automated prover for ZermeloFraenkel set theory in
+ Theorema}},
+ 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{Rump, Siegfried M.}
+\index{Schreiner, Wolfgang}
\begin{chunk}{axiom.bib}
@article{Rump88,
 author = "Rump, Siegfried M.",
 title = {{Algebraic Computation, Numerical Computation and Verified
 Inclusions}},
 journal = "LNCS",
 volume = "296",
 pages = "177197",
 year = "1988",
 abstract =
 "The three different types of computation  the algebraic
 manipulation, the numerical computation and the computation of
 verified results  are aiming on different problems and deliver
 qualitatively different results, each method having its specific
 advantages for specific classes of problems. The following remarks
 give some thoughts on possible combinations of all three methods to
 obtain algorithms benefitting from the specific strength of either
 method.",
 paper = "Rump88.pdf"
+@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"
}
\end{chunk}
\index{Engelman, C.}
+\index{Paule, Peter}
\begin{chunk}{axiom.bib}
@inproceedings{Enge65,
 author = "Engelman, C.",
 title = {{A Program for OnLine Assistance in Symbolic Computation}},
 booktitle = "Proc. Fall Joint Comput. Conf. 2",
 year = "1965",
 publisher = "Spartan Books"
+@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}",
+ 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"
}
\end{chunk}
\index{Church, Alonzo}
+\index{Khan, Muhammad Taimoor}
\begin{chunk}{axiom.bib}
@article{Chur40,
 author = "Church, Alonzo",
 title = {{A Formulation of the Simple Theory of Types}},
 journal = "J. of Symbolic Logic",
 volume = "5",
 number = "2",
 year = "1940",
 pages = "5668",
+@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 =
 "The purpose of the present paper is to give a formulation of the
 simple theory of types which incorporates certain features of the
 calculus of $\lambda$conversion. A complete incorporation of the
 calculus of $\lambda$conversion into the theory of types is
 impossible if we require that $\lambda x$ and juxtaposition shall
 retain their respective meanings as an abstraction operator and as
 denoting the application of function to argument. But the present
 partial incorporation has certain advantages from the point of view of
 type theory and is offered as being of interest on this basis
 (whatever may be thought of the finally satisfactory character of the
 theory of types as a foundation for logic and mathematics).",
 paper = "Chur40.pdf"
+ "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{Redfern, D.}
+\index{Kryvolap, Andrii}
+\index{Nikitchenko, Mykola}
+\index{Schreiner, Wolfgang}
\begin{chunk}{axiom.bib}
@book{Redf98,
 author = "Redfern, D.",
 title = {{The Maple Handbook: Maple V Release 5}},
+@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",
 year = "1998"
+ 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{Sorge, Volker}
+\index{Khan, Muhammad Taimoor}
\begin{chunk}{axiom.bib}
@misc{Sorg96,
 author = "Sorge, Volker",
 title = {{Integration eines Computeralgebrasystems in eine logische
 Beweisumgebung }},
 school = "Univ. des Saarlandes",
 year = "1996",
 comment = "Master's thesis"
+@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"
}
\end{chunk}
\index{Farmer, William M.}
\index{Guttman, Joshua D.}
\index{Thayer, Javier}
+\index{Khan, Muhammad Taimoor}
\begin{chunk}{axiom.bib}
@article{Farm93a,
 author = "Farmer, William M. and Guttman, Joshua D. and Thayer, Javier",
 title = {{IMPS: An Interactive Mathematical Proof Systems}},
 journal = "J. of Automated Reasoning",
 volume = "11",
 pages = "213248",
 year = "1993",
+@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 =
 "IMPS is an interactive mathematical proof system intended as a
 generalpurpose too! formulating and applying mathematics in a
 familiar fashion. The logic of IMPS is based on a version of simple
 type theory with partial functions and subtypes. Mathematical
 specification and inference are performed relative to axiomatic
 theories, which can be related to one another via inclusion and theory
 interpretation. IMPS provides relatively large primitive inference
 steps to facilitate human control of the deductive process and human
 comprehension of the resulting proofs. An initial theory library con
 taining over a thousand repeatable proofs covers significant portions
 of logic, algebra, and analysis and provides some support for modeling
 applications in computer science.",
 paper = "Farm93a.pdf"
+ "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"
}
\end{chunk}
\index{Bundy, Alan}
\index{Wallen, Lincoln}
+\index{Khan, Muhammad Taimoor}
\begin{chunk}{axiom.bib}
@inproceedings{Bund75,
 author = "Bundy, Alan and Wallen, Lincoln",
 title = {{The UT Theorem Prover}},
 booktitle = "Catalogue of Artificial Intelligence Tools",
 pages = "132133",
 year = "1975",
+@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 =
 "The UT theorem prover is probably the best known natural deduction
 <153> theorem prover. It was written in LISP <34> by woody Bledsoe and
 his coworkers at the University of Texas, and is best described in
 (Bledsoe and Tyson 75]. The theorem prover embodies a Gentzenlike
 deduction system for firstorder predicate calculus, and many special
 purpose techniques, including: subgoaling, rewrite rules, controlled
 lorward chaining, controlled definition instantiation, conditional
 procedures, and induction. The prover, though powerful in its own
 right, is essentially interactive and thus allows the user of the
 prover to control the search for the proof in radical ways. The user
 can for example : add hypotheses, instruct the prover to instantiate
 certain variables with values, or instruct the prover as to which
 deduction rule to use next."
+ "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"
}
\end{chunk}
\index{Bledsoe, W.W.}
+\index{Khan, Muhammad Taimoor}
+\index{Schreiner, Wolfgang}
\begin{chunk}{axiom.bib}
@techreport{Bled83,
 author = "Bledsoe, W.W.",
 title = {{The UT Natural Deduction Prover}},
+@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",
+ 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"
+}
+
+\end{chunk}
+
+\index{Kutsia, Temur}
+\index{Marin, Mircea}
+\begin{chunk}{axiom.bib}
+@techreport{Kuts12,
+ author = "Kutsia, Temur and Marin, Mircea",
+ title = {{Solving, Reasoning, and Programming in Common Logic}},
type = "technical report",
 institution = "Univ. of Texas at Austin",
 year = "1983",
 number = "ATP17B"
}
+ 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"
+}
\end{chunk}
\index{Bledsoe, W.W.}
+\index{Kutsia, Temur}
+\index{Marin, Mircea}
\begin{chunk}{axiom.bib}
@inproceedings{Bled84,
 author = "Bledsoe, W.W.",
 title = {{Some Automatic Proofs in Analysis}},
 booktitle = "Automated Theorem Proving: After 25 Years",
 publisher = "American Mathematical Society",
 year = "1984"
+@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"
}
\end{chunk}
\index{Bledsoe, W.W.}
\index{Bruell, P.}
\index{Shostak, R.}
+\index{Erascu, Madalina}
\begin{chunk}{axiom.bib}
@techreport{Bled79,
 author = "Bledsoe, W.W. and Bruell, P. and Shostak, R.",
 title = {{A Prover for General Inequalities}},
+@techreport{Eras11,
+ author = "Erascu, Madalina",
+ title = {{Symbolic Computation and Program Verification. Proving
+ Partial Correctness and Synthesizing Optimal Algorithms}},
type = "technical report",
 institution = "Univ. of Texas at Austin",
 year = "1979",
 number = "ATP40A"
+ 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"
}
\end{chunk}
\index{Fitting, M.}
+\index{Khan, Muhammad Taimoor}
\begin{chunk}{axiom.bib}
@book{Fitt90,
 author = "Fitting, M.",
 title = {{Firstorder Logic and Automated Theorem Proving}},
 publisher = "SpringerVerlag",
 year = "1990",
 isbn = "9781461275152"
+@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"
}
\end{chunk}
\index{Gallier, Jean H.}
+\index{Khan, Muhammad Taimoor}
+\index{Schreiner, Wolfgang}
\begin{chunk}{axiom.bib}
@book{Gall86,
 author = "Gallier, Jean H.",
 title = {{Logic for Computer Science: Foundations of Automatic
 Theorem Proving}},
 publisher = "Harper and Row",
 year = "1986",
 isbn = "9780486780825"
+@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"
}
\end{chunk}
\index{Guessarian, Irene}
\index{Meseguer, Jose}
+\index{Khan, Muhammad Taimoor}
\begin{chunk}{axiom.bib}
@article{Gues87,
 author = "Guessarian, Irene and Meseguer, Jose",
 title = {{On the Axiomatization of ``IFTHENELSE''}},
 journal = "SIAM J. Comput.",
 volume = "16",
 numbrrer = "2",
 year = "1987",
 pages = "332357",
+@techreport{Khan11b,
+ author = "Khan, Muhammad Taimoor",
+ title = {{Towards a Behavioral Analysis of Computer Algebra
+ Programs}},
+ type = "technical report",
+ number = "1113",
+ year = "2011",
abstract =
 "The equationally complete proof system for ``ifthenelse'' of Bloom
 and Tindell is extended to a complete proof system for manyosrted
 algebras with extra operations, predicates and equations among
 those. We give similar completeness results for continuous algebras
 and program schemes (infinite trees) by the methods of algebraic
 semantics. These extensions provide a purely equational proof system
 to prove properties of functional programs over userdefinable data
 types.",
 paper = "Gues87.pdf"
+ "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{Cunningham, R.J.}
\index{Dick, A.J.J}
+\index{Erascu, Madalina}
+\index{Jebelean, Tudor}
\begin{chunk}{axiom.bib}
@article{Cunn85,
 author = "Cunningham, R.J. and Dick, A.J.J",
 title = {{Rewrite Systems on a Lattice of Types}},
 journal = "Acta Informatica",
 volume = "22",
 pages = "149169",
 year = "1985",
+@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",
+ 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}",
abstract =
 "Rewriting systems for partial algebras are developed by modifying
 the KnuthBendix completion algorithm to permit the use of
 latticestructured domains. Some problems with the original algorithm,
 such as the treatment of division rings, are overcome conveniently by
 this means. The use of a type lattice also gives a natural framework
 for specifying data types in Computer Science without overspecifying
 error situations. The soundness and meaning of the major concepts
 involed in rewriting systems are reviewed when applied to such
 structures.",
 paper = "Cunn85.pdf"
+ "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"
}
\end{chunk}
\index{Paulson, Lawrence C.}
+\index{Vajda, Robert}
+\index{Jebelean, Tudor}
+\index{Buchberger, Bruno}
\begin{chunk}{axiom.bib}
@article{Paul90,
 author = "Paulson, Lawrence C.",
 title = {{A Formulation of the Simple Theory of Types (for
 Isabelle}}},
 journal = "LNCS",
 volume = "417",
 pages = "246274",
 year = "1990",
+@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 =
 "Simple type theory is formulated for use with the generic theorem
 prover Isabelle. This requires explicit type inference rules. There
 are function, product, and subset types, which may be
 empty. Descriptions (the etaoperator) introduce the Axiom of
 Choice. Higherorder logic is obtained through reflection between
 formulae and terms of type bool. Recursive types and functions can be
 formally constructed. Isabelle proof procedures are described. The
 logic appears suitable for general mathematics as well as
 computational problems.",
 paper = "Paul90.pdf"
+ "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"
}
\end{chunk}
\index{Kelsey, Tom}
+\index{Mayrhofer, Gunther}
\begin{chunk}{axiom.bib}
@phdthesis{Kels99,
 author = "Kelsey, Tom",
 title = {{Formal Methods and Computer Algebra: A Larch Specification of
 AXIOM Categories and Functors}},
 school = "University of St Andrews",
 year = "1999",
 keywords = "axiomref"
+@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",
+ 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{Lee, Wonyeol}
\index{Sharma, Rahul}
\index{Aiken, Alex}
\begin{chunk}{axiom.bib}
@article{Wony18,
 author = "Lee, Wonyeol and Sharma, Rahul and Aiken, Alex",
 title = {{On Automatically Proving the Correctness of math.h
 Implementation}},
 journal = "Proc. ACM Programming Languages",
 volume = "2",
 number = "42",
 year = "2018",
 pages = "132",
 abstract =
 "Industry standard implementations of math.h claim (often without
 formal proof) tight bounds on floating point errors. We demonstrate a
 novel static analysis that proves these bounds and verifies the
 correctness of these implementations. Our key insight is a reduction
 of this verification task to a set of mathematical optimization
 problems that can be solved by offtheshelf computer algebra
 systems. We use this analysis to prove the correctness of
 implementations in Intel’s math library automatically. Prior to this
 work, these implementations could only be verified with significant
 manual effort.",
 paper = "Wony18.pdf"
}

\end{chunk}

\index{Daly, Timothy}
\begin{chunk}{axiom.bib}
@misc{Daly10,
 author = "Daly, Timothy",
 title = {{Intel Instruction Semantics Generator}},
 link = "\url{http://daly.axiomdeveloper.org/TimothyDaly_files/publications/sei/intel/intel.pdf}",
 abstract =
 "Given an Intel x86 binary, extract the semantics of the instruction
 stream as Conditional Concurrent Assignments (CCAs). These CCAs
 represent the semantics of each individual instruction. They can be
 composed to represent higher level semantics.",
 paper = "Daly10.pdf"
}

\end{chunk}

\index{Naylor, William A.}
\begin{chunk}{axiom.bib}
@phdthesis{Nayl00,
 author = "Naylor, Bill",
 title = {{Polynomial GCD Using Straight Line Program Representation}},
 school = "University of Bath",
 year = "2000",
 link = "\url{http://www.sci.csd.uwo.ca/~bill/thesis.ps}",
 abstract = "
 This thesis is concerned with calculating polynomial greatest common
 divisors using straight line program representation.

 In the Introduction chapter, we introduce the problem and describe
 some of the traditional representations for polynomials, we then talk
 about some of the general subjects central to the thesis, terminating
 with a synopsis of the category theory which is central to the Axiom
 computer algebra system used during this research.

 The second chapter is devoted to describing category theory. We follow
 with a chapter detailing the important sections of computer code
 written in order to investigate the straight line program subject.
 The following chapter on evalution strategies and algorithms which are
 dependant on these follows, the major algorith which is dependant on
 evaluation and which is central to our theis being that of equality
 checking. This is indeed central to many mathematical problems.
 Interpolation, that is the determination of coefficients of a
 polynomial is the subject of the next chapter. This is very important
 for many straight line program algorithms, as their noncanonical
 structure implies that it is relatively difficult to determine
 coefficients, these being the basic objects that many algorithms work
 on. We talk about three separate interpolation techniques and compare
 their advantages and disadvantages. The final two chapters describe
 some of the results we have obtained from this research and finally
 conclusions we have drawn as to the viability of the straight line
 program approach and possible extensions.

 Finally we terminate with a number of appendices discussing side
 subjects encountered during the thesis.",
 paper = "Nayl00.pdf"
}

\end{chunk}

\index{Shoup, Victor}
\begin{chunk}{axiom.bib}
@inproceedings{Shou93,
 author = "Shoup, Victor",
 title = {{Factoring Polynomials over Finite Fields:
 Asymptotic Complexity vs Reality*}},
 booktitle = "Proc. IMACS Symposium, Lille, France",
 year = "1993",
 link = "\url{http://www.shoup.net/papers/lille.pdf}",
 abstract =
 "This paper compares the algorithms by Berlekamp, Cantor and
 Zassenhaus, and Gathen and Shoup to conclude that (a) if large
 polynomials are factored the FFT should be used for polynomial
 multiplication and division, (b) Gathen and Shoup should be used if
 the number of irreducible factors of $f$ is small. (c) if nothing is
 know about the degrees of the factors then Berlekamp's algorithm
 should be used.",
 paper = "Shou93.pdf"
}

\end{chunk}

\index{Wang, Paul S.}
\begin{chunk}{axiom.bib}
@article{Wang78,
 author = "Wang, Paul S.",
 title = {{An Improved Multivariate Polynomial Factoring Algorithm}},
 journal = "Mathematics of Computation",
 volume = "32",
 number = "144",
 year = "1978",
 pages = "12151231",
 link = "\url{http://www.ams.org/journals/mcom/197832144/S00255718197805682843/S00255718197805682843.pdf}",
 abstract = "
 A new algorithm for factoring multivariate polynomials over the
 integers based on an algorithm by Wang and Rothschild is described.
 The new algorithm has improved strategies for dealing with the known
 problems of the original algorithm, namely, the leading coefficient
 problem, the badzero problem and the occurence of extraneous factors.
 It has an algorithm for correctly predetermining leading coefficients
 of the factors. A new and efficient padic algorith named EEZ is
 described. Basically it is a linearly convergent variablebyvariable
 parallel construction. The improved algorithm is generally faster and
 requires less store than the original algorithm. Machine examples with
 comparative timing are included.",
 paper = "Wang78.pdf"
}

\end{chunk}

\index{Baez, John C.}
\index{Stay, Mike}
\begin{chunk}{axiom.bib}
@misc{Baez09,
 author = "Baez, John C.; Stay, Mike",
 title = {{Physics, Topology, Logic and Computation: A Rosetta Stone}},
 link = "\url{http://arxiv.org/pdf/0903.0340v3.pdf}",
 abstract = "
 In physics, Feynman diagrams are used to reason about quantum
 processes. In the 1980s, it became clear that underlying these
 diagrams is a powerful analogy between quantum physics and
 topology. Namely, a linear operator behaves very much like a
 ``cobordism'': a manifold representing spacetime, going between two
 manifolds representing space. But this was just the beginning: simiar
 diagrams can be used to reason about logic, where they represent
 proofs, and computation, where they represent programs. With the rise
 of interest in quantum cryptography and quantum computation, it became
 clear that there is an extensive network of analogies between physics,
 topology, logic and computation. In this expository paper, we make
 some of these analogies precise using the concept of ``closed
 symmetric monodial category''. We assume no prior knowledge of
 category theory, proof theory or computer science.",
 paper = "Baez09.pdf"
}

\end{chunk}

\index{Dunstan, Martin}
\begin{chunk}{axiom.bib}
@misc{Duns00,
 author = "Dunstan, Martin N.",
 title = {{Adding Larch/Aldor Specifications to Aldor}},
 abstract =
 "We describe a proposal to add Larchstyle annotations to the Aldor
 programming language, based on our PhD research. The annotations
 are intended to be machinecheckable and may be used for a variety
 of purposes ranging from compiler optimizations to verification
 condition (VC) generation. In this report we highlight the options
 available and describe the changes which would need to be made to
 the compiler to make use of this technology.",
 paper = "Duns00.pdf",
 keywords = "axiomref"
}

\end{chunk}

\index{Thompson, Simon}
\begin{chunk}{axiom.bib}
@InProceedings{Thom01,
 author = "Thompson, Simon",
 title = {{Logic and dependent types in the Aldor Computer Algebra System}},
 booktitle = "Symbolic computation and automated reasoning",
 series = "CALCULEMUS 2000",
 year = "2001",
 location = "St. Andrews, Scotland",
 pages = "205233",
+
+\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",
link =
 "\url{http://axiomwiki.newsynthesis.org/public/refs/aldorcalc2000.pdf}",
 abstract =
 "We show how the Aldor type system can represent propositions of
 firstorder logic, by means of the 'propositions as types'
 correspondence. The representation relies on type casts (using
 pretend) but can be viewed as a prototype implementation of a modified
 type system with {\sl type evaluation} reported elsewhere. The logic
 is used to provide an axiomatisation of a number of familiar Aldor
 categories as well as a type of vectors.",
 paper = "Thom01.pdf",
 keywords = "axiomref"
}

\end{chunk}

\index{Newcombe, Chris}
\index{Rath, Tim}
\index{Zhang, Fan}
\index{Munteanu, Bogdan}
\index{Brooker, Marc}
\index{Deardeuff, Michael}
\begin{chunk}{axiom.bib}
@misc{Newc13,
 author = "Newcombe, Chris and Rath, Tim and Zhang, Fan and
 Munteanu, Bogdan and Brooker, Marc and Deardeuff, Michael",
 title = {{Use of Formal Methods at Amazon Web Services}},
 link = "\url{http://research.microsoft.com/enus/um/people/lamport/tla/formalmethodsamazon.pdf}",
 abstract =
 "In order to find subtle bugs in a system design, it is necessary to
 have a precise description of that design. There are at least two
 major benefits to writing a precise design; the author is forced to
 think more clearly, which helps eliminate ``plausible handwaving'',
 and tools can be applied to check for errors in the design, even while
 it is being written. In contrast, conventional design documents
 consist of prose, static diagrams, and perhaps pseudocode in an ad
 hoc untestable language. Such descriptions are far from precise; they
 are often ambiguous, or omit critical aspects such as partial failure
 or the granularity of concurrency (i.e. which constructs are assumed
 to be atomic). At the other end of the spectrum, the final executable
 code is unambiguous, but contains an overwhelming amount of detail. We
 needed to be able to capture the essence of a design in a few hundred
 lines of precise description. As our designs are unavoidably complex,
 we need a highlyexpressive language, far above the level of code, but
 with precise semantics. That expressivity must cover realworld
 concurrency and faulttolerance. And, as we wish to build services
 quickly, we wanted a language that is simple to learn and apply,
 avoiding esoteric concepts. We also very much wanted an existing
 ecosystem of tools. We found what we were looking for in TLA+, a
 formal specification language."
}

\end{chunk}

\index{O'Connor, Liam}
\begin{chunk}{axiom.bib}
@misc{OCon15,
 author = {O'Connor, Liam},
 title = {{Write Your Compiler by Proving It Correct}},
 year = "2015",
 link = "\url{http://liamoc.net/posts/20150823verifiedcompiler.html}",
 abstract =
 "Recently my research has been centered around the development of a
 selfcertifying compiler for a functional language with linear types
 called Cogent (see O'Connor et al. [2016]). The compiler works by
 emitting, along with generated lowlevel code, a proof in Isabelle/HOL
 (see Nipkow et al. [2002]) that the generated code is a refinement of
 the original program, expressed via a simple functional semantics in HOL.

 As dependent types unify for us the language of code and proof, my
 current endeavour has been to explore how such a compiler would look
 if it were implemented and verified in a dependently typed programming
 language instead. In this post, I implement and verify a toy compiler
 for a language of arithmetic expressions and variables to an idealised
 assembly language for a virtual stack machine, and explain some of the
 useful features that dependent types give us for writing verified
 compilers."
}

\end{chunk}

\index{Briggs, Keith}
\begin{chunk}{axiom.bib}
@misc{Brig04,
 author = "Briggs, Keith",
 title = {{Exact real arithmetic}},
 link = "\url{http://keithbriggs.info/documents/xrkenttalkpp.pdf}",
 year = "2004",
 paper = "Bri04.pdf"
}

\end{chunk}

\index{Fateman, Richard J.}
\index{Yan, Tak W.}
\begin{chunk}{axiom.bib}
@misc{Fate94a,
 author = "Fateman, Richard J.; Yan, Tak W.",
 title ={{Computation with the Extended Rational Numbers and an
 Application to Interval Arithmetic}},
 link = "\url{http://www.cs.berkeley.edu/~fateman/papers/extrat.pdf}",
 abstract = "
 Programming languages such as Common Lisp, and virtually every
 computer algebra system (CAS), support exact arbitraryprecision
 integer arithmetic as well as exect rational number computation.
 Several CAS include interval arithmetic directly, but not in the
 extended form indicated here. We explain why changes to the usual
 rational number system to include infinity and ``notanumber'' may be
 useful, especially to support robust interval computation. We describe
 techniques for implementing these changes.",
 paper = "Fate94a.pdf"
+ "\url{http://www.risc.jku.at/publications/download/risc_3913/PopJeb.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"
}
\end{chunk}

\index{Atkinson, Kendall}
\index{Han, Welmin}
\index{Stewear, David}
\begin{chunk}{axiom.bib}
@misc{Atki09,
 author = "Atkinson, Kendall and Han, Welmin and Stewear, David",
 title = {{Numerical Solution of Ordinary Differential Equations}},
 link =
 "\url{http://homepage.math.uiowa.edu/~atkinson/papers/NAODE_Book.pdf}",
 abstract = "
 This book is an expanded version of supplementary notes that we used
 for a course on ordinary differential equations for upperdivision
 undergraduate students and beginning graduate students in mathematics,
 engineering, and sciences. The book introduces the numerical analysis
 of differential equations, describing the mathematical background for
 understanding numerical methods and giving information on what to
 expect when using them. As a reason for studying numerical methods as
 a part of a more general course on differential equations, many of the
 basic ideas of the numerical analysis of differential equations are
 tied closely to theoretical behavior associated with the problem being
 solved. For example, the criteria for the stability of a numerical
 method is closely connected to the stability of the differential
 equation problem being solved.",
 paper = "Atki09.pdf"
+\end{chunk}
+
+\index{Popov, Nikolaj}
+\index{Jebelean, Tudor}
+\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}",
+ 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"
+}
+
+\end{chunk}
+
+\index{Schreiner, Wolfgang}
+\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"
+}
+
+\end{chunk}
+
+\index{Buchberger,B}
+\index{Craciun, A.}
+\index{Jebelean, T.}
+\index{Kovacs, L.}
+\index{Kutsia, T.}
+\index{Nakagawa, K.}
+\index{Piroi, F.}
+\index{Popov, N.}
+\index{Robu, J.}
+\index{Rosenkranz, M.}
+\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",
+ 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"
+}
+
+\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}
+\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"
+}
+
+\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"
}
\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index b24a432..b440695 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5854,6 +5854,8 @@ books/bookvolbib respect case in paper titles
books/bookvolbib add references
20171109.01.tpd.patch
books/bookvolbib add references
+20171113.01.tpd.patch
+books/bookvolbib add references

1.9.1