Lines Matching defs:and
10 \usepackage{charter} % very clean and readable font
26 \usepackage{lstsemantic} % loads listings and defines some languages
52 %% following the points (and some others in the text):
172 used as function or predicate, and \item sequence markers allow
183 like SPASS, darwin and Vampire, such that logical consequences
186 and Leo-II in order to perform induction proofs in theories
204 \section{The Heterogeneous Tool Set and Its Input Languages}
207 provide a general framework for formal methods integration and proof
210 being individual logics (with their analysis and proof tools) as well
213 and more, as well as model finders). Hence, a variety of tools is
220 \caption{The \Hets motherboard and some expansion cards}
223 \Hets consists of logic-specific tools for the parsing and static
225 logic-independent parsing and static analysis tool for structured and
226 architectural specifications and libraries. The latter of course needs
236 Logic and OWL2 and \HetCASL. They will be described in the next
239 \subsection{Common Logic and the Common Logic Interchange Format (CLIF)}
243 CLIF syntax, and also recursively reads in any imported files (cf.\ Sect.~\ref{relationsInCL} for the syntax).
247 features that speak about structuring and comparing logical
253 interpretations and other things, see Sect.~\ref{HetCASL} below.
260 Manchester syntax \cite{w3c:owl2-manchester}, as well as RDF \cite{w3c:owl2-RDF-mapping}. The RDF data model has multiple possible syntaxes itself, including RDF/XML \cite{w3c04:rdf-xml} and the text-oriented Turtle syntax \cite{w3c:turtle}.
262 Since OWL2 does not support relative theory interpretations and other
279 (if they are formalised as institutions and plugged into
286 currently supported logics and logic translations (the latter are also
287 called comorphisms) is shown in Fig.~\ref{fig:LogicGraph}, and the
291 \begin{lstlisting}[float,label={fig:lang},caption={Syntax of a simple subset of the heterogeneous specification language. \texttt{BASIC-SPEC} and \texttt{SYMBOL-MAP} have a logic specific syntax, while \texttt{ID} stands for some form of identifiers.},basicstyle=\ttfamily\small,morecomment={[l]{\%\%\ }},morekeywords={then,with,logic,spec,end,view,to},escapeinside={<>}]
293 | SPEC then SPEC %% extension of a spec with new symbols and axioms
309 combine and rename specifications, hide parts thereof, and also
312 libraries} are collections of named structured and architectural
338 other dialects, send us a message and we will add them.
345 written in Java to obtain the abstract syntax for an OWL file and its
347 the OWL ontology into the sublanguages OWL Full (all of OWL, under the RDF semantics, undecidable \cite{w3c:owl2-rdf-based-semantics}), OWL DL (all of OWL, under the direct semantics \cite{w3c:owl2-direct-semantics}), and the so-called OWL Profiles (i.e.\ proper sublanguages) OWL EL, OWL QL, and OWL RL \cite{w3c:owl2-profiles}.
361 \item E-KRHyper \cite{DBLP:conf/cade/PelzerW07}, see \url{http://www.uni-koblenz.de/~bpelzer/ekrhyper}, and
372 functions and subsorting. It also provides induction sentences,
387 polymorphic datatypes and functions. It is closely related to the
388 programming language Haskell and allows program constructs being
391 to the provers Isabelle and Leo-II.
402 and Isabelle offer interfaces to higher-order provers, which
410 explain both the \CASL logic and language of basic specifications as
411 well as the logic-independent constructs for structured and
427 target logic. More precisely, one and the same logic translation
428 may have several source and target \emph{sub}logics: for
476 and Mac OS X.
500 Download a \texttt{.jar} file and start it with
506 \texttt{libglade2} package (and all its dependencies) yourself. In order to
510 a graphical interface. It will download and install further
529 You have to unpack it with \texttt{bunzip2} and then put it into
531 install the above mentioned software and set
537 link ``Hets: source code and information for developers''
539 svn), and follow the
543 Depending on your application further tools are supported and may be
568 (and (P x) (Q y))
572 (exists (z) (and (Pet x) (Happy z) (Attr x z)))
575 \Hets can be used for parsing and
596 -- the static analysis is skipped and no development graph is created.
597 \item[\texttt{-s}, \texttt{-{}-just-structured}] Do the parsing and the
627 Although the endings \texttt{.casl} and \texttt{.het} are
629 homogeneous \CASL specifications and the latter for \HetCASL libraries
638 The subsequent specifications are then parsed and analysed as
646 The endings \texttt{.clf} and \texttt{.clif} are available for directly reading in
649 the logic Common Logic has to be chosen explicitly, and the \CASL structuring
659 (and (P x) (Q y))
667 Pred and Cat then
668 . (exists (z) (and (Pet x) (Happy z) (Attr x z)))
683 (and (P x) (Q y))
698 (exists (z) (and (Pet x) (Happy z) (Attr x z)))
704 file with the extension \texttt{.het} and the latter in a file with one of the extensions
706 parts, which are linked to each other. These links and some more information can
713 structured theorem proving and proof management.
716 structured specifications or parts thereof), and a set of edges
719 associated with a signature and some set of local axioms. The axioms
735 Both definition and theorem links can be \emph{homogeneous},
743 into simpler (local and global) ones. Theorem links that have been
751 on a theorem \cite{Habil} stating soundness and relative completeness
755 and in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
765 graph calculus to the final graph and save applying these rules via the GUI.
771 with incoming hiding links. (This may take long and may not be implemented
775 For a summary of the types of nodes and links occurring in
787 Moreover, the nodes and links of the
788 graph have attached pop-up menus, which appear when clicking (and
790 The node menus ``Prove'' and ``Check consistency'' are the most
791 important ones. With ``Add sentence'', you can add axioms and
799 them, the importation, is defined in ISO/IEC 24707:2007 \cite{CommonLogic:oldfashioned}, and has a syntax within Common Logic. All the other relations are
800 unofficial extensions used e.g.\ by the Common Logic Repository COLORE \cite{Colore}, and represented externally of Common Logic texts. COLORE currently represents them in external XML documents, and any required symbol maps in external CLIF files. \Hets, in contrast, allows for declaring them as \emph{views} within \HetCASL files, outside of specifications, as can be seen from the syntax specification in List.~\ref{fig:lang}.
807 them, send us a message at \href{mailto:hets@informatik.uni-bremen.de}{hets@informatik.uni-bremen.de}, and we will fix it.
814 for a file called \texttt{someFile.clif} in first place and then for
815 \texttt{someFile.clf} in the current directory and then in the library paths.
818 \texttt{file:}, \texttt{http:} and \texttt{https:}.
851 \item[Non-conservative extension] is informally defined as follows: One module non-conservatively extends other modules, if its “axioms entail new facts for the shared lexicon of the [other] module(s). [That is, the] shared lexicon between the current module and a [non-conservatively extended] module are not logically equivalent with respect to their modules.” \cite{Colore-metadata}.
872 Except for importation and inclusion, you can specify an optional symbol map
873 (name map) in a relation.\footnote{While the ``copy'' semantics of Common Logic importations does not permit renamings, \HetCASL's extension mechanism offers an alternative possibility to reuse ontologies and rename some of their symbols, using the ``\textit{importedSpec} \textbf{with} \textit{name1Old} |-> \textit{name1New}, \textit{name2Old} |-> \textit{name2New} \textbf{then} \textit{importingSpec}'' syntax.}
886 This example has two almost identical Common Logic texts, \texttt{upper.clif} and
922 and the target ontology; the other names (none in this concrete case) are implicitly the same. A mapping of a single name is defined with
925 Hence a space must be placed between the separation-comma and a name.
929 We give two examples for relative interpretation: one from COLORE (in this section), and one standalone one (in Sect.~\ref{sec:rel-intpr-standalone}).
937 \caption{Boolean algebras and lattices in COLORE (subgraph)}
943 For easier understanding, the \HetCASL implementation includes literal copies of the \texttt{Region\-Boolean\-Contact\-Algebra} and \texttt{Atomless\-Boolean\-Lattice} modules; actually, they could as well have been included from their respective files using \texttt{from ... get ...}.
958 (and (not (= y 0))
966 (if (and (not (= x 0))
969 (and (complement x y)
978 This example defines a partial order twice: once as an extension of a strict partial order, and once directly. Then, we connect both definitions by a view that expresses the relative interpretation.
995 (if (and (lt x y)
1016 (if (and (le x y)
1021 (if (and (le x y)
1029 \subsubsection{Ontology-based Ambient Assisted Living Services and Devices}
1035 Clara instructs her \textbf{wheelchair} to get her to the \textbf{kitchen} (\textbf{\underline{next door}} to the \textbf{living room}. For \textbf{dinner}, she would like to take a pizza from the \textbf{freezer} and bake it in the \textbf{oven}. (Her diet is vegetarian.) \textbf{\underline{Afterwards}} she needs to rest in \textbf{bed}.
1037 Existing ontologies for ambient assisted living (e.g.\ the OpenAAL\footnote{\url{http://openaal.org}} OWL ontology) cover the \emph{core} of these concepts; they provide at least classes (or generic superclasses) corresponding to the concepts highlighted in \textbf{bold}. However, that does not cover the scenario completely. In particular, there are relevant concepts (here: space and time, \underline{underlined}), which are not covered at the required level of complexity. OpenAAL says that appointments have a date and that rooms can be connected to each other, but not what exactly that means. Foundational ontologies and spatial calculi, often formalized in first-order logic, cover space and time at the level of complexity required by a central controller of an apartment and by an autonomously navigating wheelchair.
1084 (and (forall (...x)
1085 (not (and (p ...x) (q ...x))))
1099 %% and "is-door-of", but otherwise we wouldn't be able to restrict the
1107 (and (Door door)
1117 In the previous example, we established a link between an OWL ontology and a Common Logic ontology by reusing elements of the signature of the OWL ontology (concretely: OpenAAL's \texttt{is-in-room} predicate) in the Common Logic ontology.
1121 The following example, which is available as \texttt{Ontology/Examples/TimeInOWLandCL.het} in the \Hets library \cite{hets-library:URL}, establishes a view between the OWL Time ontology and its reimplementation in Common Logic, \ednote{CL: There is no way to make that explicit in \HetCASL, is there?\\ TM: you mean the datatype stuff that the OWL to CL translation generates? We should modify the translation to generate this only if really needed.\\ CL: No, I just thought (and was wrong) that \HetCASL had no way of explicitly choosing a logic translation. But not I don't understand what \emph{you} mean. Maybe it's related to the error that I get when loading the file; see my ticket.}using the ``OWL22CommonLogic'' translation:
1135 %% CommonLogic equivalent of Domain and Range above
1138 (and (TemporalEntity t1)
1142 (if (and (before t1 t2)
1161 on the Edit-menu in the development graph window and selecting
1170 indicates a disproved goal, a space denotes an open goal, and a
1184 \caption{\Hets Goal and Prover Interface\label{fig:proof_window}}
1201 proved goal the used axioms, its proof script, and its proof are shown ---
1206 provers (among them \Isabelle, MathServe Broker, \SPASS, Vampire, and
1208 launched and the theory along with the selected goals is translated via the
1215 \item Since the amount and kind of sentences sent to an ATP system is a major
1217 the bottom lists the axioms and proven theorems that will comprise the
1219 vary and so do the available provers and the comorphism paths leading to provers. Former
1223 \item If you press the bottom-right `Close' button the window is closed and
1237 (and (P x) (Q y))
1243 In this specification\footnote{\texttt{HelloWorldExamples/ToProve.het} in the \Hets library \cite{hets-library:URL}} the theorems, annotated (named) by \texttt{correct} and
1254 (and (P x) (Q y))
1264 keyword of \Hets must be used, and thus the specification is not pure CLIF. Because the texts have
1301 (Fig.~\ref{fig:cons_res}) will pop up and allow you to inspect the models for
1326 preceding proven theorems in next proof attempt' and pressing `Prove all'
1333 of the ATP system. The `Save' buttons allow you to save the input and
1342 (SPCs) defined upon the basis of logical, language and syntactical
1343 properties by Sutcliffe and Suttner \cite{SutcliffeEA:2001:EvalATP}.
1345 by \Hets currently: Vampire and the brokering system. The ATP systems
1346 are offered as Web Services using standardised protocols and formats
1347 such as SOAP, HTTP and XML. Currently, the ATP system Vampire may be
1395 has a very small core guaranteeing correctness, and its provers,
1398 and several mathematical textbooks have been partially
1430 now can replace the 'oops' commands with real \Isabelle proofs, and
1433 key sequence), and by exiting Emacs (Ctrl-x Ctrl-c).
1437 \section{Reading, Writing and Formatting}
1440 that are read and written.
1495 The \texttt{env} and \texttt{prf} formats are for subsequent reading,
1506 markup format and data model for Open Mathematical Documents. It
1507 serves as semantics-oriented representation format and ontology
1509 state, Common Logic theories can be exported to and imported from OMDoc.
1520 each specification in the library to \Isabelle, and write one \Isabelle
1524 the composition and inverse table of a Tarskian relation algebra from
1527 generated by basic relations, and that the specification is written
1596 (i.e.\ \texttt{-d LogicGraph} lists the logics and comorphisms)
1620 \item[\texttt{-V}, \texttt{-{}-version}] Print version number and exit.
1622 Print usage information and exit.