From 5efd8bede274fa3ff3dcb7ddcdeaa0c83a6d673c Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Mon, 27 Jun 2016 08:27:35 0400
Subject: [PATCH] buglist: add todo 339: missing side conditions
Goal: Correct Axiom Mathematics
=========================================================================
todo 339: missing side conditions
integrate((xb)^(1),x)
(1) log(x  b)
Type: Union(Expression(Integer),...)
should show the sidecondition x > b or should be log(abs(xb))

buglist  12 +
changelog  2 +
patch  575 +
src/axiomwebsite/patches.html  2 +
4 files changed, 23 insertions(+), 568 deletions()
diff git a/buglist b/buglist
index cd69374..83841cd 100644
 a/buglist
+++ b/buglist
@@ 1,7 +1,7 @@
=========================================================================
bug 7305:
todo 339:
+todo 340:
wish 1012:
meh 5:
errors 10016:
@@ 12,6 +12,16 @@ dup 50006:
nonextend 60077:
=========================================================================
+todo 339: missing side conditions
+
+integrate((xb)^(1),x)
+
+ (1) log(x  b)
+ Type: Union(Expression(Integer),...)
+
+should show the sidecondition x > b or should be log(abs(xb))
+
+=========================================================================
bug 7303: Duplicate signature in )show ALIST
parts : % > List(Record(key: Key,entry: Entry))
diff git a/changelog b/changelog
index 34c6aab..a3cd4c0 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20160627 tpd src/axiomwebsite/patches.html 20160627.01.tpd.patch
+20160627 tpd buglist: add todo 339: missing side conditions
20160626 tpd src/axiomwebsite/patches.html 20160626.10.tpd.patch
20160626 tpd books/bookvolbib Axiom Citations in the Literature
20160626 tpd src/axiomwebsite/patches.html 20160626.09.tpd.patch
diff git a/patch b/patch
index 83a346c..ecc6842 100644
 a/patch
+++ b/patch
@@ 1,573 +1,14 @@
books/bookvolbib Axiom Citations in the Literature
+buglist: add todo 339: missing side conditions
Goal: Axiom Literate Programming
+Goal: Correct Axiom Mathematics
\index{Prevosto, Virgile}
\index{Doligez, Damien}
\begin{chunk}{axiom.bib}
@article{Prev02,
 author = "Prevosto, Virgile and Doligez, Damien",
 title = "Algorithms and proofs inheritance in the FOC language",
 journal = "J. Autom. Reasoning",
 volume = "29",
 number = "34",
 pages = "337363",
 keywords = "axiomref",
 paper = "Prev02.pdf",
 abstract =
 "In this paper, we present the FOC language, dedicated to the
 development of certified computer algebra libraries (that is sets of
 programs). These libraries are based on a hierarchy of implementations
 of mathematical structures. After presenting the core set of features
 of our language, we describe the static analyses, which reject
 inconsistent programs. We then show how we translate FOC definitions
 into OCAML and COQ, our target languages for the computational part
 and the proof checking, respectively."
}
+=========================================================================
+todo 339: missing side conditions
\end{chunk}
+integrate((xb)^(1),x)
\index{Schwarz, Fritz}
\begin{chunk}{axiom.bib}
@InProceedings{Schw02,
 author = "Schwarz, Fritz",
 title = "ALLTYPES: An algebraic language and type system",
 booktitle = "1st Int. Congress on Mathematical Software",
 year = "2002",
 isbn = "9812380485",
 location = "Beijing China",
 pages = "486500",
 keywords = "axiomref",
 paper = "Schw02.pdf",
 url =
"http://www.scai.fraunhofer.de/content/dam/scai/de/documents/MitarbeiterinnenundMitarbeiter/ICMS2002.pdf",
 abstract =
 "The software system ALLTYPES provides an environment that is
 particularly designed for developing software in differential
 algebra. Its most important features may be described as follows: A
 set of about thirty parametrized algebraic types is defined. Data
 objects represented by these types may be manipulated by more than one
 hundred polymorphic functions. Reusability of code is achieved by
 genericity and multiple inheritance. The user may extend the system by
 defining new types and polymorphic functions. A language comprising
 seven basic language constructs is defined for implementing
 mathematical algorithms. The easy manipulation of types is
 particularly supported due to a special portion of the language
 dedicated to manipulating typed objects, i.e. for performing
 userdefined or automatic type coercions. Type inquiries are also
 included in the language."
}
+ (1) log(x  b)
+ Type: Union(Expression(Integer),...)
\end{chunk}

