- \item The \emph{\GETTER} is a Web service to retrieve an (XML) document
- from a physical location (URL) given its logical name (URI). The Getter is
- responsible of updating a table that maps URIs to URLs. Thanks to the Getter
- it is possible to work on a logically monolithic library that is physically
- distributed on the network. More information on the Getter can be found
- in~\cite{zack-master}.
- \item \emph{\WHELP} is a search engine to index and locate mathematical
- notions (axioms, theorems, definitions) in the logical library managed
- by the Getter. Typical examples of a query to Whelp are queries that search
- for a theorem that generalize or instantiate a given formula, or that
- can be immediately applied to prove a given goal. The output of Whelp is
- an XML document that lists the URIs of a complete set of candidates that
- are likely to satisfy the given query. The set is complete in the sense
- that no notion that actually satisfies the query is thrown away. However,
- the query is only approximated in the sense that false matches can be
- returned. Whelp has been described in~\cite{whelp}.
- \item \emph{\UWOBO} is a Web service that, given the URI of a mathematical
- notion in the distributed library, renders it according to the user provided
- two dimensional mathematical notation. \UWOBO{} may also embed the rendering
- of mathematical notions into arbitrary documents before returning them.
- The Getter is used by \UWOBO{} to retrieve the document to be rendered.
- \UWOBO{} has been described in~\cite{zack-master}.
- \item The \emph{Proof Checker} is a Web service that, given the URI of
- notion in the distributed library, checks its correctness. Since the notion
- is likely to depend in an acyclic way over other notions, the proof checker
- is also responsible of building in a top-down way the DAG of all
- dependencies, checking in turn every notion for correctness.
- The proof checker has been described in~\cite{zack-master}.
- \item The \emph{Dependency Analyzer} is a Web service that can produce
- a textual or graphical representation of the dependencies of an object.
- The dependency analyzer has been described in~\cite{zack-master}.
+
+ \item The \emph{\GETTER}~\cite{zack-master} is a Web service to
+ retrieve an (XML) document from a physical location (URL) given its
+ logical name (URI). The Getter is responsible of updating a table that
+ maps URIs to URLs. Thanks to the Getter it is possible to work on a
+ logically monolithic library that is physically distributed on the
+ network.
+
+ \item \emph{\WHELP}~\cite{whelp} is a search engine to index and
+ locate mathematical concepts (axioms, theorems, definitions) in the
+ logical library managed by the Getter. Typical examples of
+ \WHELP{} queries are those that search for a theorem that generalize or
+ instantiate a given formula, or that can be immediately applied to
+ prove a given goal. The output of Whelp is an XML document that lists
+ the URIs of a complete set of candidates that are likely to satisfy
+ the given query. The set is complete in the sense that no concept that
+ actually satisfies the query is thrown away. However, the query is
+ only approximated in the sense that false matches can be returned.
+
+ \item \emph{\UWOBO}~\cite{zack-master} is a Web service that, given the
+ URI of a mathematical concept in the distributed library, renders it
+ according to the user provided two dimensional mathematical notation.
+ \UWOBO{} may also inline the rendering of mathematical concepts into
+ arbitrary documents before returning them. The Getter is used by
+ \UWOBO{} to retrieve the document to be rendered.
+
+ \item The \emph{Proof Checker}~\cite{zack-master} is a Web service
+ that, given the URI of a concept in the distributed library, checks its
+ correctness. Since the concept is likely to depend in an acyclic way
+ on other concepts, the proof checker is also responsible of building
+ in a top-down way the DAG of all dependencies, checking in turn every
+ concept for correctness.
+
+ \item The \emph{Dependency Analyzer}~\cite{zack-master} is a Web
+ service that can produce a textual or graphical representation of the
+ dependencies of a concept.
+