(************** Content-type: application/mathematica ************** CreatedBy='Mathematica 4.2' Mathematica-Compatible Notebook This notebook can be used with any Mathematica-compatible application, such as Mathematica, MathReader or Publicon. The data for the notebook starts with the line containing stars above. To get the notebook into a Mathematica-compatible application, do one of the following: * Save the data starting with the line of stars above into a file with a name ending in .nb, then open the file inside the application; * Copy the data starting with the line of stars above to the clipboard, then use the Paste menu command inside the application. Data for notebooks contains only printable 7-bit ASCII and can be sent directly in email or through ftp in text mode. Newlines can be CR, LF or CRLF (Unix, Macintosh or MS-DOS style). NOTE: If you modify the data for this notebook not in a Mathematica- compatible application, you must delete the line below containing the word CacheID, otherwise Mathematica-compatible applications may try to use invalid cache data. For more information on notebooks and Mathematica-compatible applications, contact Wolfram Research: web: http://www.wolfram.com email: info@wolfram.com phone: +1-217-398-0700 (U.S.) Notebook reader applications are available free of charge from Wolfram Research. *******************************************************************) (*CacheID: 232*) (*NotebookFileLineBreakTest NotebookFileLineBreakTest*) (*NotebookOptionsPosition[ 70609, 1846]*) (*NotebookOutlinePosition[ 99954, 2920]*) (* CellTagsIndexPosition[ 99860, 2914]*) (*WindowFrame->Normal*) Notebook[{ Cell[CellGroupData[{ Cell[TextData[{ "Algorithm Retrieval:\nConcept Clarification and Case Study in ", StyleBox["Theorema", FontSlant->"Italic"], " " }], "Title", TextAlignment->Center, TextJustification->0, FontSize->24], Cell["\<\ Bruno Buchberger Research Institute for Symbolic Computation Johannes Kepler University, Linz, Austria bruno.buchberger@jku.at\ \>", "Subtitle", TextAlignment->Center, TextJustification->0, FontSize->14], Cell[CellGroupData[{ Cell["Abstract", "Subsection"], Cell["\<\ Algorithm retrieval is a special case of mathematical knowledge retrieval, \ which is one of the fundamental problems of mathematical knowledge \ management.\ \>", "Text"], Cell["\<\ In this paper, we distinguish between various versions of the \ problem of algorithm retrieval focusing on the version which can only be \ appropriately formulated in the frame of formal logic. This is the following \ problem: \ \>", "Text"], Cell["\<\ Given formulae S[ p, q, ...] that specify properties of a couple of \ (algorithmic operations) p,q,... and a knowledge base K of formulae,\ \>", "Text", CellMargins->{{42, Inherited}, {Inherited, Inherited}}], Cell["\<\ find operations P, Q, ... (occurring in the vocabulary of K) such that S[ P, \ Q, ...] is a logical consequence of K. \ \>", "Text", CellMargins->{{42, Inherited}, {Inherited, Inherited}}], Cell["\<\ Considering candidate operations P, Q, ... in the vocabulary of K, the \ problem of checking whether or not S[ P, Q, ...] is a logical consequence of \ K, can be trivial, easy, moderately difficult or very difficult depending on \ how much knowledge on P, Q, ... is already contained in K. Accordingly, in \ this paper, we consider the following two instances of algorithm retrieval in \ a formal (logic based) setting:\ \>", "Text"], Cell[TextData[{ "K contains no knowledge on P, Q, ... except their (algorithmic) \ definitions. ", StyleBox["In this case,", FontWeight->"Bold"], " ", StyleBox["algorithm retrieval essentially is algorithm verification", FontWeight->"Bold"], "." }], "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{52.375, Inherited}, {Inherited, Inherited}}], Cell[TextData[{ "K contains so much knowledge on P, Q, ... that the proof of S[ P, Q, ...] \ from K becomes \"easy\" in the sense that it can be done by \"", StyleBox["symbolic computation", FontWeight->"Bold"], "\" (conditional equational proving, propositional proving, manipulation \ with bounded quantifiers etc.). ", StyleBox["This is the case which we consider to be desirable", FontWeight->"Bold"], ", i.e. good knowledge bases should contain sufficiently much knowledge for \ making algorithm retrieval less cumbersome than algorithm verification. In \ other words, as a tendency, one should always try to \"complete\" \ mathematical knowledge bases on given concepts to the extent that subsequent \ proving (and disproving) of additional statements about these concepts is \ \"easily\" possible by symbolic computation proving." }], "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{52.375, Inherited}, {Inherited, Inherited}}], Cell[TextData[{ "Furthermore, it may be the case that K contains no candidate operations P, \ Q, ... for which S[ P, Q, ...] is a logical consequence of K.", StyleBox[" In this case, algorithm retrieval becomes algorithm invention \ (algorithm synthesis).", FontWeight->"Bold"] }], "Text"], Cell[TextData[{ "We give a ", StyleBox["case study", FontWeight->"Bold"], " in which the distinction between the three basic cases and the dependence \ of algorithm retrieval on the contents of the knowledge base becomes clear. \ We demonstrate that ", StyleBox["algorithm retrieval in a knowledge base essentially is theorem \ proving", FontWeight->"Bold"], ", namely proving that the given specification of the algorithm(s), for \ algorithms that occur in the knowledge base, is a logical consequence of the \ information on these algorithms already stored in the knowledge base." }], "Text"], Cell[TextData[{ StyleBox["Keywords", FontWeight->"Bold"], ": algorithm retrieval, mathematical knowledge retrieval, symbolic \ computation proving, high\[Dash]school proving, proving by rewriting, \ physicists' proving, basic prover, complete knowledge for mathematical \ notions, algorithm verification, algorithm synthesis, program synthesis, \ decoupling of requirements, re\[Dash]usable algorithms, functors, requirement \ engineering, didactics of programming, sorting, merging, merge", "\[Dash]", "sort, ", StyleBox["Theorema", FontSlant->"Italic"], "." }], "Text"], Cell[TextData[{ StyleBox["Acknowledgement", FontWeight->"Bold"], ": Sponsored by FWF (\[CapitalODoubleDot]sterreichischer Fonds zur F\ \[ODoubleDot]rderung der Wissenschaftlichen Forschung; Austrian Science \ Foundation), project SFB 1302 (\"", StyleBox["Theorema", FontSlant->"Italic"], "\") of the SFB 013 (\"Scientific Computing\")." }], "Text"] }, Open ]], Cell[CellGroupData[{ Cell["Introduction", "Section"], Cell[TextData[{ "As any other information retrieval problem, the problem of algorithm \ retrieval is the problem of finding ", StyleBox["detailed information", FontWeight->"Bold"], " about an algorithm, e.g. code for the algorithm, under the assumption \ that ", StyleBox["some information", FontWeight->"Bold"], " about the algorithm, for example its name or its specification, is \ given." }], "Text"], Cell[TextData[{ "Of course this problem is only meaningful if we also specify the ", StyleBox["knowledge base", FontWeight->"Bold"], " in which the search should be carried out: libraries with journals and \ books in printed form, mathematical software systems like Mathematica or \ Maple, or information in digitized form accessible through the web. \ Currently, quite some effort is spent on \"digitizing\" printed mathematical \ papers, to add semantic information to digitized versions of mathematical \ papers and to turn digitized papers into papers in a formal language, see \ [Buchberger et al. 2003] for various research directions in digitization of \ mathematical knowledge. " }], "Text"], Cell["In this paper, we start from the situation that", "Text"], Cell["the given information on the algorithm, ", "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{52, Inherited}, {Inherited, Inherited}}], Cell["the knowledge base,", "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{52, Inherited}, {Inherited, Inherited}}], Cell["and the information to be found", "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{52.375, Inherited}, {Inherited, Inherited}}], Cell[TextData[{ "are ", StyleBox["presented as formulae in a logical language", FontWeight->"Bold"], ". We believe that this assumption will be realistic in the near future. In \ other words, we believe that only when mathematical information is available \ in completely formal presentation within a well", "\[Dash]", "defined logic, the more sophisticated versions of the information \ retrieval problem can be attacked." }], "Text"], Cell["\<\ Of course, on a first layer of algorithm retrieval, one thinks about finding \ details of an algorithm by a search through libraries given some keywords \ about the algorithm like \"Lagrange\", \"interpolation\", \"polynomials\" \ etc. These days, the solution of this problem, with the web, powerful search \ engines, special research and citations indices etc., is already in a state \ that is by far more pleasant than only 10 years ago and more progress is to \ be expected soon by the joint effort of the mathematical knowledge management \ community that recently established itself also as a formal organization at \ the 1st International Workshop of Mathematical Knowledge Management (MKM) \ initiated by this author with annual successor conferences well established \ both in Europe and the US, see [Asperti 2003]. \ \>", "Text"], Cell["\<\ However, we need to go a decisive step forward: In this paper, the \ information on the algorithm(s) is not given by \"external\" keywords but is \ given by formulae that describe properties of the algorithm(s), which we call \ \"specification\" of the algorithm(s), and the problem consists in deciding \ whether an algorithm (algorithms) meeting the given specification are \ available in the given formulae knowledge base. Needless to say that this \ problem is much more demanding than the algorithm retrieval problem based on \ textual information but one might argue whether this, more demanding, version \ of the algorithm retrieval problem really occurs \"in pratice\". Thus, let us \ start with an example that illustrates the substantial relevance of this \ formal version of algorithm retrieval:\ \>", "Text"], Cell[TextData[{ StyleBox["Example", FontWeight->"Bold"], ": In our \"lazy thinking\" automated algorithm invention (program \ synthesis) paradigm based on algorithm schemes and learning by failure, see \ [Buchberger 2003a], we showed how finding an algorithm 'sorted' satisfying \ the specification" }], "Text"], Cell[BoxData[ \(\[ForAll] \+\(is\[Dash]tuple[X]\)is\[Dash]sorted\[Dash]version[X, \ sorted[X]]\)], "Input"], Cell["\<\ can be automatically reduced to finding algorithms \ 'left\[Dash]split', 'right\[Dash]split', and 'merged' satisfying the \ specification\ \>", "Text"], Cell[BoxData[ \(is\[Dash]left - right - merge\[Dash]structure[left\[Dash]split, right\[Dash]split, merged]\)], "Input"], Cell["defined by", "Text"], Cell[BoxData[ RowBox[{ RowBox[{ RowBox[{\(\[ForAll] \+\(left\[Dash]split, right\[Dash]split, merged\)\), RowBox[{ RowBox[{"(", RowBox[{\(is\[Dash]left\[Dash]right\[Dash]merge\[Dash]structure[ left\[Dash]split, right\[Dash]split, merged]\), "\[DoubleLeftRightArrow]", "\[IndentingNewLine]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ { RowBox[{\(\(\[ForAll] \+\(is\[Dash]tuple[ X]\)\)\+\(\[Not] \ is\[Dash]trivial\[Dash]tuple[X]\)\), RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(left\[Dash]split[X] \[Precedes] X\)}, {\(is\[Dash]tuple[left\[Dash]split[X]]\)}, {\(right\[Dash]split[X] \[Precedes] X\)}, {\(is\[Dash]tuple[right\[Dash]split[X]]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}]}]}, {\(\[ForAll] \+\(is\[Dash]tuple[Y, Z]\)is\[Dash]tuple[ merged[Y, Z]]\)}, { RowBox[{\(\(\[ForAll] \+\(is\[Dash]tuple[X, Y, Z]\)\)\+\(\[Not] \ is\[Dash]trivial\[Dash]tuple[X]\)\), RowBox[{"(", RowBox[{ RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(left\[Dash]split[X] \[TildeTilde] Y\)}, {\(right\[Dash]split[X] \[TildeTilde] Z\)}, {\(is\[Dash]sorted[Y]\)}, {\(is\[Dash]sorted[Z]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}], "\[Implies]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(merged[Y, Z] \[TildeTilde] X\)}, {\(is\[Dash]sorted[merged[Y, Z]]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}]}], ")"}], " "}]} }, ColumnAlignments->{Left}], "}"}]}], ")"}]}]}], StyleBox["}", ShowContents->False]}], " "}]], "Input"], Cell["\<\ Here, (all) details of the specification predicate 'is\[Dash]sorted\ \[Dash]version' must be contained in the underlying knowledge base, see \ appendix.\ \>", "Text"], Cell["\<\ For completing the algorithm invention process we must, of course, find \ suitable algorithms 'left\[Dash]split', 'right\[Dash]split', and 'merged'. \ For this problem, it is not sufficient to do a textual search, in the \ knowledge base, for algorithms with names 'left\[Dash]split', \ 'right\[Dash]split', and 'merged': \ \>", "Text"], Cell["\<\ There may exist algorithms with these names in the knowledge base. \ However, they may not meet exactly the specification above (although their \ names may suggest this!).\ \>", "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{52, Inherited}, {Inherited, Inherited}}], Cell["\<\ There may exist algorithms with these names in the knowledge base \ and these algorithms may well meet the specification above but their \ definitions and properties may, literally, be quite distinct from the \ specification above. Thus, by a purely textual search, we cannot find out \ that these algorithms are appropriate .\ \>", "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{52, Inherited}, {Inherited, Inherited}}], Cell["\<\ There may exist algorithms whose names are quite distinct from the \ names above and these algorithms may well meet the specification above but, \ again, we cannot find this out by a purely textual search.\ \>", "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{52, Inherited}, {Inherited, Inherited}}], Cell[TextData[{ "Hence, \"finding\" in the existing knowledge base suitable algorithms that \ meet the above specification is a problem that goes far beyond purely textual \ search of appropriate algorithm names. Rather, the problem is essentially a \ theorem proving problem, which we call \"", StyleBox["logical algorithm retrieval problem", FontWeight->"Bold"], "\"", " and whose nature we will explore in the subsequent sections. We will \ study variants of the logical algorithm invention problem of increasing \ logical complexity." }], "Text"], Cell[TextData[{ "Note: All examples, in this paper, are presented in the ", StyleBox["Theorema", FontSlant->"Italic"], " system, see [Buchberger et al. 1997, 2000]. However, the analysis of the \ algorithm retrieval problem presented is quite general and independent of a \ particular system for computer\[Dash]supported theory exploration and also \ holds in the context of theory exploration without computer support." }], "Text"] }, Open ]], Cell[CellGroupData[{ Cell["\<\ The Trivial Variant: Logical Algorithm Retrieval = Formulae Identity\ \>", "Section"], Cell["\<\ In the first variant of the logical algorithm retrieval problem, we assume \ that the specification for the algorithms to be found (in our example, the \ algorithms 'left\[Dash]split', 'right\[Dash]split', and 'merged') and \ inductive definitions for these algorithms already appear in the given \ knowledge base. In our example, this means that the formulae\ \>", "Text"], Cell[BoxData[ RowBox[{\(\(\[ForAll] \+\(is\[Dash]tuple[ X]\)\)\+\(\[Not] is\[Dash]trivial\[Dash]tuple[X]\)\), RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(left\[Dash]split[X] \[Precedes] X\)}, {\(is\[Dash]tuple[left\[Dash]split[X]]\)}, {\(right\[Dash]split[X] \[Precedes] X\)}, {\(is\[Dash]tuple[right\[Dash]split[X]]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}]}]], "Input"], Cell[BoxData[ \(\[ForAll] \+\(is\[Dash]tuple[Y, Z]\)\((is\[Dash]tuple[ merged[Y, Z]])\)\)], "Input"], Cell[BoxData[ RowBox[{\(\(\[ForAll] \+\(is\[Dash]tuple[X, Y, Z]\)\)\+\(\[Not] is\[Dash]trivial\[Dash]tuple[X]\)\), RowBox[{ RowBox[{"(", RowBox[{ RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(left\[Dash]split[X] \[TildeTilde] Y\)}, {\(right\[Dash]split[X] \[TildeTilde] Z\)}, {\(is\[Dash]sorted[Y]\)}, {\(is\[Dash]sorted[Z]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}], "\[Implies]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(merged[Y, Z] \[TildeTilde] X\)}, {\(is\[Dash]sorted[merged[Y, Z]]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}]}], ")"}], "."}]}]], "Input"], Cell["and, for example, the formulae", "Text"], Cell[BoxData[GridBox[{ {\(left\[Dash]split[\[LeftAngleBracket]\[RightAngleBracket]]\ = \ \[LeftAngleBracket]\[RightAngleBracket]\)}, {\(\[ForAll] \+x\((left\[Dash]split[\[LeftAngleBracket]x\ \[RightAngleBracket]]\ = \[LeftAngleBracket]x\[RightAngleBracket])\)\)}, {\(\[ForAll] \+\(x, y, \ z\&_\)\((left\[Dash]split[\[LeftAngleBracket]x, y, z\&_\[RightAngleBracket]] = x\[Cup]left\[Dash]split[\[LeftAngleBracket]z\&_\ \[RightAngleBracket]])\)\)}, {\(right\[Dash]split[\[LeftAngleBracket]\[RightAngleBracket]]\ = \ \[LeftAngleBracket]\[RightAngleBracket]\)}, {\(\[ForAll] \+x\((right\[Dash]split[\[LeftAngleBracket]x\ \[RightAngleBracket]]\ = \[LeftAngleBracket]\[RightAngleBracket])\)\)}, {\(\[ForAll] \+\(x, y, \ z\&_\)\((right\[Dash]split[\[LeftAngleBracket]x, y, z\&_\[RightAngleBracket]] = y\[Cup]right\[Dash]split[\[LeftAngleBracket]z\&_\ \[RightAngleBracket]])\)\)} }, ColumnAlignments->{Left}]], "Input"], Cell[BoxData[GridBox[{ {\(merged[\[LeftAngleBracket]\[RightAngleBracket], \ \[LeftAngleBracket]\[RightAngleBracket]] = \[LeftAngleBracket]\ \[RightAngleBracket]\)}, {\(\[ForAll] \+\(y, \ y\&_\)\((merged[\[LeftAngleBracket]\ \[RightAngleBracket], \[LeftAngleBracket]y, \ y\&_\[RightAngleBracket]] = \[LeftAngleBracket]y, \ y\&_\[RightAngleBracket])\)\)}, {\(\[ForAll] \+\(x, \ x\&_\)\((merged[\[LeftAngleBracket]x, \ x\&_\[RightAngleBracket], \[LeftAngleBracket]\ \[RightAngleBracket]] = \[LeftAngleBracket]x, \ x\&_\[RightAngleBracket])\)\)}, { RowBox[{\(\[ForAll] \+\(x, \ x\&_, y, \ y\&_\)\), RowBox[{"(", RowBox[{\(merged[\[LeftAngleBracket]x, \ x\&_\[RightAngleBracket], \[LeftAngleBracket]y, \ y\&_\[RightAngleBracket]]\), " ", "=", RowBox[{"{", GridBox[{ {\(x\[Cup] merged[\[LeftAngleBracket]x\&_\[RightAngleBracket]\ , \[LeftAngleBracket]y, \ y\&_\[RightAngleBracket]] \[DoubleLeftArrow] \ x > y\)}, {\(y\[Cup] merged[\[LeftAngleBracket]x, \ x\&_\[RightAngleBracket], \ \[LeftAngleBracket]y\&_\[RightAngleBracket]] \[DoubleLeftArrow] \(\[Not] x > y\)\)} }, ColumnAlignments->{Left}], "}"}]}], ")"}]}]} }, ColumnAlignments->{Left}]], "Input"], Cell["\<\ that give inductive definitions of 'left\[Dash]split', \ 'right\[Dash]split', and 'merged', already appear in the knowledge base. \ (Here and in the rest of the paper we assume that the knowledge base only \ contains formulae whose correctness has already been (automatically) proved \ w.r.t. the underlying theory that introduces the data type in which we are \ working, in our case the theory of tuples.)\ \>", "Text"], Cell["\<\ In this case, checking whether the algorithms 'left\[Dash]split', \ 'right\[Dash]split', and 'merged' meet the specification \ \>", "Text"], Cell[BoxData[ \(is\[Dash]left\[Dash]right\[Dash]merge\[Dash]structure[left\[Dash]split, right\[Dash]split, merged]\)], "Input"], Cell["\<\ is a trivial task in the exact sense that proving is a \ \"one\[Dash]line\" proof. \ \>", "Text"], Cell["\<\ Of course, still, this task would be trivial if the property of the \ algorithms 'left\[Dash]split', 'right\[Dash]split', and 'merged', in the \ knowledge base, were described by some logical variant (with different choice \ of the bound variables, with some re\[Dash]arrangement of the formulae etc.), \ for example by the variant\ \>", "Text"], Cell[BoxData[ RowBox[{\(\(\[ForAll] \+\(is\[Dash]tuple[ A]\)\)\+\(\[Not] is\[Dash]trivial\[Dash]tuple[A]\)\), RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(left\[Dash]split[A] \[Precedes] A\)}, {\(is\[Dash]tuple[left\[Dash]split[A]]\)}, {\(right\[Dash]split[A] < A\)}, {\(is\[Dash]tuple[right\[Dash]split[A]]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}]}]], "Input"], Cell[BoxData[ \(\[ForAll] \+\(is\[Dash]tuple[B, C]\)is\[Dash]tuple[ merged[B, C]]\)], "Input"], Cell[BoxData[ RowBox[{\(\(\[ForAll] \+\(is\[Dash]tuple[A, B, C]\)\)\+\(\[Not] is\[Dash]trivial\[Dash]tuple[A]\)\), RowBox[{"(", RowBox[{ RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(left\[Dash]split[A] \[TildeTilde] B\)}, {\(right\[Dash]split[A] \[TildeTilde] C\)}, {\(is\[Dash]sorted[B]\)}, {\(is\[Dash]sorted[C]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}], "\[Implies]", \(merged[B, C] \[TildeTilde] A\)}], ")"}]}]], "Input"], Cell[BoxData[ RowBox[{\(\(\[ForAll] \+\(is\[Dash]tuple[A, B, C]\)\)\+\(\[Not] is\[Dash]trivial\[Dash]tuple[A]\)\), RowBox[{ RowBox[{ RowBox[{"(", RowBox[{ RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(left\[Dash]split[A] \[TildeTilde] B\)}, {\(right\[Dash]split[A] \[TildeTilde] C\)}, {\(is\[Dash]sorted[B]\)}, {\(is\[Dash]sorted[C]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}], "\[Implies]", \(is\[Dash]sorted[merged[B, C]]\)}], ")"}], "."}]}]}]], "Input"], Cell["", "Text"] }, Open ]], Cell[CellGroupData[{ Cell["\<\ A Degenerate Variant: Logical Algorithm Retrieval = Algorithm Verification\ \>", "Section"], Cell["\<\ This variant of the logical algorithm retrieval problem is characterized by \ the fact that the knowledge base contains the inductive definitions of \ algorithm candidates without any further (proved) properties of the \ algorithms and we have to find out whether these candidates meet the given \ specification. In this variant, the algorithm retrieval problem is nothing \ else than an algorithm verification problem.\ \>", "Text"], Cell["\<\ In our example, this means that we would find the inductive definition of \ three algorithms, say 'l', 'r', 'm', in the knowledge base, for example,\ \>", "Text"], Cell[BoxData[GridBox[{ {\(l[\[LeftAngleBracket]\[RightAngleBracket]]\ = \[LeftAngleBracket]\ \[RightAngleBracket]\)}, {\(\[ForAll] \+x\((l[\[LeftAngleBracket]x\[RightAngleBracket]]\ = \ \[LeftAngleBracket]x\[RightAngleBracket])\)\)}, {\(\[ForAll] \+\(x, y, z\&_\)\((l[\[LeftAngleBracket]x, y, z\&_\[RightAngleBracket]] = x\[Cup]l[\[LeftAngleBracket]z\&_\[RightAngleBracket]])\)\)}, {\(r[\[LeftAngleBracket]\[RightAngleBracket]]\ = \[LeftAngleBracket]\ \[RightAngleBracket]\)}, {\(\[ForAll] \+x\((r[\[LeftAngleBracket]x\[RightAngleBracket]]\ = \ \[LeftAngleBracket]\[RightAngleBracket])\)\)}, {\(\[ForAll] \+\(x, y, z\&_\)\((r[\[LeftAngleBracket]x, y, z\&_\[RightAngleBracket]] = y\[Cup]r[\[LeftAngleBracket]z\&_\[RightAngleBracket]])\)\)} }, ColumnAlignments->{Left}]], "Input"], Cell[BoxData[GridBox[{ {\(m[\[LeftAngleBracket]\[RightAngleBracket], \[LeftAngleBracket]\ \[RightAngleBracket]] = \[LeftAngleBracket]\[RightAngleBracket]\)}, {\(\[ForAll] \+\(y, \ y\&_\)\((m[\[LeftAngleBracket]\ \[RightAngleBracket], \[LeftAngleBracket]y, \ y\&_\[RightAngleBracket]] = \[LeftAngleBracket]y, \ y\&_\[RightAngleBracket])\)\)}, {\(\[ForAll] \+\(x, \ x\&_\)\((m[\[LeftAngleBracket]x, \ x\&_\[RightAngleBracket], \[LeftAngleBracket]\ \[RightAngleBracket]] = \[LeftAngleBracket]x, \ x\&_\[RightAngleBracket])\)\)}, { RowBox[{\(\[ForAll] \+\(x, \ x\&_, y, \ y\&_\)\), RowBox[{"(", RowBox[{\(m[\[LeftAngleBracket]x, \ x\&_\[RightAngleBracket], \[LeftAngleBracket]y, \ y\&_\[RightAngleBracket]]\), " ", "=", RowBox[{"{", GridBox[{ {\(x\[Cup] m[\[LeftAngleBracket]x\&_\[RightAngleBracket], \ \[LeftAngleBracket]y, \ y\&_\[RightAngleBracket]] \[DoubleLeftArrow] \ x > y\)}, {\(y\[Cup] m[\[LeftAngleBracket]x, \ x\&_\[RightAngleBracket], \ \[LeftAngleBracket]y\&_\[RightAngleBracket]] \[DoubleLeftArrow] \(\[Not] x > y\)\)} }, ColumnAlignments->{Left}], "}"}]}], ")"}]}]} }, ColumnAlignments->{Left}]], "Input"], Cell["and we would have to prove that ", "Text"], Cell[BoxData[ \(\(\(is\[Dash]left\[Dash]right\[Dash]merge\[Dash]structure[l, r, m]\)\(.\)\)\)], "Input"], Cell[TextData[{ "In many cases, such proofs can be carried out completely automatically \ with current mathematical software systems like ", StyleBox["Theorema", FontSlant->"Italic"], ". We do not give the details of the appropriate proof for our example \ because, in this paper, our main emphasis will be on the non\[Dash]degenerate \ variant of the algorithm retrieval problem described in the next section. \ Note however that, typically, ", StyleBox["such algorithm verification proofs are non", FontWeight->"Bold"], "\[Dash]", StyleBox["trivial inductive proofs", FontWeight->"Bold"], "." }], "Text"] }, Open ]], Cell[CellGroupData[{ Cell["\<\ The Non\[Dash]Degenerate Variant: Logical Algorithm Retrieval = \ Symbolic Computation Proving\ \>", "Section"], Cell[CellGroupData[{ Cell["The Problem", "Subsubsection"], Cell["\<\ This variant of the logical algorithm retrieval problem is \ characterized by the fact that the knowledge base contains the inductive \ definitions of algorithm candidates together with a couple of (proved) \ properties of the algorithms that describe these algorithms \"completely\" \ and we have to find out whether these candidates meet the given \ specification. Here, the emphasis is on \"completeness\" of properties. We \ will expand on this notion in more detail below. In fact, this notion is the \ central notion in this paper. In this variant, the algorithm retrieval \ problem can be solved by \"easy\" proving, which more specifically is \ \"symbolic computation proving\" (\"proving by rewriting\", \ \"high\[Dash]school proving\", \"physicists' proving\").\ \>", "Text"], Cell["\<\ Before we go into an analysis of \"complete knowledge\" and \ \"symbolic computation proving\", we study the non\[Dash]degenerate variant \ of the algorithm retrieval problem in our example: \ \>", "Text"], Cell["\<\ We assume again that we find the inductive definition of three algorithms, \ say 'l', 'r', 'm', in the knowledge base, for example,\ \>", "Text"], Cell[BoxData[GridBox[{ {\(l[\[LeftAngleBracket]\[RightAngleBracket]]\ = \[LeftAngleBracket]\ \[RightAngleBracket]\)}, {\(\[ForAll] \+x\((l[\[LeftAngleBracket]x\[RightAngleBracket]]\ = \ \[LeftAngleBracket]x\[RightAngleBracket])\)\)}, {\(\[ForAll] \+\(x, y, z\&_\)\((l[\[LeftAngleBracket]x, y, z\&_\[RightAngleBracket]] = x\[Cup]l[\[LeftAngleBracket]z\&_\[RightAngleBracket]])\)\)}, {\(r[\[LeftAngleBracket]\[RightAngleBracket]]\ = \[LeftAngleBracket]\ \[RightAngleBracket]\)}, {\(\[ForAll] \+x\((r[\[LeftAngleBracket]x\[RightAngleBracket]]\ = \ \[LeftAngleBracket]\[RightAngleBracket])\)\)}, {\(\[ForAll] \+\(x, y, z\&_\)\((r[\[LeftAngleBracket]x, y, z\&_\[RightAngleBracket]] = y\[Cup]r[\[LeftAngleBracket]z\&_\[RightAngleBracket]])\)\)} }, ColumnAlignments->{Left}]], "Input"], Cell[BoxData[GridBox[{ {\(m[\[LeftAngleBracket]\[RightAngleBracket], \[LeftAngleBracket]\ \[RightAngleBracket]] = \[LeftAngleBracket]\[RightAngleBracket]\)}, {\(\[ForAll] \+\(y, \ y\&_\)\((m[\[LeftAngleBracket]\ \[RightAngleBracket], \[LeftAngleBracket]y, \ y\&_\[RightAngleBracket]] = \[LeftAngleBracket]y, \ y\&_\[RightAngleBracket])\)\)}, {\(\[ForAll] \+\(x, \ x\&_\)\((m[\[LeftAngleBracket]x, \ x\&_\[RightAngleBracket], \[LeftAngleBracket]\ \[RightAngleBracket]] = \[LeftAngleBracket]x, \ x\&_\[RightAngleBracket])\)\)}, { RowBox[{\(\[ForAll] \+\(x, \ x\&_, y, \ y\&_\)\), RowBox[{ RowBox[{"(", RowBox[{\(m[\[LeftAngleBracket]x, \ x\&_\[RightAngleBracket], \[LeftAngleBracket]y, \ y\&_\[RightAngleBracket]]\), " ", "=", RowBox[{"{", GridBox[{ {\(x\[Cup] m[\[LeftAngleBracket]x\&_\[RightAngleBracket], \ \[LeftAngleBracket]y, \ y\&_\[RightAngleBracket]] \[DoubleLeftArrow] \ x > y\)}, {\(y\[Cup] m[\[LeftAngleBracket]x, \ x\&_\[RightAngleBracket], \ \[LeftAngleBracket]y\&_\[RightAngleBracket]] \[DoubleLeftArrow] \(\[Not] x > y\)\)} }, ColumnAlignments->{Left}], "}"}]}], ")"}], "."}]}]} }, ColumnAlignments->{Left}]], "Input"], Cell["\<\ However, in addition, we also assume that the following (proved) properties \ is\[Dash]left\[Dash]right\[Dash]structure[l,r] and \ is\[Dash]merge\[Dash]structure[m] were already available in the knowledge \ base, where is\[Dash]left\[Dash]right\[Dash]structure and is\[Dash]merge\ \[Dash]structure are defined as follows:\ \>", "Text"], Cell[BoxData[ RowBox[{\(\[ForAll] \+\(l, r\)\), RowBox[{ RowBox[{"(", RowBox[{\(is\[Dash]left\[Dash]right\[Dash]structure[l, r]\), "\[DoubleLeftRightArrow]", "\[IndentingNewLine]", RowBox[{\(\(\[ForAll] \+\(is\[Dash]tuple[ X]\)\)\+\(\[Not] is\[Dash]trivial\[Dash]tuple[X]\)\), RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(l[X] \[Precedes] X\)}, {\(is\[Dash]tuple[l[X]]\)}, {\(r[X] \[Precedes] X\)}, {\(is\[Dash]tuple[r[X]]\)}, {\(\((l[X] \[CupCap] r[X])\) \[TildeTilde] X\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}]}]}], ")"}]}]}]], "Input"], Cell[BoxData[ RowBox[{\(\[ForAll] \+m\), RowBox[{"(", RowBox[{\(is\[Dash]merge\[Dash]structure[m]\), "\[DoubleLeftRightArrow]", "\[IndentingNewLine]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(\[ForAll] \+\(is\[Dash]tuple[Y, Z]\)is\[Dash]tuple[ m[Y, Z]]\)}, { RowBox[{\(\[ForAll] \+\(is\[Dash]tuple[Y, Z]\)\), RowBox[{"(", RowBox[{ RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(is\[Dash]sorted[Y]\)}, {\(is\[Dash]sorted[Z]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}], "\[Implies]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(\((Y \[CupCap] Z)\) \[TildeTilde] m[Y, Z]\)}, {\(is\[Dash]sorted[m[Y, Z]]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}]}], " ", ")"}]}]} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}]}], " ", ")"}]}]], "Input"], Cell["\<\ where '\[CupCap]' denotes concatenation.\ \>", "Text"], Cell["We now, again, have to prove that", "Text"], Cell[BoxData[ \(\(\(is\[Dash]left\[Dash]right\[Dash]merge\[Dash]structure[l, r, m]\)\(.\)\)\)], "Input"], Cell["Now, let's look to this proof:", "Text"] }, Open ]], Cell[CellGroupData[{ Cell["The Proof", "Subsubsection"], Cell["We assume", "Text"], Cell[BoxData[ \(is\[Dash]left\[Dash]right\[Dash]structure[l, r]\)], "Input"], Cell["and", "Text"], Cell[BoxData[ \(is\[Dash]merge\[Dash]structure[m]\)], "Input"], Cell["and we have to prove", "Text"], Cell[BoxData[ \(\(\(is\[Dash]left\[Dash]right\[Dash]merge\[Dash]structure[l, r, m]\)\(,\)\(\ \)\)\)], "Input"], Cell["i.e., for arbitrary X, Y, Z satisfying", "Text"], Cell[BoxData[GridBox[{ {\(is\[Dash]tuple[X]\)}, {\(\[Not] is\[Dash]trivial\[Dash]tuple[X]\)}, {\(is\[Dash]tuple[Y]\)}, {\(is\[Dash]tuple[Z]\)} }, ColumnAlignments->{Left}]], "Input"], Cell["and", "Text"], Cell[BoxData[GridBox[{ {\(l[X] \[TildeTilde] Y\)}, {\(r[X] \[TildeTilde] Z\)}, {\(is\[Dash]sorted[Y]\)}, {\(is\[Dash]sorted[Z]\)} }, ColumnAlignments->{Left}]], "Input"], Cell["we have to prove", "Text"], Cell[BoxData[GridBox[{ {\(l[X] \[Precedes] X\)}, {\(is\[Dash]tuple[l[X]]\)}, {\(r[X] \[Precedes] X\)}, {\(is\[Dash]tuple[r[X]]\)}, {\(is\[Dash]tuple[m[Y, Z]]\)}, {\(m[Y, Z] \[TildeTilde] X\)}, {\(\(is\[Dash]sorted[m[Y, Z]]\)\(.\)\)} }, ColumnAlignments->{Left}]], "Input"], Cell["\<\ Now, the first four goals are true by \ is\[Dash]left\[Dash]right\[Dash]structure[ l, r], the fifth goal is true by \ the assumptions and the first formula in is\[Dash]merge\[Dash]structure[ m], \ and the seventh formula is true by the assumptions and the third formula in \ is\[Dash]merge\[Dash]structure[ m].\ \>", "Text"], Cell["Proof of the sixth goal:", "Text"], Cell[BoxData[ RowBox[{\(m[Y, Z]\), OverscriptBox["\[TildeTilde]", Cell["(1)"]], \((Y \[CupCap] Z)\), OverscriptBox["\[TildeTilde]", Cell["(2)"]], \((l[X] \[CupCap] r[X])\), OverscriptBox["\[TildeTilde]", Cell["(3)"]], "X"}]], "Input"], Cell["\<\ and, hence, by transitivity and symmetry of \[TildeTilde] (see \ knowledge base in the appendix)\ \>", "Text"], Cell[BoxData[ \(m[Y, Z] \[TildeTilde] \(\(X\)\(.\)\)\)], "Input"], Cell["\<\ (1): By the assumptions and the second formula in is\[Dash]merge\ \[Dash]structure[ m].\ \>", "Text"], Cell["\<\ (2): By the assumptions and the property (see knowledge base in the \ appendix)\ \>", "Text"], Cell[BoxData[ \(\[ForAll] \+\(is\[Dash]tuple[A, B, Y, Z]\)\(\((\((A \[TildeTilde] Y \[And] B \[TildeTilde] Z)\) \[Implies] \((\((A \[CupCap] B)\) \[TildeTilde] \((Y \[CupCap] Z)\))\))\)\(.\)\)\)], "Input"], Cell["\<\ (3): By the last formula in is\[Dash]left\[Dash]right\[Dash]structure [l, r].\ \ \>", "Text"] }, Open ]], Cell[CellGroupData[{ Cell["\<\ Observation on the Proof Method and on Complete Knowledge Bases\ \>", "Subsubsection"], Cell[TextData[{ "Note that the above proof is neither trivial (i.e. just be renaming of \ bound variables and simple re\[Dash]arrangement of the formulae) nor \ \"difficult\". More exactly, the proof is carried out exclusively by ", StyleBox["\"rewrite steps\" (\"symbolic computation steps\", \"high", FontWeight->"Bold"], "\[Dash]", StyleBox["school proving steps\", \"physicists' proving steps\", \"proving \ by algebraic manipulation\")", FontWeight->"Bold"], ". These are steps that involve only the \"arbitrary but fixed\" technique \ for universally bound variables in goals, substition of terms for universally \ bound variables in formulae in the knowledge base, replacement of a term by \ another term whose equality or congruence modulo an equivalence is already \ known, propositional steps including the expansion of formulae containing \ case distinction, and special inference rules for bounded quantifiers. This \ kind of proving is typical for proofs in high\[Dash]school textbooks and also \ for \"derivations\" of formulae in applied mathematics, e.g. physics, where \ proofs normally do not involve alternating quantifiers ('\[ForAll] \[Exists] \ \[ForAll] ...' etc.) and, hence, no full\[Dash]fledged predicate logic \ proving with the necessity of finding term instances for proving existential \ propositions, nor induction proofs for formulae universally quantified over \ inductive data types is necessary. Within \"symbolic computation proving\", \ the only available proof technique for universally quantified goals in \ symbolic computation proving is the \"arbitrary but fixed\" technique. \ \"Symbolic computation proving\" does not need any big ideas for the \ ingenious choice of suitable instances for existentially quantified proof \ goals, it has a purely computational flavor. The only ingenuity that may be \ necessary lies in finding the appropriate ", StyleBox["sequence", FontSlant->"Italic"], " of proof steps leading to a successful proof." }], "Text"], Cell[TextData[{ "This notion of \"symbolic computation proving\", which is admittedly \ somewhat vague, is in some sense dual to the notion of a \"", StyleBox["complete knowledge base", FontWeight->"Bold"], "\": We consider a knowledge base K to be ", StyleBox["complete", FontSlant->"Italic"], " if all formulae that are logical consequences of formulae in K and are \ not yet in K can be obtained from formulae in K by symbolic computation \ proving (i.e. \"easy\" proving). Conversely, if we had a clear understanding \ of what \"complete\" knowledge bases are, we would say that symbolic \ computation proving is the proving sufficient for deriving all logical \ consequences from complete knowledge bases. Complete knowledge bases also \ could be (vaguely) characterized by saying that they admit a decision \ algorithm by symbolic computation." }], "Text"], Cell[TextData[{ "Of course, by the fundamental theorems of logic (Goedel's incompleteness \ theorem etc.) there exist knowledge bases (\"theories\") that cannot be \ completed. However, practically, many of the hundreds of theories that arise \ in the layered build\[Dash]up of mathematics ", StyleBox["can", FontSlant->"Italic"], " be completed in a quite concrete and natural way. Our strategic \ suggestion is that, in the systematic layered build", "\[Dash]", "up of mathematics (including both nonalgorithmic and algorithmic \ mathematics), ", StyleBox["after the introduction of any new, albeit intermediate and \ auxiliary concepts (operations, i.e. functions and predicates) by axioms or \ definitions, always complete the knowledge base for the new concepts by a \ systematic exploration of all possible interactions of the new concepts with \ all existing concepts and with themselves, before you proceed to introducing \ and exploring the next new concepts. ", FontWeight->"Bold"], "Ways for a systematic exploration and completion of the theories \ introduced by new concepts are described in [Buchberger 2000] and [Buchberger \ 2003b]." }], "Text"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["\<\ Another Degenerate Variant: Logical Algorithm Retrieval = Algorithm Invention\ \ \>", "Section"], Cell["\<\ This variant of the logical algorithm retrieval problem is characterized by \ the fact that the knowledge base does not contain any algorithms that meet \ the given specification. In this case, the logical algorithm retrieval \ problem becomes the algorithm invention (algorithm synthesis) problem.\ \>", "Text"], Cell["\<\ In our example, this means that we would have to synthesize algorithms 'l', \ 'r', 'm' satisfying\ \>", "Text"], Cell[BoxData[ \(is\[Dash]left\[Dash]right\[Dash]merge\[Dash]structure[l, r, m]\)], "Input"], Cell["\<\ from the operations available in the knowledge base. For example, the \ following algorithms could be synthesized\ \>", "Text"], Cell[BoxData[GridBox[{ {\(l[\[LeftAngleBracket]\[RightAngleBracket]]\ = \[LeftAngleBracket]\ \[RightAngleBracket]\)}, {\(\[ForAll] \+x\((l[\[LeftAngleBracket]x\[RightAngleBracket]]\ = \ \[LeftAngleBracket]x\[RightAngleBracket])\)\)}, {\(\[ForAll] \+\(x, y, z\&_\)\((l[\[LeftAngleBracket]x, y, z\&_\[RightAngleBracket]] = x\[Cup]l[\[LeftAngleBracket]z\&_\[RightAngleBracket]])\)\)}, {\(r[\[LeftAngleBracket]\[RightAngleBracket]]\ = \[LeftAngleBracket]\ \[RightAngleBracket]\)}, {\(\[ForAll] \+x\((r[\[LeftAngleBracket]x\[RightAngleBracket]]\ = \ \[LeftAngleBracket]\[RightAngleBracket])\)\)}, {\(\[ForAll] \+\(x, y, z\&_\)\((r[\[LeftAngleBracket]x, y, z\&_\[RightAngleBracket]] = y\[Cup]r[\[LeftAngleBracket]z\&_\[RightAngleBracket]])\)\)} }, ColumnAlignments->{Left}]], "Input"], Cell[BoxData[GridBox[{ {\(m[\[LeftAngleBracket]\[RightAngleBracket], \[LeftAngleBracket]\ \[RightAngleBracket]] = \[LeftAngleBracket]\[RightAngleBracket]\)}, {\(\[ForAll] \+\(y, \ y\&_\)\((m[\[LeftAngleBracket]\ \[RightAngleBracket], \[LeftAngleBracket]y, \ y\&_\[RightAngleBracket]] = \[LeftAngleBracket]y, \ y\&_\[RightAngleBracket])\)\)}, {\(\[ForAll] \+\(x, \ x\&_\)\((m[\[LeftAngleBracket]x, \ x\&_\[RightAngleBracket], \[LeftAngleBracket]\ \[RightAngleBracket]] = \[LeftAngleBracket]x, \ x\&_\[RightAngleBracket])\)\)}, { RowBox[{\(\[ForAll] \+\(x, \ x\&_, y, \ y\&_\)\), RowBox[{ RowBox[{ RowBox[{"(", RowBox[{\(m[\[LeftAngleBracket]x, \ x\&_\[RightAngleBracket], \[LeftAngleBracket]y, \ y\&_\[RightAngleBracket]]\), " ", "=", RowBox[{"{", GridBox[{ {\(x\[Cup] m[\[LeftAngleBracket]x\&_\[RightAngleBracket],\ \[LeftAngleBracket]y, \ y\&_\[RightAngleBracket]] \[DoubleLeftArrow] \ x > y\)}, {\(y\[Cup] m[\[LeftAngleBracket]x, \ x\&_\[RightAngleBracket], \ \[LeftAngleBracket]y\&_\[RightAngleBracket]] \[DoubleLeftArrow] \(\[Not] x > y\)\)} }, ColumnAlignments->{Left}], "}"}]}], ")"}], "."}]}]}]} }, ColumnAlignments->{Left}]], "Input"], Cell["\<\ In fact, this synthesis is automatically possible by the method described in \ [Buchberger 2003a] and other algorithm synthesis methods. The method in \ [Buchberger 2003a] synthesizes the algorithms 'l', 'r', 'm' while \ establishing, in parallel, a proof of the fact that\ \>", "Text"], Cell[BoxData[ \(\(\(is\[Dash]left\[Dash]right\[Dash]merge\[Dash]structure[l, r, m]\)\(.\)\)\)], "Input"], Cell[TextData[{ "Note that, similarly to the algorithm verification problem, the algorithm \ synthesis problem requires to come up with ", StyleBox[" non", FontWeight->"Bold"], "\[Dash]", StyleBox["trivial inductive proofs", FontWeight->"Bold"], " that go beyond the capability of \"symbolic computation proving\"." }], "Text"] }, Open ]], Cell[CellGroupData[{ Cell["Decoupling Coupled Algorithm Specifications", "Section"], Cell[CellGroupData[{ Cell["Coupled and Decoupled Specifications", "Subsubsection"], Cell["\<\ The relation between the two requirements (algorithm specifications)\ \>", "Text"], Cell[BoxData[ \(is\[Dash]left\[Dash]right\[Dash]merge\[Dash]structure[l, r, m]\)], "Input"], Cell["and", "Text"], Cell[BoxData[ \(is\[Dash]left\[Dash]right\[Dash]structure[l, r]\ \[And] is\[Dash]merge\[Dash]structure[m]\)], "Input"], Cell[TextData[{ "is a very interesting one: We call the second requirement \"", StyleBox["decoupled", FontWeight->"Bold"], "\", whereas the first one is \"", StyleBox["coupled", FontWeight->"Bold"], "\". This is an analogy, on the higher", "\[Dash]", "order level for algorithms, to the notion of decoupled and coupled systems \ of, say, algebraic or differential equations." }], "Text"], Cell[TextData[{ StyleBox["Decoupling coupled requirements is of eminent practical \ importance", FontWeight->"Bold"], ": Typically, for given algorithms, the correctness proof of decoupled \ requirements is much easier than the correctness proof of coupled \ requirements. Analogously, the synthesis of algorithms satisfying decoupled \ requirements is much easier than the synthesis of algorithms satisfying \ coupled requirements. Thus, finding a decoupled requirement that entails a \ coupled requirement is an important subgoal in the exploration of theories. \ In our example, the decoupled requirement" }], "Text"], Cell[BoxData[ \(is\[Dash]left\[Dash]right\[Dash]structure[l, r]\ \[And] is\[Dash]merge\[Dash]structure[m]\)], "Input"], Cell["entails the coupled requirement", "Text"], Cell[BoxData[ \(is\[Dash]left\[Dash]right\[Dash]merge\[Dash]structure[l, r, m]\)], "Input"], Cell["\<\ as we have shown in the section on algorithm retrieval by symbolic \ computation.\ \>", "Text"] }, Open ]], Cell[CellGroupData[{ Cell["\<\ Explicit and Non\[Dash]explicit Formulation of Specifications\ \>", \ "Subsubsection"], Cell["\<\ Note furthermore that, in our example, the definition of both decoupled \ requirements \ \>", "Text"], Cell[BoxData[ \(is\[Dash]left\[Dash]right\[Dash]structure[l, r]\)], "Input"], Cell["and", "Text"], Cell[BoxData[ \(is\[Dash]merge\[Dash]structure[m]\)], "Input"], Cell["\<\ are what we call \"explicit requirement formulations\" (or \ \"explicit problem descriptions\"): Formulae T (with the one free variable x) \ and P (with the two free variables x and y) are an explicit formulation of a \ requirement R for algorithms if \ \>", "Text"], Cell[BoxData[ \(\[ForAll] \+f\((R[ f] \[DoubleLeftRightArrow] \(\(\[ForAll] \+x\)\+\(T[x]\)P[x, f[x]]\))\)\)], "Input"], Cell["\<\ (and analogously for algorithms with more than one argument and \ also algorithms with more than one output \[Dash] which may also be conceived \ as two simultaneous algorithms). T, x, P, y are called the \"input formula\", \ \"input variable\", \"input / output formula\" (or, just, \"output \ formula\"), and \"output variable\" of the explicit requirement formulation, \ respectively.\ \>", "Text"], Cell["(More exactly, the above formula should be written:", "Text"], Cell[BoxData[ \(\[ForAll] \+f\((R[ f] \[DoubleLeftRightArrow] \(\(\[ForAll] \+x\)\+T P\_\(y \ \[LeftArrow] f[x]\)\))\)\)], "Input"], Cell["\<\ where '\[LeftArrow]' denotes the substitution operation.)\ \>", "Text"], Cell["\<\ For example, the requirement 'is\[Dash]merge\[Dash]structure' is explicitly \ defined by the input formula\ \>", "Text"], Cell[BoxData[ \(is\[Dash]tuple[Y, Z]\)], "Input"], Cell["with input variables 'Y' and 'Z' and the output formula", "Text"], Cell[BoxData[GridBox[{ {\(is\[Dash]tuple[M]\)}, { RowBox[{"(", RowBox[{ RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(is\[Dash]sorted[Y]\)}, {\(is\[Dash]sorted[Z]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}], "\[Implies]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(\((Y \[CupCap] Z)\) \[TildeTilde] M\)}, {\(is\[Dash]sorted[M]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}]}], " ", ")"}]} }, ColumnAlignments->{Left}]], "Input"], Cell["\<\ with the additional output variables 'M'.\ \>", "Text"], Cell["\<\ Also, the requirement 'is\[Dash]left\[Dash]right\[Dash]structure' is \ explicitly defined. For this we consider l and r as yielding two outputs for \ one input. The input formula is \ \>", "Text"], Cell[BoxData[ \(is\[Dash]tuple[X] \[And] \[Not] is - trivial - tuple[X]\)], "Input"], Cell["with input variable 'X' and the output formula is", "Text"], Cell[BoxData[GridBox[{ {\(L \[Precedes] X\)}, {\(is\[Dash]tuple[L]\)}, {\(R \[Precedes] X\)}, {\(is\[Dash]tuple[R]\)}, {\(\((L \[CupCap] R)\) \[TildeTilde] X\)} }, ColumnAlignments->{Left}]], "Input"], Cell[TextData[{ "with the additional ", StyleBox["two ", FontSlant->"Italic"], " output", " variables 'L', 'R'. " }], "Text"], Cell["\<\ Even the requirement \ 'is\[Dash]left\[Dash]rigth\[Dash]merge\[Dash]structure', although it is not \ decoupled, is explicitly defined by the formula in the introduction: We just \ look at the part \ \>", "Text"], Cell[BoxData[ RowBox[{\(\(\[ForAll] \+\(is\[Dash]tuple[X, Y, Z]\)\)\+\(\[Not] is\[Dash]trivial\[Dash]tuple[X]\)\), RowBox[{"(", RowBox[{ RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(left\[Dash]split[X] \[TildeTilde] Y\)}, {\(right\[Dash]split[X] \[TildeTilde] Z\)}, {\(is\[Dash]sorted[Y]\)}, {\(is\[Dash]sorted[Z]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}], "\[Implies]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(merged[Y, Z] \[TildeTilde] X\)}, {\(is\[Dash]sorted[merged[Y, Z]]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}]}], ")"}], " "}]], "Input"], Cell["\<\ of the definition, which describes the interaction between 'left\ \[Dash]split' and 'right\[Dash]split' on the one side and 'merged' on the \ other side. (The other parts are explicit as we have seen above.) This is a \ formula that can be read as an explicit definition with input formula\ \>", \ "Text"], Cell[BoxData[ \(is\[Dash]tuple[X, Y, Z]\)], "Input"], Cell["with input variables 'X', 'Y', 'Z' and output formula", "Text"], Cell[BoxData[ RowBox[{\(\[Not] is\[Dash]trivial\[Dash]tuple[X]\), "\[Implies]", RowBox[{"(", RowBox[{ RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(L \[TildeTilde] Y\)}, {\(R \[TildeTilde] Z\)}, {\(is\[Dash]sorted[Y]\)}, {\(is\[Dash]sorted[Z]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}], "\[Implies]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(M \[TildeTilde] X\)}, {\(is\[Dash]sorted[M]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}]}], ")"}]}]], "Input"], Cell[TextData[{ "with additional ", StyleBox["three ", FontSlant->"Italic"], "output variables 'L', 'R', and 'M'." }], "Text"], Cell["\<\ Here is an example of an algorithm requirement (specification) that \ is inherently non\[Dash]explicit, i.e. for which one cannot find an \ equivalent definition that is explicit:\ \>", "Text"], Cell[BoxData[ RowBox[{\(is\[Dash]canonic\[Dash]simplifier[t, \[Sigma], ~]\), "\[DoubleLeftRightArrow]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ { RowBox[{\(\[ForAll] \+\(t[x]\)\), Cell["(\[Sigma][x]~x)"]}]}, {\(\(\(\(\[ForAll]\)\(\ \)\)\+\(t[x, y]\)\) \(\((x~ y \[Implies] \((\[Sigma][x] = \[Sigma][ y])\))\)\(.\)\)\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}]}]], "Input"], Cell[TextData[StyleBox["I have an easy proof of the fact\nthat this \ requirement cannot be made explict\nbut, unfortunately, time and space\ndoes \ not permit me to give this proof\nhere.\n\n(Additional remark: I do hope \ that,\nin approximately 300 years from now,\nsomebody will find this paper \ and\ntry to find and write down a proof.)", "SmallText"]], "Text", CellMargins->{{2.4375, Inherited}, {Inherited, Inherited}}], Cell["\<\ More on coupled and decoupled, explicitly and non\[Dash]explicitly \ defined requirements will be contained in [Buchberger 2003 b].\ \>", "Text"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["Conclusion", "Section"], Cell["\<\ We have clarified the problem of \"logical algorithm retrieval\" \ and have emphasized the importance of two notions in this context:\ \>", \ "Text"], Cell["\<\ \"symbolic computation proving\" (\"high\[Dash]school proving\", \ \"physicists' proving\", \"algebraic proving\", \"table look\[Dash]up proving\ \", \"basic proving\")\ \>", "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{40, Inherited}, {Inherited, Inherited}}], Cell["\"complete knowledge base\".", "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{40, Inherited}, {Inherited, Inherited}}], Cell[TextData[{ "For the ", StyleBox["Theorema", FontSlant->"Italic"], " system, this has the following practical consequence: We will put \ decisive effort into implement a \"basic prover\" that can be used as an \ elementary building block for the problem of algorithm retrieval (and any \ other type of mathematical knowledge retrieval) and, at the same time, also \ as a sub", "\[Dash]", "prover for all other, more sophisticated special provers for the various \ areas of mathematics." }], "Text"] }, Open ]], Cell[CellGroupData[{ Cell["References", "Section"], Cell["\<\ [Asperti 2003] Proceedings of the 2nd International Conference on Mathematical Knowledge \ Management, Bologna, 2003.\ \>", "Text"], Cell[TextData[{ "[Buchberger et al. 1997] ", StyleBox["B. Buchberger, T. Jebelean, F. Kriftner, M. Marin, D. Vasaru.\nAn \ Overview on the Theorema Project.\nIn: W. Kuechlin (ed.), Proceedings of \ ISSAC'97 (International Symposium on Symbolic and Algebraic Computation, \ Maui, Hawaii, July 21", CharacterEncoding->"WindowsANSI"], "\[Dash]", StyleBox["23, 1997), ACM Press 1997, pp. 384", CharacterEncoding->"WindowsANSI"], "\[Dash]", StyleBox["391.", CharacterEncoding->"WindowsANSI"] }], "Text"], Cell[TextData[{ "[Buchberger 2000] ", StyleBox["B. Buchberger. \nTheory Exploration with ", CharacterEncoding->"WindowsANSI"], StyleBox["Theorema", FontSlant->"Italic", CharacterEncoding->"WindowsANSI"], StyleBox[". \nAnalele Universitatii Din Timisoara, Ser. Matematica", CharacterEncoding->"WindowsANSI"], "\[Dash]", StyleBox["Informatica, Vol. XXXVIII, Fasc.2, 2000, (Proceedings of SYNASC \ 2000, 2nd International Workshop on Symbolic and Numeric Algorithms in \ Scientific Computing, Oct. 4", CharacterEncoding->"WindowsANSI"], "\[Dash]", StyleBox["6, 2000, Timisoara, Rumania, T. Jebelean, V. Negru, A. Popovici \ eds.), pp. 9", CharacterEncoding->"WindowsANSI"], "\[Dash]", StyleBox["32. ", CharacterEncoding->"WindowsANSI"] }], "Text"], Cell[TextData[{ "[Buchberger et al. 2000] ", StyleBox["B. Buchberger,", CharacterEncoding->"WindowsANSI"], " C. Dupre, Tudor Jebelean, F. Kriftner, Koji Nakagawa, D. Vasaru, W. \ Windsteiger", StyleBox[". \nThe ", CharacterEncoding->"WindowsANSI"], StyleBox["Theorema", FontSlant->"Italic", CharacterEncoding->"WindowsANSI"], StyleBox[" Project: A Progress Report.\n", CharacterEncoding->"WindowsANSI"], "In: Symbolic Computation and Automated Reasoning (Proceedings of \ CALCULEMUS 2000, Symposium on the Integration of Symbolic Computation and \ Mechanized Reasoning, August 6\[Dash]7, 2000, St. Andrews, Scotland), M. \ Kerber and M. Kohlhase (eds.), A.K. Peters, Natick, Massachusetts, pp. 98", "\[Dash]", "113." }], "Text"], Cell["\<\ [Buchberger 2003a] B. Buchberger. Algorithm Invention and \ Verification by Lazy Thinking. In: D. Petcu, V. Negru, D. Zaharie, T. Jebelean (eds), Proceedings of SYNASC \ 2003 (Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, \ Romania, October 1\[Dash]4, 2003), Mirton Publishing, ISBN 973\[Dash]661\ \[Dash]104\[Dash]3, pp. 2\[Dash]26.\ \>", "Text"], Cell["\<\ [Buchberger 2003b] B. Buchberger. Methods for Systematic Mathematical Theory Exploration. Technical Report of the SFB (Special Research Area) Scientific Computing, \ October 2003, Johannes Kepler University, Linz, Austria.\ \>", "Text"], Cell["\<\ [Buchberger et al. 2003] B.Buchberger, G.Gonnet, M.Hazewinkel \ (eds.), Mathematical Knowledgement Management, special issue of the Journal \ Annals of Mathematics and Artificial Intelligence, Vol. 38, Nos. 1\[Dash]3, \ Kluwer Academic Publishers, 2003.\ \>", "Text"] }, Open ]], Cell[CellGroupData[{ Cell["Appendix: Knowledge Base for the Sorting Problem", "Section"], Cell[CellGroupData[{ Cell["Definitions ", "Subsubsection"], Cell[BoxData[ RowBox[{ RowBox[{\(\[ForAll] \+\(is\[Dash]tuple[X], Y\)\), RowBox[{"(", RowBox[{\(is\[Dash]sorted\[Dash]version[X, Y]\), " ", "\[DoubleLeftRightArrow]", RowBox[{"{", GridBox[{ {\(\(is\[Dash]tuple[Y]\)\(\ \)\)}, {\(\(X\)\(\[TildeTilde]\)\(Y\)\(\ \ \)\)}, {\(is\[Dash]sorted[Y]\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}]}], ")"}]}], "\[IndentingNewLine]"}]], "Input"], Cell[BoxData[ RowBox[{GridBox[{ {\(\(is\[Dash]sorted[\[LeftAngleBracket]\[RightAngleBracket]]\)\(\ \ \)\)}, {\(\[ForAll] \+x is\[Dash]sorted[\[LeftAngleBracket]x\[RightAngleBracket]]\)}, { RowBox[{\(\[ForAll] \+\(x, y, \(z\&-\)\)\), RowBox[{"(", RowBox[{\(is\[Dash]sorted[\[LeftAngleBracket]x, y, z\&_\[RightAngleBracket]]\), " ", "\[DoubleLeftRightArrow]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(x \[GreaterEqual] y\)}, {\(is\[Dash]sorted[\[LeftAngleBracket]y, z\&_\[RightAngleBracket]]\)} }, ColumnAlignments->{Left}], " ", StyleBox["}", ShowContents->False]}]}], ")"}]}]} }, ColumnAlignments->{Left}], "\[IndentingNewLine]"}]], "Input"], Cell[BoxData[GridBox[{ {\(\(\[LeftAngleBracket]\[RightAngleBracket]\)\(\[TildeTilde]\)\(\ \[LeftAngleBracket]\[RightAngleBracket]\)\(\ \)\)}, {\(\[ForAll] \+\(y, y\&_\)\((\[LeftAngleBracket]\[RightAngleBracket] \ \[NotTildeTilde] \[LeftAngleBracket]y, y\&_\[RightAngleBracket])\)\)}, {\(\(\[ForAll] \+\(x, x\&_, y\&_\)\((\[LeftAngleBracket]x, x\&_\[RightAngleBracket] \[TildeTilde] \ \[LeftAngleBracket]y\&_\[RightAngleBracket]\ \[DoubleLeftRightArrow] \((x \ \[Element] \[LeftAngleBracket]y\&_\[RightAngleBracket] \[And] \ \[LeftAngleBracket]x\&_\[RightAngleBracket] \[TildeTilde] dfo[x, \ \ \[LeftAngleBracket]y\&_\[RightAngleBracket]])\))\)\)\(\[IndentingNewLine]\) \)} }, ColumnAlignments->{Left}]], "Input"], Cell[BoxData[ RowBox[{GridBox[{ {\(\[ForAll] \+x\((x \[NotElement] \[LeftAngleBracket]\ \[RightAngleBracket])\)\)}, {\(\[ForAll] \+\(x, y, y\&_\)\((\((x \[Element] \ \[LeftAngleBracket]y, y\&_\[RightAngleBracket])\)\ \ \ \[DoubleLeftRightArrow] \((\((x = y)\) \[Or] x \[Element] \ \[LeftAngleBracket]y\&_\[RightAngleBracket])\))\)\)} }, ColumnAlignments->{Left}], "\[IndentingNewLine]"}]], "Input"], Cell[BoxData[ RowBox[{GridBox[{ {\(\[ForAll] \+a\((dfo[ a, \ \[LeftAngleBracket]\[RightAngleBracket]] = \ \[LeftAngleBracket]\[RightAngleBracket])\)\)}, { RowBox[{\(\[ForAll] \+\(a, x, x\&_\)\), RowBox[{"(", RowBox[{\(dfo[ a, \ \[LeftAngleBracket]x, x\&_\[RightAngleBracket]\ ]\), " ", "=", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(\[LeftAngleBracket]x\&_\[RightAngleBracket]\), "\[DoubleLeftArrow]", \(x = a\)}, {\(x\[Cup] dfo[a, \ \[LeftAngleBracket]x\&_\ \[RightAngleBracket]]\), "\[DoubleLeftArrow]", "otherwise"} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}]}], " ", ")"}]}]} }, ColumnAlignments->{Left}], "\[IndentingNewLine]"}]], "Input"], Cell[BoxData[GridBox[{ {\(\[ForAll] \+\(y\&_\)\((\[Not] \[LeftAngleBracket]\ \[RightAngleBracket] \[Succeeds] \[LeftAngleBracket]y\&_\[RightAngleBracket])\ \)\)}, {\(\[ForAll] \+\(x, x\&_\)\((\[LeftAngleBracket]x, x\&_\[RightAngleBracket] \[Succeeds] \[LeftAngleBracket]\ \[RightAngleBracket])\)\)}, {\(\[ForAll] \+\(x, x\&_, y, y\&_\)\((\[LeftAngleBracket]x, x\&_\[RightAngleBracket] \[Succeeds] \ \[LeftAngleBracket]y, y\&_\[RightAngleBracket]\ \[DoubleLeftRightArrow] \ \[LeftAngleBracket]x\&_\[RightAngleBracket] \[Succeeds] \ \[LeftAngleBracket]y\&_\[RightAngleBracket])\)\)} }, ColumnAlignments->{Left}]], "Input", InitializationCell->True, CellTags->"Definition (is longer than)"], Cell[BoxData[ \(\[ForAll] \+\(x, y\&_\)\((x\[Cup]\[LeftAngleBracket]y\&_\ \[RightAngleBracket] = \[LeftAngleBracket]x, y\&_\[RightAngleBracket])\)\)], "Input"], Cell[BoxData[ \(\[ForAll] \+\(x, y\&_\)\((\[LeftAngleBracket]y\&_\[RightAngleBracket]\ \[Cap]x = \[LeftAngleBracket]y\&_, x\[RightAngleBracket])\)\)], "Input"], Cell[BoxData[ \(\(\(\[ForAll] \+\(x\&_, y\&_\)\((\(\(<\)\(x\&_\)\(>\)\(\[CupCap]\)\(<\)\ \(\(\(y\)\(\ \)\)\&_\)\(>=\)\(<\)\(x\&_\)\), \(\(\(\(y\)\(\ \)\)\&_\)\(>\)\)\ \ )\)\)\(\[IndentingNewLine]\) \)\)], "Input"], Cell[BoxData[{\(\[ForAll] \+X\((is\[Dash]tuple[ X]\ \[DoubleLeftRightArrow] \ \(\[Exists] \+\(x\&_\)\((X = \ \[LeftAngleBracket]x\&_\[RightAngleBracket])\)\))\)\), "\[IndentingNewLine]", GridBox[{ {\(\[ForAll] \+X\((is\[Dash]empty\[Dash]tuple[ X]\ \[DoubleLeftRightArrow] \((X = \[LeftAngleBracket]\ \[RightAngleBracket])\))\)\)}, {\(\[ForAll] \+X\((is\[Dash]singleton\[Dash]tuple[ X]\ \[DoubleLeftRightArrow] \(\[Exists] \+x\((X = \ \[LeftAngleBracket]x\[RightAngleBracket])\)\))\)\)}, {\(\[ForAll] \+X\((is\[Dash]trivial\[Dash]tuple[ X] \[DoubleLeftRightArrow] \((is\[Dash]empty\[Dash]tuple[ X] \[Or] is\[Dash]singleton\[Dash]tuple[X])\))\)\)} }, ColumnAlignments->{Left}]}], "Input"] }, Open ]], Cell[CellGroupData[{ Cell["Axioms", "Subsubsection"], Cell[BoxData[GridBox[{ {\(\[ForAll] \+\(x, x\&_, y, y\&_\)\((\[LeftAngleBracket]x, x\&_\[RightAngleBracket]\ = \[LeftAngleBracket]y, y\&_\[RightAngleBracket])\) \[DoubleLeftRightArrow] \ \((\((x = y)\) \[And] \((\[LeftAngleBracket]x\&_\ \[RightAngleBracket] = \[LeftAngleBracket]y\&_\[RightAngleBracket])\))\)\)}, {\(\[ForAll] \+\(x, x\&_\)\((\[LeftAngleBracket]x, x\&_\[RightAngleBracket] \[NotEqual] \[LeftAngleBracket]\ \[RightAngleBracket])\)\)} }, ColumnAlignments->{Left}]], "Input"] }, Open ]], Cell[CellGroupData[{ Cell["Properties", "Subsubsection"], Cell[BoxData[ \(\[ForAll] \+\(is\[Dash]trivial\[Dash]tuple[X]\)is\[Dash]sorted[ X]\)], "Input"], Cell[BoxData[ \(\[ForAll] \+\(is\[Dash]trivial\[Dash]tuple[X], \ \ is\[Dash]tuple[Y]\)\((X \[TildeTilde] Y \[DoubleLeftRightArrow] \((X = Y)\))\)\)], "Input"], Cell[BoxData[GridBox[{ {\(\[ForAll] \+\(is\[Dash]tuple[X]\)\((X \[TildeTilde] X)\)\)}, {\(\[ForAll] \+\(is\[Dash]tuple[X, Y]\)\((X \[TildeTilde] Y \[Implies] Y \[TildeTilde] X)\)\)}, {\(\(\[ForAll] \+\(is\[Dash]tuple[X, Y, Z]\)\((\((X \[TildeTilde] Y \[And] Y \[TildeTilde] Z)\) \[Implies] X \[TildeTilde] Z)\)\)\(\[IndentingNewLine]\) \)}, {\(\[ForAll] \+\(is\[Dash]tuple[A, B, Y, Z]\)\((\((A \[TildeTilde] Y \[And] B \[TildeTilde] Z)\) \[Implies] \((A \[CupCap] B)\) \[TildeTilde] \((Y \[CupCap] Z)\))\)\)} }, ColumnAlignments->{Left}]], "Input"], Cell[BoxData[GridBox[{ {\(\[ForAll] \+\(is\[Dash]tuple[X, Y]\)\((X \[Succeeds] Y \[Implies] \((Y \[NotSucceeds] X)\))\)\)}, {\(\[ForAll] \+\(is\[Dash]tuple[X, Y, Z]\)\((\((X \[Succeeds] Y \[And] Y \[Succeeds] Z)\) \[Implies] X \[Succeeds] Z)\)\)} }, ColumnAlignments->{Left}]], "Input"] }, Open ]] }, Open ]] }, Open ]] }, FrontEndVersion->"4.2 for Microsoft Windows", ScreenRectangle->{{0, 1024}, {0, 685}}, AutoGeneratedPackage->None, WindowToolbars->{"RulerBar", "EditBar"}, WindowSize->{1016, 651}, WindowMargins->{{0, Automatic}, {Automatic, 0}}, PrintingCopies->1, PrintingPageRange->{Automatic, Automatic}, PageHeaders->{{Inherited, Inherited, Inherited}, {None, Inherited, None}}, PageFooters->{{Inherited, Inherited, Inherited}, {Inherited, Cell[ TextData[ { CounterBox[ "Page"]}], "PageNumber"], Inherited}}, PageHeaderLines->{Inherited, False}, PrintingOptions->{"FirstPageFooter"->False}, Magnification->1.5, StyleDefinitions -> Notebook[{ Cell[CellGroupData[{ Cell["Style Definitions", "Subtitle"], Cell["\<\ Modify the definitions below to change the default appearance of all cells in \ a given style. Make modifications to any definition using commands in the \ Format menu.\ \>", "Text"], Cell[CellGroupData[{ Cell["Style Environment Names", "Section"], Cell[StyleData[All, "Working"], PageWidth->WindowWidth, ScriptMinSize->9], Cell[StyleData[All, "Presentation"], PageWidth->WindowWidth, ScriptMinSize->12, FontSize->16], Cell[StyleData[All, "Condensed"], PageWidth->WindowWidth, CellBracketOptions->{"Margins"->{1, 1}, "Widths"->{0, 5}}, ScriptMinSize->8, FontSize->11], Cell[StyleData[All, "Printout"], PageWidth->PaperWidth, ScriptMinSize->5, FontSize->10, PrivateFontOptions->{"FontType"->"Outline"}] }, Closed]], Cell[CellGroupData[{ Cell["Notebook Options", "Section"], Cell["\<\ The options defined for the style below will be used at the Notebook level.\ \>", "Text"], Cell[StyleData["Notebook"], PageHeaders->{{Cell[ TextData[ { CounterBox[ "Page"]}], "PageNumber"], None, Cell[ TextData[ { ValueBox[ "FileName"]}], "Header"]}, {Cell[ TextData[ { ValueBox[ "FileName"]}], "Header"], None, Cell[ TextData[ { CounterBox[ "Page"]}], "PageNumber"]}}, CellFrameLabelMargins->6, AutoItalicWords->{"Theorema"}, LimitsPositioningTokens->{}, StyleMenuListing->None] }, Closed]], Cell[CellGroupData[{ Cell["Styles for Headings", "Section"], Cell[CellGroupData[{ Cell[StyleData["Title"], CellMargins->{{12, Inherited}, {20, 40}}, CellGroupingRules->{"TitleGrouping", 0}, PageBreakBelow->False, CounterIncrements->"Title", CounterAssignments->{{"Section", 0}, {"Equation", 0}, {"Figure", 0}, { "Subtitle", 0}, {"Subsubtitle", 0}}, FontFamily->"Arial", FontSize->36, FontWeight->"Bold", FontColor->GrayLevel[0], Background->None], Cell[StyleData["Title", "Presentation"], CellMargins->{{24, 10}, {20, 40}}, LineSpacing->{1, 0}, FontSize->44], Cell[StyleData["Title", "Condensed"], CellMargins->{{8, 10}, {4, 8}}, FontSize->20], Cell[StyleData["Title", "Printout"], CellMargins->{{2, 10}, {12, 30}}, FontSize->24] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Subtitle"], CellMargins->{{12, Inherited}, {20, 15}}, CellGroupingRules->{"TitleGrouping", 10}, PageBreakBelow->False, CounterIncrements->"Subtitle", CounterAssignments->{{"Section", 0}, {"Equation", 0}, {"Figure", 0}, { "Subsubtitle", 0}}, FontFamily->"Arial", FontSize->24, FontColor->GrayLevel[0], Background->None], Cell[StyleData["Subtitle", "Presentation"], CellMargins->{{24, 10}, {20, 20}}, LineSpacing->{1, 0}, FontSize->36], Cell[StyleData["Subtitle", "Condensed"], CellMargins->{{8, 10}, {4, 4}}, FontSize->14], Cell[StyleData["Subtitle", "Printout"], CellMargins->{{2, 10}, {12, 8}}, FontSize->18] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Subsubtitle"], CellMargins->{{12, Inherited}, {20, 15}}, CellGroupingRules->{"TitleGrouping", 20}, PageBreakBelow->False, CounterIncrements->"Subsubtitle", CounterAssignments->{{"Section", 0}, {"Equation", 0}, {"Figure", 0}}, FontFamily->"Arial", FontSize->14, FontSlant->"Italic", FontColor->GrayLevel[0], Background->None], Cell[StyleData["Subsubtitle", "Presentation"], CellMargins->{{24, 10}, {20, 20}}, LineSpacing->{1, 0}, FontSize->24], Cell[StyleData["Subsubtitle", "Condensed"], CellMargins->{{8, 10}, {8, 8}}, FontSize->12], Cell[StyleData["Subsubtitle", "Printout"], CellMargins->{{2, 10}, {12, 8}}, FontSize->14] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Section"], CellDingbat->"\[FilledSquare]", CellMargins->{{25, Inherited}, {8, 24}}, CellGroupingRules->{"SectionGrouping", 30}, PageBreakBelow->False, CounterIncrements->"Section", CounterAssignments->{{"Subsection", 0}, {"Subsubsection", 0}}, FontFamily->"Arial", FontSize->16, FontWeight->"Bold", FontColor->GrayLevel[0], Background->None], Cell[StyleData["Section", "Presentation"], CellMargins->{{40, 10}, {11, 32}}, LineSpacing->{1, 0}, FontSize->24], Cell[StyleData["Section", "Condensed"], CellMargins->{{18, Inherited}, {6, 12}}, FontSize->12], Cell[StyleData["Section", "Printout"], CellMargins->{{13, 0}, {7, 22}}, FontSize->14] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Subsection"], CellDingbat->"\[FilledSmallSquare]", CellMargins->{{22, Inherited}, {8, 20}}, CellGroupingRules->{"SectionGrouping", 40}, PageBreakBelow->False, CounterIncrements->"Subsection", CounterAssignments->{{"Subsubsection", 0}}, FontFamily->"Arial", FontSize->14, FontWeight->"Bold", FontColor->GrayLevel[0], Background->None], Cell[StyleData["Subsection", "Presentation"], CellMargins->{{36, 10}, {11, 32}}, LineSpacing->{1, 0}, FontSize->22], Cell[StyleData["Subsection", "Condensed"], CellMargins->{{16, Inherited}, {6, 12}}, FontSize->12], Cell[StyleData["Subsection", "Printout"], CellMargins->{{9, 0}, {7, 22}}, FontSize->12] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Subsubsection"], CellDingbat->"\[FilledSmallSquare]", CellMargins->{{22, Inherited}, {8, 18}}, CellGroupingRules->{"SectionGrouping", 50}, PageBreakBelow->False, CounterIncrements->"Subsubsection", FontFamily->"Arial", FontWeight->"Bold", FontColor->GrayLevel[0], Background->None], Cell[StyleData["Subsubsection", "Presentation"], CellMargins->{{34, 10}, {11, 26}}, LineSpacing->{1, 0}, FontSize->18], Cell[StyleData["Subsubsection", "Condensed"], CellMargins->{{17, Inherited}, {6, 12}}, FontSize->10], Cell[StyleData["Subsubsection", "Printout"], CellMargins->{{9, 0}, {7, 14}}, FontSize->11] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Subsubsubsection"], CellDingbat->"\[EmptySmallSquare]", CellMargins->{{22, Inherited}, {8, 18}}, CellGroupingRules->{"SectionGrouping", 60}, PageBreakBelow->False, CounterIncrements->"Subsubsubsection", FontFamily->"Arial", FontWeight->"Bold", FontColor->GrayLevel[0], Background->None], Cell[StyleData["Subsubsection", "Presentation"], CellMargins->{{34, 10}, {11, 26}}, LineSpacing->{1, 0}, FontSize->18], Cell[StyleData["Subsubsection", "Condensed"], CellMargins->{{17, Inherited}, {6, 12}}, FontSize->10], Cell[StyleData["Subsubsection", "Printout"], CellMargins->{{9, 0}, {7, 14}}, FontSize->11] }, Open ]] }, Closed]], Cell[CellGroupData[{ Cell["Styles for Body Text", "Section", FontFamily->"Arial"], Cell[CellGroupData[{ Cell[StyleData["Text"], CellMargins->{{12, 10}, {7, 7}}, TextJustification->1, LineSpacing->{1, 3}, CounterIncrements->"Text", FontFamily->"Arial", FontColor->GrayLevel[0], Background->None], Cell[StyleData["Text", "Presentation"], CellMargins->{{24, 10}, {10, 10}}, LineSpacing->{1, 5}], Cell[StyleData["Text", "Condensed"], CellMargins->{{8, 10}, {6, 6}}, LineSpacing->{1, 1}], Cell[StyleData["Text", "Printout"], CellMargins->{{2, 2}, {6, 6}}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["SmallText"], CellMargins->{{12, 10}, {6, 6}}, LineSpacing->{1, 3}, CounterIncrements->"SmallText", FontFamily->"Arial", FontSize->9, FontColor->GrayLevel[0], Background->None], Cell[StyleData["SmallText", "Presentation"], CellMargins->{{24, 10}, {8, 8}}, LineSpacing->{1, 5}, FontSize->12], Cell[StyleData["SmallText", "Condensed"], CellMargins->{{8, 10}, {5, 5}}, LineSpacing->{1, 2}, FontSize->9], Cell[StyleData["SmallText", "Printout"], CellMargins->{{2, 2}, {5, 5}}, FontSize->7] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Styles for Input/Output", "Section"], Cell["\<\ The cells in this section define styles used for input and output to the \ kernel. Be careful when modifying, renaming, or removing these styles, \ because the front end associates special meanings with these style names. \ Some attributes for these styles are actually set in FormatType Styles (in \ the last section of this stylesheet). \ \>", "Text"], Cell[CellGroupData[{ Cell[StyleData["Input"], CellMargins->{{45, 10}, {5, 7}}, Evaluatable->True, CellGroupingRules->"InputGrouping", PageBreakWithin->False, GroupPageBreakWithin->False, CellLabelMargins->{{11, Inherited}, {Inherited, Inherited}}, DefaultFormatType->DefaultInputFormatType, AutoItalicWords->{}, FormatType->InputForm, ShowStringCharacters->True, NumberMarks->True, CounterIncrements->"Input", FontFamily->"Times", FontWeight->"Plain", FontSlant->"Plain", FontTracking->"Plain", FontColor->GrayLevel[0], Background->None, FontVariations->{"Underline"->False, "Outline"->False, "Shadow"->False}], Cell[StyleData["Input", "Presentation"], CellMargins->{{72, Inherited}, {8, 10}}, LineSpacing->{1, 0}], Cell[StyleData["Input", "Condensed"], CellMargins->{{40, 10}, {2, 3}}], Cell[StyleData["Input", "Printout"], CellMargins->{{39, 0}, {4, 6}}, FontSize->9] }, Open ]], Cell[StyleData["InputOnly"], Evaluatable->True, CellGroupingRules->"InputGrouping", DefaultFormatType->DefaultInputFormatType, AutoItalicWords->{}, FormatType->InputForm, ShowStringCharacters->True, NumberMarks->True, CounterIncrements->"Input", StyleMenuListing->None, FontWeight->"Bold", FontColor->GrayLevel[0], Background->None], Cell[CellGroupData[{ Cell[StyleData["Output"], CellMargins->{{47, 10}, {7, 5}}, CellEditDuplicate->True, CellGroupingRules->"OutputGrouping", CellHorizontalScrolling->True, PageBreakWithin->False, GroupPageBreakWithin->False, GeneratedCell->True, CellAutoOverwrite->True, CellLabelMargins->{{11, Inherited}, {Inherited, Inherited}}, DefaultFormatType->DefaultOutputFormatType, AutoItalicWords->{}, FormatType->InputForm, CounterIncrements->"Output", FontColor->GrayLevel[0], Background->None], Cell[StyleData["Output", "Presentation"], CellMargins->{{72, Inherited}, {10, 8}}, LineSpacing->{1, 0}], Cell[StyleData["Output", "Condensed"], CellMargins->{{41, Inherited}, {3, 2}}], Cell[StyleData["Output", "Printout"], CellMargins->{{39, 0}, {6, 4}}, FontSize->9] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Message"], CellMargins->{{45, Inherited}, {Inherited, Inherited}}, CellGroupingRules->"OutputGrouping", PageBreakWithin->False, GroupPageBreakWithin->False, GeneratedCell->True, CellAutoOverwrite->True, ShowCellLabel->False, CellLabelMargins->{{11, Inherited}, {Inherited, Inherited}}, DefaultFormatType->DefaultOutputFormatType, AutoItalicWords->{}, FormatType->InputForm, CounterIncrements->"Message", StyleMenuListing->None, FontColor->GrayLevel[0], Background->None], Cell[StyleData["Message", "Presentation"], CellMargins->{{72, Inherited}, {Inherited, Inherited}}, LineSpacing->{1, 0}], Cell[StyleData["Message", "Condensed"], CellMargins->{{41, Inherited}, {Inherited, Inherited}}], Cell[StyleData["Message", "Printout"], CellMargins->{{39, Inherited}, {Inherited, Inherited}}, FontSize->8] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Print"], CellMargins->{{45, Inherited}, {Inherited, Inherited}}, CellGroupingRules->"OutputGrouping", PageBreakWithin->False, GroupPageBreakWithin->False, GeneratedCell->True, CellAutoOverwrite->True, ShowCellLabel->False, CellLabelMargins->{{11, Inherited}, {Inherited, Inherited}}, DefaultFormatType->DefaultOutputFormatType, AutoItalicWords->{}, FormatType->InputForm, CounterIncrements->"Print", StyleMenuListing->None, FontColor->GrayLevel[0], Background->None], Cell[StyleData["Print", "Presentation"], CellMargins->{{72, Inherited}, {Inherited, Inherited}}, LineSpacing->{1, 0}], Cell[StyleData["Print", "Condensed"], CellMargins->{{41, Inherited}, {Inherited, Inherited}}], Cell[StyleData["Print", "Printout"], CellMargins->{{39, Inherited}, {Inherited, Inherited}}, FontSize->8] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Graphics"], CellMargins->{{4, Inherited}, {Inherited, Inherited}}, CellGroupingRules->"GraphicsGrouping", CellHorizontalScrolling->True, PageBreakWithin->False, GeneratedCell->True, CellAutoOverwrite->True, ShowCellLabel->False, DefaultFormatType->DefaultOutputFormatType, FormatType->InputForm, CounterIncrements->"Graphics", ImageMargins->{{43, Inherited}, {Inherited, 0}}, StyleMenuListing->None, FontColor->GrayLevel[0], Background->None], Cell[StyleData["Graphics", "Presentation"], ImageMargins->{{62, Inherited}, {Inherited, 0}}], Cell[StyleData["Graphics", "Condensed"], ImageMargins->{{38, Inherited}, {Inherited, 0}}, Magnification->0.6], Cell[StyleData["Graphics", "Printout"], ImageMargins->{{30, Inherited}, {Inherited, 0}}, FontSize->9, Magnification->0.8] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["CellLabel"], StyleMenuListing->None, FontFamily->"Helvetica", FontSize->9, FontColor->GrayLevel[0], Background->None], Cell[StyleData["CellLabel", "Presentation"], FontSize->12], Cell[StyleData["CellLabel", "Condensed"], FontSize->9], Cell[StyleData["CellLabel", "Printout"], FontFamily->"Courier", FontSize->8, FontSlant->"Italic"] }, Closed]] }, Open ]], Cell[CellGroupData[{ Cell["Styles for Proof Cells", "Section"], Cell[CellGroupData[{ Cell[StyleData["ProofText"], CellMargins->{{12, 10}, {7, 7}}, LineSpacing->{1, 3}, ParagraphIndent->0, CounterIncrements->"Text", FontColor->GrayLevel[0]], Cell[StyleData["ProofText", "Presentation"], CellMargins->{{24, 10}, {10, 10}}, LineSpacing->{1, 5}], Cell[StyleData["ProofText", "Condensed"], CellMargins->{{8, 10}, {6, 6}}, LineSpacing->{1, 1}], Cell[StyleData["ProofText", "Printout"], CellMargins->{{2, 2}, {6, 6}}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Label"], CellMargins->{{20, 30}, {7, 7}}, LineSpacing->{1, 3}, FontColor->RGBColor[0, 0, 1]], Cell[StyleData["Label", "Presentation"], CellMargins->{{24, 10}, {10, 10}}, LineSpacing->{1, 5}], Cell[StyleData["Label", "Condensed"], CellMargins->{{8, 10}, {6, 6}}, LineSpacing->{1, 1}], Cell[StyleData["Label", "Printout"], CellMargins->{{2, 2}, {6, 6}}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Conclusion"], CellMargins->{{12, 10}, {7, 7}}, LineSpacing->{1, 3}, FontColor->RGBColor[1, 0, 0]], Cell[StyleData["Conclusion", "Presentation"], CellMargins->{{24, 10}, {10, 10}}, LineSpacing->{1, 5}], Cell[StyleData["Conclusion", "Condensed"], CellMargins->{{8, 10}, {6, 6}}, LineSpacing->{1, 1}], Cell[StyleData["Conclusion", "Printout"], CellMargins->{{2, 2}, {6, 6}}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Assumption"], CellMargins->{{12, 10}, {7, 7}}, LineSpacing->{1, 3}, FontColor->RGBColor[0.270588, 0.545098, 0.454902]], Cell[StyleData["Assumption", "Presentation"], CellMargins->{{24, 10}, {10, 10}}, LineSpacing->{1, 5}], Cell[StyleData["Assumption", "Condensed"], CellMargins->{{8, 10}, {6, 6}}, LineSpacing->{1, 1}], Cell[StyleData["Assumption", "Printout"], CellMargins->{{2, 2}, {6, 6}}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Expression"], CellMargins->{{12, 10}, {7, 7}}, LineSpacing->{1, 3}], Cell[StyleData["Expression", "Presentation"], CellMargins->{{24, 10}, {10, 10}}, LineSpacing->{1, 5}], Cell[StyleData["Expression", "Condensed"], CellMargins->{{8, 10}, {6, 6}}, LineSpacing->{1, 1}], Cell[StyleData["Expression", "Printout"], CellMargins->{{2, 2}, {6, 6}}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Indent"], CellSize->{25, Inherited}], Cell[StyleData["Indent", "Presentation"], CellSize->{30, Inherited}], Cell[StyleData["Indent", "Condensed"], CellSize->{15, Inherited}], Cell[StyleData["Indent", "Printout"], CellSize->{15, Inherited}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Blank"], CellSize->{15, Inherited}], Cell[StyleData["Blank", "Presentation"], CellSize->{20, Inherited}], Cell[StyleData["Blank", "Condensed"], CellSize->{10, Inherited}], Cell[StyleData["Blank", "Printout"], CellSize->{10, Inherited}] }, Closed]] }, Open ]], Cell[CellGroupData[{ Cell["Formulas and Programming", "Section"], Cell[CellGroupData[{ Cell[StyleData["InlineFormula"], CellMargins->{{10, 4}, {0, 8}}, CellHorizontalScrolling->True, ScriptLevel->1, SingleLetterItalics->True], Cell[StyleData["InlineFormula", "Presentation"], CellMargins->{{24, 10}, {10, 10}}, LineSpacing->{1, 5}], Cell[StyleData["InlineFormula", "Condensed"], CellMargins->{{8, 10}, {6, 6}}, LineSpacing->{1, 1}], Cell[StyleData["InlineFormula", "Printout"], CellMargins->{{2, 0}, {6, 6}}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["DisplayFormula"], CellMargins->{{42, Inherited}, {Inherited, Inherited}}, CellHorizontalScrolling->True, DefaultFormatType->DefaultInputFormatType, ScriptLevel->0, SingleLetterItalics->True, UnderoverscriptBoxOptions->{LimitsPositioning->True}], Cell[StyleData["DisplayFormula", "Presentation"], LineSpacing->{1, 5}], Cell[StyleData["DisplayFormula", "Condensed"], LineSpacing->{1, 1}], Cell[StyleData["DisplayFormula", "Printout"]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Styles for Headers and Footers", "Section"], Cell[StyleData["Header"], CellMargins->{{0, 0}, {4, 1}}, StyleMenuListing->None, FontSize->10, FontSlant->"Italic"], Cell[StyleData["Footer"], CellMargins->{{0, 0}, {0, 4}}, StyleMenuListing->None, FontSize->9, FontSlant->"Italic"], Cell[StyleData["PageNumber"], CellMargins->{{0, 0}, {4, 1}}, StyleMenuListing->None, FontFamily->"Times", FontSize->10] }, Closed]], Cell[CellGroupData[{ Cell["Palette Styles", "Section"], Cell["\<\ The cells below define styles that define standard ButtonFunctions, for use \ in palette buttons.\ \>", "Text"], Cell[StyleData["Paste"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`NotebookApply[ FrontEnd`InputNotebook[ ], #, After]}]&)}], Cell[StyleData["Evaluate"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`NotebookApply[ FrontEnd`InputNotebook[ ], #, All], SelectionEvaluate[ FrontEnd`InputNotebook[ ], All]}]&)}], Cell[StyleData["EvaluateCell"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`NotebookApply[ FrontEnd`InputNotebook[ ], #, All], FrontEnd`SelectionMove[ FrontEnd`InputNotebook[ ], All, Cell, 1], FrontEnd`SelectionEvaluateCreateCell[ FrontEnd`InputNotebook[ ], All]}]&)}], Cell[StyleData["CopyEvaluate"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`SelectionCreateCell[ FrontEnd`InputNotebook[ ], All], FrontEnd`NotebookApply[ FrontEnd`InputNotebook[ ], #, All], FrontEnd`SelectionEvaluate[ FrontEnd`InputNotebook[ ], All]}]&)}], Cell[StyleData["CopyEvaluateCell"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`SelectionCreateCell[ FrontEnd`InputNotebook[ ], All], FrontEnd`NotebookApply[ FrontEnd`InputNotebook[ ], #, All], FrontEnd`SelectionEvaluateCreateCell[ FrontEnd`InputNotebook[ ], All]}]&)}] }, Closed]], Cell[CellGroupData[{ Cell["Hyperlink Styles", "Section"], Cell["\<\ The cells below define styles useful for making hypertext ButtonBoxes. The \ \"Hyperlink\" style is for links within the same Notebook, or between \ Notebooks.\ \>", "Text"], Cell[CellGroupData[{ Cell[StyleData["Hyperlink"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontColor->RGBColor[0, 0, 1], FontVariations->{"Underline"->True}, ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`NotebookLocate[ #2]}]&), Active->True, ButtonNote->ButtonData}], Cell[StyleData["Hyperlink", "Presentation"]], Cell[StyleData["Hyperlink", "Condensed"]], Cell[StyleData["Hyperlink", "Printout"], FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]], Cell["\<\ The following styles are for linking automatically to the on-line help \ system.\ \>", "Text"], Cell[CellGroupData[{ Cell[StyleData["MainBookLink"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontColor->RGBColor[0, 0, 1], FontVariations->{"Underline"->True}, ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`HelpBrowserLookup[ "MainBook", #]}]&), Active->True, ButtonFrame->"None"}], Cell[StyleData["MainBookLink", "Presentation"]], Cell[StyleData["MainBookLink", "Condensed"]], Cell[StyleData["MainBookLink", "Printout"], FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["AddOnsLink"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontFamily->"Courier", FontColor->RGBColor[0, 0, 1], FontVariations->{"Underline"->True}, ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`HelpBrowserLookup[ "AddOns", #]}]&), Active->True, ButtonFrame->"None"}], Cell[StyleData["AddOnsLink", "Presentation"]], Cell[StyleData["AddOnsLink", "Condensed"]], Cell[StyleData["AddOnLink", "Printout"], FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["RefGuideLink"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontFamily->"Courier", FontColor->RGBColor[0, 0, 1], FontVariations->{"Underline"->True}, ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`HelpBrowserLookup[ "RefGuideLink", #]}]&), Active->True, ButtonFrame->"None"}], Cell[StyleData["RefGuideLink", "Presentation"]], Cell[StyleData["RefGuideLink", "Condensed"]], Cell[StyleData["RefGuideLink", "Printout"], FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["GettingStartedLink"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontColor->RGBColor[0, 0, 1], FontVariations->{"Underline"->True}, ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`HelpBrowserLookup[ "GettingStarted", #]}]&), Active->True, ButtonFrame->"None"}], Cell[StyleData["GettingStartedLink", "Presentation"]], Cell[StyleData["GettingStartedLink", "Condensed"]], Cell[StyleData["GettingStartedLink", "Printout"], FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["OtherInformationLink"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontColor->RGBColor[0, 0, 1], FontVariations->{"Underline"->True}, ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`HelpBrowserLookup[ "OtherInformation", #]}]&), Active->True, ButtonFrame->"None"}], Cell[StyleData["OtherInformationLink", "Presentation"]], Cell[StyleData["OtherInformationLink", "Condensed"]], Cell[StyleData["OtherInformationLink", "Printout"], FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Placeholder Styles", "Section"], Cell["\<\ The cells below define styles useful for making placeholder objects in \ palette templates.\ \>", "Text"], Cell[CellGroupData[{ Cell[StyleData["Placeholder"], Editable->False, Selectable->False, StyleBoxAutoDelete->True, Placeholder->True, StyleMenuListing->None], Cell[StyleData["Placeholder", "Presentation"]], Cell[StyleData["Placeholder", "Condensed"]], Cell[StyleData["Placeholder", "Printout"]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["SelectionPlaceholder"], Editable->False, Selectable->False, StyleBoxAutoDelete->True, Placeholder->PrimaryPlaceholder, StyleMenuListing->None, DrawHighlighted->True], Cell[StyleData["SelectionPlaceholder", "Presentation"]], Cell[StyleData["SelectionPlaceholder", "Condensed"]], Cell[StyleData["SelectionPlaceholder", "Printout"]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["FormatType Styles", "Section"], Cell["\<\ The cells below define styles that are mixed in with the styles of most \ cells. If a cell's FormatType matches the name of one of the styles defined \ below, then that style is applied between the cell's style and its own \ options. This is particularly true of Input and Output.\ \>", "Text"], Cell[StyleData["CellExpression"], PageWidth->Infinity, CellMargins->{{6, Inherited}, {Inherited, Inherited}}, ShowCellLabel->False, ShowSpecialCharacters->False, AllowInlineCells->False, AutoItalicWords->{}, StyleMenuListing->None, FontFamily->"Courier", FontSize->12, Background->GrayLevel[1]], Cell[StyleData["InputForm"], AllowInlineCells->False, StyleMenuListing->None, FontFamily->"Courier"], Cell[StyleData["OutputForm"], PageWidth->Infinity, TextAlignment->Left, LineSpacing->{0.6, 1}, StyleMenuListing->None, FontFamily->"Courier"], Cell[StyleData["StandardForm"], LineSpacing->{1.25, 0}, StyleMenuListing->None], Cell[StyleData["TraditionalForm"], LineSpacing->{1.25, 0}, SingleLetterItalics->True, TraditionalFunctionNotation->True, DelimiterMatching->None, StyleMenuListing->None], Cell["\<\ The style defined below is mixed in to any cell that is in an inline cell \ within another.\ \>", "Text"], Cell[StyleData["InlineCell"], TextAlignment->Left, ScriptLevel->1, StyleMenuListing->None], Cell[StyleData["InlineCellEditing"], StyleMenuListing->None, Background->RGBColor[1, 0.749996, 0.8]] }, Closed]] }, Open ]] }] ] (******************************************************************* Cached data follows. If you edit this Notebook file directly, not using Mathematica, you must remove the line containing CacheID at the top of the file. The cache data will then be recreated when you save this file from within Mathematica. *******************************************************************) (*CellTagsOutline CellTagsIndex->{ "Definition (is longer than)"->{ Cell[66242, 1738, 791, 16, 132, "Input", InitializationCell->True, CellTags->"Definition (is longer than)"]} } *) (*CellTagsIndex CellTagsIndex->{ {"Definition (is longer than)", 99709, 2906} } *) (*NotebookFileOutline Notebook[{ Cell[CellGroupData[{ Cell[1776, 53, 217, 8, 180, "Title"], Cell[1996, 63, 219, 8, 156, "Subtitle"], Cell[CellGroupData[{ Cell[2240, 75, 30, 0, 68, "Subsection"], Cell[2273, 77, 181, 4, 75, "Text"], Cell[2457, 83, 251, 5, 75, "Text"], Cell[2711, 90, 220, 4, 75, "Text"], Cell[2934, 96, 201, 4, 48, "Text"], Cell[3138, 102, 444, 7, 129, "Text"], Cell[3585, 111, 375, 11, 75, "Text"], Cell[3963, 124, 967, 17, 210, "Text"], Cell[4933, 143, 297, 6, 75, "Text"], Cell[5233, 151, 612, 13, 156, "Text"], Cell[5848, 166, 591, 14, 130, "Text"], Cell[6442, 182, 364, 9, 76, "Text"] }, Open ]], Cell[CellGroupData[{ Cell[6843, 196, 31, 0, 79, "Section"], Cell[6877, 198, 422, 11, 102, "Text"], Cell[7302, 211, 709, 12, 183, "Text"], Cell[8014, 225, 63, 0, 48, "Text"], Cell[8080, 227, 152, 2, 48, "Text"], Cell[8235, 231, 131, 2, 48, "Text"], Cell[8369, 235, 147, 2, 48, "Text"], Cell[8519, 239, 449, 10, 129, "Text"], Cell[8971, 251, 850, 12, 210, "Text"], Cell[9824, 265, 830, 12, 210, "Text"], Cell[10657, 279, 320, 7, 102, "Text"], Cell[10980, 288, 120, 2, 55, "Input"], Cell[11103, 292, 161, 4, 48, "Text"], Cell[11267, 298, 139, 3, 41, "Input"], Cell[11409, 303, 26, 0, 48, "Text"], Cell[11438, 305, 3195, 64, 536, "Input"], Cell[14636, 371, 176, 4, 75, "Text"], Cell[14815, 377, 348, 6, 102, "Text"], Cell[15166, 385, 291, 6, 75, "Text"], Cell[15460, 393, 446, 8, 102, "Text"], Cell[15909, 403, 325, 6, 75, "Text"], Cell[16237, 411, 563, 11, 129, "Text"], Cell[16803, 424, 443, 8, 130, "Text"] }, Open ]], Cell[CellGroupData[{ Cell[17283, 437, 95, 2, 79, "Section"], Cell[17381, 441, 383, 6, 102, "Text"], Cell[17767, 449, 549, 13, 114, "Input"], Cell[18319, 464, 114, 2, 55, "Input"], Cell[18436, 468, 1017, 25, 114, "Input"], Cell[19456, 495, 46, 0, 48, "Text"], Cell[19505, 497, 1052, 20, 216, "Input"], Cell[20560, 519, 1619, 32, 170, "Input"], Cell[22182, 553, 430, 7, 129, "Text"], Cell[22615, 562, 149, 3, 48, "Text"], Cell[22767, 567, 138, 2, 41, "Input"], Cell[22908, 571, 107, 3, 48, "Text"], Cell[23018, 576, 355, 6, 102, "Text"], Cell[23376, 584, 539, 13, 114, "Input"], Cell[23918, 599, 106, 2, 55, "Input"], Cell[24027, 603, 673, 16, 114, "Input"], Cell[24703, 621, 782, 19, 114, "Input"], Cell[25488, 642, 16, 0, 48, "Text"] }, Open ]], Cell[CellGroupData[{ Cell[25541, 647, 101, 2, 79, "Section"], Cell[25645, 651, 443, 7, 129, "Text"], Cell[26091, 660, 173, 3, 75, "Text"], Cell[26267, 665, 920, 16, 216, "Input"], Cell[27190, 683, 1587, 31, 170, "Input"], Cell[28780, 716, 48, 0, 48, "Text"], Cell[28831, 718, 117, 2, 41, "Input"], Cell[28951, 722, 632, 15, 130, "Text"] }, Open ]], Cell[CellGroupData[{ Cell[29620, 742, 121, 3, 110, "Section"], Cell[CellGroupData[{ Cell[29766, 749, 36, 0, 62, "Subsubsection"], Cell[29805, 751, 795, 12, 210, "Text"], Cell[30603, 765, 216, 4, 75, "Text"], Cell[30822, 771, 156, 3, 75, "Text"], Cell[30981, 776, 920, 16, 216, "Input"], Cell[31904, 794, 1645, 32, 170, "Input"], Cell[33552, 828, 345, 6, 102, "Text"], Cell[33900, 836, 923, 22, 280, "Input"], Cell[34826, 860, 1633, 36, 203, "Input"], Cell[36462, 898, 64, 2, 48, "Text"], Cell[36529, 902, 49, 0, 48, "Text"], Cell[36581, 904, 117, 2, 41, "Input"], Cell[36701, 908, 46, 0, 48, "Text"] }, Open ]], Cell[CellGroupData[{ Cell[36784, 913, 34, 0, 62, "Subsubsection"], Cell[36821, 915, 25, 0, 48, "Text"], Cell[36849, 917, 80, 1, 41, "Input"], Cell[36932, 920, 19, 0, 48, "Text"], Cell[36954, 922, 66, 1, 41, "Input"], Cell[37023, 925, 36, 0, 48, "Text"], Cell[37062, 927, 121, 2, 41, "Input"], Cell[37186, 931, 54, 0, 48, "Text"], Cell[37243, 933, 228, 6, 114, "Input"], Cell[37474, 941, 19, 0, 48, "Text"], Cell[37496, 943, 215, 6, 114, "Input"], Cell[37714, 951, 32, 0, 48, "Text"], Cell[37749, 953, 342, 9, 188, "Input"], Cell[38094, 964, 335, 6, 102, "Text"], Cell[38432, 972, 40, 0, 48, "Text"], Cell[38475, 974, 266, 5, 56, "Input"], Cell[38744, 981, 120, 3, 48, "Text"], Cell[38867, 986, 69, 1, 41, "Input"], Cell[38939, 989, 111, 3, 48, "Text"], Cell[39053, 994, 103, 3, 48, "Text"], Cell[39159, 999, 306, 6, 55, "Input"], Cell[39468, 1007, 103, 3, 48, "Text"] }, Open ]], Cell[CellGroupData[{ Cell[39608, 1015, 96, 2, 62, "Subsubsection"], Cell[39707, 1019, 2021, 32, 454, "Text"], Cell[41731, 1053, 880, 16, 211, "Text"], Cell[42614, 1071, 1183, 22, 292, "Text"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell[43846, 1099, 106, 3, 79, "Section"], Cell[43955, 1104, 322, 5, 102, "Text"], Cell[44280, 1111, 121, 3, 48, "Text"], Cell[44404, 1116, 102, 2, 41, "Input"], Cell[44509, 1120, 137, 3, 48, "Text"], Cell[44649, 1125, 920, 16, 216, "Input"], Cell[45572, 1143, 1700, 33, 170, "Input"], Cell[47275, 1178, 296, 5, 102, "Text"], Cell[47574, 1185, 117, 2, 41, "Input"], Cell[47694, 1189, 345, 9, 75, "Text"] }, Open ]], Cell[CellGroupData[{ Cell[48076, 1203, 62, 0, 79, "Section"], Cell[CellGroupData[{ Cell[48163, 1207, 61, 0, 62, "Subsubsection"], Cell[48227, 1209, 92, 2, 48, "Text"], Cell[48322, 1213, 102, 2, 41, "Input"], Cell[48427, 1217, 19, 0, 48, "Text"], Cell[48449, 1219, 130, 2, 41, "Input"], Cell[48582, 1223, 409, 11, 102, "Text"], Cell[48994, 1236, 629, 11, 156, "Text"], Cell[49626, 1249, 130, 2, 41, "Input"], Cell[49759, 1253, 47, 0, 48, "Text"], Cell[49809, 1255, 102, 2, 41, "Input"], Cell[49914, 1259, 105, 3, 48, "Text"] }, Open ]], Cell[CellGroupData[{ Cell[50056, 1267, 96, 3, 62, "Subsubsection"], Cell[50155, 1272, 111, 3, 48, "Text"], Cell[50269, 1277, 80, 1, 41, "Input"], Cell[50352, 1280, 19, 0, 48, "Text"], Cell[50374, 1282, 66, 1, 41, "Input"], Cell[50443, 1285, 276, 5, 75, "Text"], Cell[50722, 1292, 150, 3, 93, "Input"], Cell[50875, 1297, 411, 7, 129, "Text"], Cell[51289, 1306, 67, 0, 48, "Text"], Cell[51359, 1308, 147, 3, 87, "Input"], Cell[51509, 1313, 81, 2, 48, "Text"], Cell[51593, 1317, 131, 3, 48, "Text"], Cell[51727, 1322, 53, 1, 41, "Input"], Cell[51783, 1325, 71, 0, 48, "Text"], Cell[51857, 1327, 884, 24, 88, "Input"], Cell[52744, 1353, 65, 2, 48, "Text"], Cell[52812, 1357, 206, 4, 75, "Text"], Cell[53021, 1363, 88, 1, 41, "Input"], Cell[53112, 1366, 65, 0, 48, "Text"], Cell[53180, 1368, 254, 7, 138, "Input"], Cell[53437, 1377, 137, 6, 49, "Text"], Cell[53577, 1385, 221, 5, 75, "Text"], Cell[53801, 1392, 956, 24, 114, "Input"], Cell[54760, 1418, 315, 6, 102, "Text"], Cell[55078, 1426, 56, 1, 41, "Input"], Cell[55137, 1429, 69, 0, 48, "Text"], Cell[55209, 1431, 840, 23, 114, "Input"], Cell[56052, 1456, 136, 5, 49, "Text"], Cell[56191, 1463, 203, 4, 75, "Text"], Cell[56397, 1469, 605, 15, 98, "Input"], Cell[57005, 1486, 429, 5, 241, "Text"], Cell[57437, 1493, 155, 3, 75, "Text"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell[57641, 1502, 29, 0, 79, "Section"], Cell[57673, 1504, 159, 4, 75, "Text"], Cell[57835, 1510, 288, 6, 75, "Text"], Cell[58126, 1518, 140, 2, 48, "Text"], Cell[58269, 1522, 516, 12, 130, "Text"] }, Open ]], Cell[CellGroupData[{ Cell[58822, 1539, 29, 0, 79, "Section"], Cell[58854, 1541, 141, 5, 102, "Text"], Cell[58998, 1548, 523, 13, 129, "Text"], Cell[59524, 1563, 792, 21, 157, "Text"], Cell[60319, 1586, 766, 19, 184, "Text"], Cell[61088, 1607, 380, 7, 129, "Text"], Cell[61471, 1616, 247, 5, 129, "Text"], Cell[61721, 1623, 277, 5, 102, "Text"] }, Open ]], Cell[CellGroupData[{ Cell[62035, 1633, 67, 0, 79, "Section"], Cell[CellGroupData[{ Cell[62127, 1637, 37, 0, 62, "Subsubsection"], Cell[62167, 1639, 600, 15, 119, "Input"], Cell[62770, 1656, 1066, 24, 168, "Input"], Cell[63839, 1682, 805, 14, 148, "Input"], Cell[64647, 1698, 489, 11, 121, "Input"], Cell[65139, 1711, 1100, 25, 132, "Input"], Cell[66242, 1738, 791, 16, 132, "Input", InitializationCell->True, CellTags->"Definition (is longer than)"], Cell[67036, 1756, 176, 3, 56, "Input"], Cell[67215, 1761, 163, 2, 56, "Input"], Cell[67381, 1765, 221, 4, 82, "Input"], Cell[67605, 1771, 818, 14, 181, "Input"] }, Open ]], Cell[CellGroupData[{ Cell[68460, 1790, 31, 0, 62, "Subsubsection"], Cell[68494, 1792, 604, 11, 92, "Input"] }, Open ]], Cell[CellGroupData[{ Cell[69135, 1808, 35, 0, 62, "Subsubsection"], Cell[69173, 1810, 107, 2, 55, "Input"], Cell[69283, 1814, 175, 3, 55, "Input"], Cell[69461, 1819, 730, 13, 198, "Input"], Cell[70194, 1834, 375, 7, 92, "Input"] }, Open ]] }, Open ]] }, Open ]] } ] *) (******************************************************************* End of Mathematica Notebook file. *******************************************************************)