\index{Adams, Andrew A.}
\index{Dunstan, Martin}
\index{Gottlieben, Hanne}
\index{Kelsey, Tom}
\index{Martin, Ursula}
\index{Owre, Sam}
\begin{chunk}{axiom.bib}
@InProceedings{Adam01,
 author = "Adams, Andrew A. and Dunstan, Martin and Gottlieben, Hanne and
 Kelsey, Tom and Martin, Ursula and Owre, Sam",
 title = "Computer algebra meets automated theorem proving: Integrating
 Maple and PVS",
 booktitle = "Theorem proving in higher order logics",
 series = "TPHOLs 2001",
 year = "2001",
 location = "Edinburgh, Scotland",
 pages = "2742",
 keywords = "axiomref",
 paper = "Adam01.pdf",
 abstract =
 "We describe an interface between version 6 of the Maple computer
 algebra system with the PVS automated theorem prover. The interface is
 designed to allow Maple users access to the robust and checkable proof
 environment of PVS. We also extend this environment by the provision
 of a library of proof strategies for use in real analysis. We
 demonstrate examples using the interface and the real analysis
 library. These examples provide proofs which are both illustrative and
 applicable to genuine symbolic computation problems."
}

\end{chunk}

\index{Antoine, Xavier}
\begin{chunk}{axiom.bib}
@article{Anto01,
 author = "Antoine, Xavier",
 title = "Microlocal diagonalization of strictly hyperbolic pseudodifferential
 systems and application to the design of radiation conditions in
 electromagnetism",
 journal = "SIAM J. Appl. Math",
 volume = "61",
 number = "6",
 pages = "18771905",
 year = "2001",
 keywords = "axiomref",
 abstract =
 "In [Commun. Pure Appl. Math. 28, 457478 (1975; Zbl 0332.35058)],
 M. E. Taylor described a constructive diagonalization method to
 investigate the reflection of singularities of the solution to
 firstorder hyperbolic systems. According to further works initiated
 by Engquist and Majda, this approach proved to be well adapted to the
 construction of artificial boundary conditions. However, in the case
 of systems governed by pseudodifferential operators with variable
 coefficients, Taylor’s method involves very elaborate calculations of
 the symbols of the operators. Hence, a direct approach may be
 difficult when dealing with highorder conditions.

 This motivates the first part of this paper, where a recursive
 explicit formulation of Taylor’s method is stated for microlocally
 strictly hyperbolic systems. Consequently, it provides an algorithm
 leading to symbolic calculations which can be handled by a computer
 algebra system. In the second part, an application of the method is
 investigated for the construction of local radiation boundary
 conditions on arbitrarily shaped surfaces for the transverse electric
 Maxwell system. It is proved that they are of complete order, provided
 the introduction of a new symbols class well adapted to the Maxwell
 system. Next, a complete secondorder condition is designed, and when
 used as an onsurface radiation condition [G. A. Kriegsmann,
 A. Taflove, and K. R. Umashankar, IEEE Trans. Antennas Propag. 35,
 153161 (1987; Zbl 0947.78571)], it can give rise to an ultrafast
 numerical approximate solution of the scattered field."
}

\end{chunk}

\index{Delliere, Stephane}
\begin{chunk}{axiom.bib}
@article{Dell01,
 author = "Delliere, Stephane",
 title = "On the links between triangular sets and dynamic constructable
 closure",
 journal = "J. Pure Appl. Algebra",
 volume = "163",
 number = "1",
 pages = "4968",
 year = "2001",
 keywords = "axiomref",
 abstract =
 "Two kinds of triangular systems are studied: normalized triangular
 polynomial systems (a weaker form of Lazard’s triangular sets
 [D. Lazard, Discrete Appl. Math. 33, No. 13, 147160 (1991; Zbl
 0753.13013)] and constructible triangular systems (involved in the
 dynamic constructible closure programs of T. GomezDíaz [Quelques
 applications de l'evaluation dynamique, Ph.D. Thesis, Universite de
 Limoges (1994)]. This paper shows that these notions are strongly
 related. In particular, combining the two points of view
 (constructible and polynomial) on the subject of squarefree
 conditions, it allows us to effect dramatic improvements in the
 dynamic constructible closure programs."
}

\end{chunk}

\index{Michler, Gerhard O.}
\begin{chunk}{axiom.bib}
@article{Mich01,
 author = "Michler, Gerhard O.",
 title = "The character values of multiplicityfree irreducible constituents
 of a transitive permutation representation",
 journal = "Kyushu J. Math.",
 volume = "55",
 number = "1",
 pages = "75106",
 year = "2001",
 keywords = "axiomref",
 url = "https://www.jstage.jst.go.jp/article/kyushujm/55/1/55\_1\_75/\_pdf",
 paper = "Mich01.pdf",
 abstract =
 "Let $G$ be a finite group and $M$ a subgroup of $G$. Let the
 permutation character of $G$ on the set of right cosets of $M$ be
 denoted by $(1_M)^G$. Any ordinary irreducible constituent of
 $(1_M)^G$ with multiplicity one is called a multiplicityfree
 constituent of $(1_M)^G$. In the paper under review the author gives
 an efficient algorithm to compute the values of any multiplicityfree
 constituent of $(1_M)^G$. The character value is in terms of the
 double coset decomposition of $M$ and related concepts concerning
 intersection matrices. The author uses this algorithm to determine the
 values of the multiplicityfree constituents of $(1_C)^{J_1}$, where
 $J_1$ is the smallest Janko group of order 175560 and $C$ is the
 centralizer of an involution in $J_1$. Using these, he then is able to
 compute the character table of $J_1$ which is already known."
}

\end{chunk}

\index{Rudnicki, Piotr}
\index{Schwarzweller, Christoph}
\index{Trybulec, Andrzej}
\begin{chunk}{axiom.bib}
@article{Rudn01,
 author = "Rudnicki, Piotr and Schwarzweller, Christoph and
 Trybulec, Andrzej",
 title = "Commutative algebra in the Mizar system",
 journal = "J. Symb. Comput.",
 volume = "32",
 number = "12",
 pages = "143169",
 year = "2001",
 keywords = "axiomref",
 url = "https://inf.ug.edu.pl/~schwarzw/papers/jsc01.pdf",
 paper = "Rudn01.pdf",
 abstract =
 "We report on the development of algebra in the Mizar system. This
 includes the construction of formal multivariate power series and
 polynomials as well as the definition of ideals up to a proof of the
 Hilbert basis theorem. We present how the algebraic structures are
 handled and how we inherited the past developments from the Mizar
 Mathematical Library (MML). The MML evolves and past contributions are
 revised and generalized. Our work on formal power series caused a
 number of such revisions. It seems that revising past developments
 with an intent to generalize them is a necessity when building a
 database of formalized mathematics. This poses a question: how much
 generalization is best?"
}

\end{chunk}

\index{Safouhi, Hassan}
\begin{chunk}{axiom.bib}
@article{Safo01,
 author = "Safouhi, Hassan",
 title = "Numerical evaluation of threecenter twoelectron Coulomb and
 hybrid integrals over $B$ functions using the $HD$ and
 $H\overline{D}$ methods and convergence properties",
 journal = "J. Math. Chem.",
 volume = "29",
 number = "3",
 pages = "213232",
 year = "2001",
 keywords = "axiomref",
 abstract =
 "The $B$ function is a product of a spherical $K$ Bessel function and
 a spherical harmonic. The integrals to be evaluated contain
 complicated expressions of finite hypergeometric functions and
 spherical $J$ Bessel functions. Sequence transformation techniques are
 used for the numerical evaluation of the integrals. Numerical examples
 illustrate the accuracy and the efficiency of the method."
}

\end{chunk}

\index{Thompson, Simon}
\begin{chunk}{ignore}
@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",
 keywords = "axiomref",
 paper = "Thom01.pdf",
 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."
}

\end{chunk}

\index{Poll, Erik}
\begin{chunk}{axiom.bib}
@misc{Poll99,
 author = "Poll, Erik",
 title = "The Type System of Axiom",
 year = "1999",
 url = "http://www.cs.ru.nl/E.Poll/talks/axiom.pdf",
 paper = "Poll99.pdf",
 keywords = "axiomref",
 abstract =
 "This is a slide deck from a talk on the correspondence between
 Axiom/Aldor types and Logic."
}

\end{chunk}

\index{Poll, Erik}
\index{Thompson, Simon}
\begin{chunk}{axiom.bib}
@misc{Pollxx,
 author = "Poll, Erik and Thompson, Simon",
 title = "Adding the axioms to Axiom. Toward a system of automated
 reasoning in Aldor",
 url =
"http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.1457&rep=rep1&type=ps",
 paper = "Pollxx.pdf",
 keywords = "axiomref",
 abstract = "
 This paper examines the proposal of using the type system of Axiom to
 represent a logic, and thus to use the constructions of Axiom to
 handle the logic and represent proofs and propositions, in the same
 way as is done in theorem provers based on type theory such as Nuprl
 or Coq.

 The paper shows an interesting way to decorate Axiom with pre and
 postconditions.

 The CurryHoward correspondence used is
 \begin{verbatim}
 PROGRAMMING LOGIC
 Type Formula
 Program Proof
 Product/record type (...,...) Conjunction
 Sum/union type \/ Disjunction
 Function type > Implication
 Dependent function type (x:A) > B(x) Universal quantifier
 Dependent product type (x:A,B(x)) Existential quantifier
 Empty type Exit Contradictory proposition
 One element type Triv True proposition
 \end{verbatim}"
}

\end{chunk}

\index{Poll, Erik}
\index{Thompson, Simon}
\begin{chunk}{axiom.bib}
@misc{Poll00,
 author = "Poll, Erik and Thompson, Simon",
 title = "Integrating Computer Algebra and Reasoning through the Type
 System of Aldor",
 paper = "P0ll00.pdf",
 keywords = "axiomref",
 year = "2000",
 abstract =
 "A number of combinations of reasoning and computer algebra systems
 have been proposed; in this paper we describe another, namely a way to
 incorporate a logic in the computer algebra system Axiom. We examine
 the type system of Aldor  the Axiom Library Compiler  and show
 that with some modifications we can use the dependent types of the
 system to model a logic, under the CurryHoward isomorphism. We give
 a number of example applications of the logic we construct and explain
 a prototype implementation of a modified typechecking system written
 in Haskell."
}

\end{chunk}

\index{Page, Bill}
\begin{chunk}{axiom.bib}
@misc{Page08,
 author = "Page, Bill",
 title = "Algebraist Network",
 url = "http://lambdatheultimate.org/node/2737",
 year = "2008",
 keywords = "axiomref"
}

\end{chunk}

\index{Poll, Erik}
\index{Thompson, Simon}
\begin{chunk}{axiom.bib}
@InProceedings{Poll00a,
 author = "Poll, Erik and Thompson, Simon",
 title = "Integrating Computer Algebra and Reasoning through the Type
 System of Aldor",
 booktitle = "Frontiers of Combining Systems",
 series = "Lecture Notes in Artificial Intelligence",
 year = "2000",
 isbn = "3540672818",
 location = "Nancy, France",
 pages = "136150",
 keywords = "axiomref"
}

\end{chunk}

\index{Davenport, James H.}
\begin{chunk}{axiom.bib}
@InProceedings{Dave00,
 author = "Davenport, James H.",
 title = "Abstract data types in computer algebra",
 booktitle = "Mathematical foundations of computer science",
 series = "MFCS 2000",
 year = "2000",
 location = "Bratislava, Slovakia",
 pages = "2135",
 keywords = "axiomref",
 abstract =
 "The theory of abstract data types was developed in the late 1970s and
 the 1980s by several people, including the ``ADJ'' group, whose work
 influenced the design of Axiom. One practical manifestation of this
 theory was the OBJ3 system. An area of computing that cries out for
 this approach is computer algebra, where the objects of discourse are
 mathematical, generally satisfying various algebraic rules. There have
 been various theoretical studies of this in the literature. The aim of
 this paper is to report on the practical applications of this theory
 within computer algebra, and also to outline some of the theoretical
 issues raised by this practical application. We also give a
 substantial bibliography."
}

\end{chunk}

\index{Weber, Andreas}
\begin{chunk}{axiom.bib}
@phdthesis{Webe93b,
 author = "Weber, Andreas",
 title = "Type Systems for Computer Algebra",
 school = "University of Tubingen",
 year = "1993",
 paper = "Webe93b.pdf",
 keywords = "axiomref",
 abstract =
 "An important feature of modern computer algebra systems is the support
 of a rich type system with the possibility of type inference. Basic
 features of such a type system are polymorphism and coercion between
 types. Recently the use of ordersorted rewrite systems was proposed
 as a general framework. We will give a quite simple example of a
 family of types arising in computer algebra whose coercion relations
 cannot be captured by a finite set of firstorder rewrite rules."
}

\end{chunk}

\index{Fateman, Richard J.}
\begin{chunk}{axiom.bib}
@InProceedings{Fate00,
 author = "Fateman, Richard J.",
 title = "Problem solving environments and symbolic computing",
 booktitle = "Enabling technologies for computational science",
 publisher = "Kluwer Academic Publishers",
 year = "2000",
 pages = "91102",
 keywords = "axiomref",
 paper = "Fate00.pdf",
 url = "http://people.eecs.berkeley.edu/~fateman/papers/psekluwer.pdf",
 abstract =
 "What role should be played by symbolic mathematical computation
 facilities in scientific and engineering ``problem solving
 environments''? Drawing upon standard facilities such as numerical and
 graphical libraries, symbolic computation should be useful for: The
 creation and manipulation of mathematical models; The production of
 custom optimized numerical software; The solution of delicate classes
 of mathematical problems that require handling beyond that available
 in traditional machinesupported floatingpoint computation. Symbolic
 representation and manipulation can potentially play a central
 organizing role in PSEs since their more general object representation
 allows a program to deal with a wider range of computational
 issues. In particular numerical, graphical, and other processing can
 be viewed as special cases of symbolic manipulation with interactive
 symbolic computing providing both an organizing backbone and the
 communication ``glue'' among otherwise dissimilar components"
}

\end{chunk}

\index{Hoang, Ngoc Minh}
\index{Petitot, Michel}
\index{Van er Hoeven, Joris}
\begin{chunk}{axiom.bib}
@article{Hoan00,
 author = "Hoang, Ngoc Minh and Petitot, Michel and Van er Hoeven, Joris",
 title = "Shuffle algebra and polylogarithms",
 journal = "Discrete Math.",
 volume = "225",
 number = "13",
 pages = "217230",
 year = "2000",
 keywords = "axiomref",
 paper = "Hoan00.pdf",
 abstract =
 "Generalized polylogarithms are defined as iterated integrals with
 respect to the two differential forms $\omega_0=\frac{dz}{z}$ and
 $\omega_1=\frac{dz}{(1z)}$. We give an algorithm which computes the
 monodromy of these special functions. This algorithm, implemented in
 AXIOM, is based on the computation of the associator $\Phi_{KZ}$ of
 Drinfel’d, in factorized form. The monodromy formulae involve special
 constants, called multiple zeta values. We prove that the algebra of
 polylogarithms is isomorphic to a shuffle algebra."
}

\end{chunk}

\index{Raab, C.G.}
\begin{chunk}{axiom.bib}
@article{Raab13,
 author = "Raab, C.G.",
 title = "Generalization of Risch's Algorithm to Special Functions",
 journal = "CoRR",
 volume = "abs/1305.1481",
 year = "2013",
 url = "http://arxiv.org/pdf/1305.1481v1.pdf",
 paper = "Raab13.pdf",
 abstract =
 "Symbolic integration deals with the evaluation of integrals in closed
 form. We present an overview of Risch's algorithm including recent
 developments. The algorithms discussed are suited for both indefinite
 and definite integration. They can also be used to compute linear
 relations among integrals and to find identities for special functions
 given by parameter integrals. The aim of this presentation is twofold:
 to introduce the reader to some basic ideas of differential algebra in
 the context of integration and to raise awareness in the physics
 community of computer algebra algorithms for indefinite and definite
 integration. "
}

\end{chunk}

\index{Houstis, Elias N.}
\index{Rice, John R.}
\begin{chunk}{axiom.bib}
@article{Hous00,
 author = "Houstis, Elias N. and Rice, John R.",
 title = "Future problem solving environments for computational science",
 journal = "Math. Comput. Simul.",
 volume = "54",
 number = "45",
 pages = "243257",
 year = "2000",
 keywords = "axiomref",
 abstract =
 "We review the current state of the Problem Solving Environment (PSE)
 field and make projections for the future. First, we describe the
 computing context, the definition of a PSE and the goals of a PSE. The
 stateoftheart is summarized along with the principal components and
 paradigms for building PSEs. The discussion of the future is given in
 three parts: future trends, scenarios for 2010/2025, and research
 issues to be addressed."
}

\end{chunk}

\index{Gallopoulos, Stratis}
\index{Houstis, Elias}
\index{Rice, John}
\begin{chunk}{axiom.bib}
@techreport{Gall92,
 author = "Gallopoulos, Stratis and Houstis, Elias and Rice, John",
 title = "Future Research Directions in Problem Solving Environments for
 Computational Science",
 institution = "Purdue University",
 year = "1992",
 type = "technical report",
 number = "CSDTR92032",
 paper = "Gall92.pdf",
 url =
"http://docs.lib.purdue.edu/cgi/viewcontent.cgi?article=1953\&context=cstech",
 keywords = "axiomref",
 abstract =
 "During the early 19605 some were visualizing that computers could
 provide a powerful problem solving environment (PSE) which would
 interact with scientists on their own terms. By the mid 1960s there
 were many attempts underway to create these PSEs, but the early
 1970s almost all of these attempts had been abandoned, because the
 technological infrastructure could not yet support PSEs in
 computational science. The dream of the 1960s can be the reality of
 the 1990s; high performance computers combined with better
 understanding of computing and computational science have put PSEs
 well within our reach."
}

\end{chunk}
+should show the sidecondition x > b or should be log(abs(xb))
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index a922046..1c4123f 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5412,6 +5412,8 @@ books/bookvol* add Mulders to ORE and LODO refs
books/bookvolbib Axiom Citations in the Literature
20160626.10.tpd.patch
books/bookvolbib Axiom Citations in the Literature
+20160627.01.tpd.patch
+buglist: add todo 339: missing side conditions

1.7.5.4