171 logic, but extends first-order logic in two ways: \begin{inparaenum}[(1)]\item any term can be
172 used as function or predicate, and \item sequence markers allow
180 \item a parser for the Common Logic Interchange Format (CLIF) --- CLIF
182 \item a connection of CL to well-known first-order theorem provers
185 \item a connection of CL to the higher-order provers Isabelle/HOL
188 \item a connection to first-order model finders like darwin that
190 \item support for proving interpretations between CL theories to be correct;
191 \item a translation that eliminates the use of CL modules\footnote{Actually, we are using a revised semantics for modules, as proposed
195 \item a translation of the Web Ontology Language OWL to CL;
196 \item a translation of propositional logic to CL.
334 \item[Common Logic] is an ISO standard published as ``ISO/IEC 24707:2007 - Information technology — Common Logic (CL): a framework for a family of logic-based languages'' \cite{CommonLogic:oldfashioned}. It is based on first-order logic, but extends first-order
340 \item[OWL2] is the Web Ontology Language recommended by the
352 \item[Propositional] is classical propositional logic, with
355 \item[SoftFOL] \cite{LuettichEA06a} offers several automated theorem
356   proving (ATP) systems for first-order logic with equality: \begin{inparaenum}[(1)]\item \SPASS
358 \item Darwin \cite{Baumgartner:etal:Darwin:IJAIT:2005}, see \url{http://combination.cs.uiowa.edu/Darwin};
359 \item Vampire \cite{RiazanovV02} see \url{http://www.vprover.org};
360 \item Eprover \cite{Schulz:AICOM-2002}, see \url{http://www.eprover.org};
361 \item E-KRHyper \cite{DBLP:conf/cade/PelzerW07}, see \url{http://www.uni-koblenz.de/~bpelzer/ekrhyper}, and 
362 \item 
371 \item[CASL] extends many sorted first-order logic with partial
378 \item[\Isabelle] \cite{NipPauWen02} is the logic of the interactive
381 \item[THF] is an interchange language for higher-order logic
386 \item[HasCASL] is a higher order extension of \CASL allowing
393 \item[RelScheme] is a logic for relational databases \cite{DBLP:journals/ao/SchorlemmerK08}.
480 \item
495 \item For Mac OS X 10.6 (Snow Leopard) we provide a meta package
498 \item
527 \item
534 \item
595 \item[\texttt{-p}, \texttt{-{}-just-parse}] Just do the parsing
597 \item[\texttt{-s}, \texttt{-{}-just-structured}] Do the parsing and the
604 \item[\texttt{-L DIR}, \texttt{-{}-hets-libdir=DIR}]
679   \item[Pred.clif:]~\\
686   \item[Cat.clif:]~\\
694   \item[Spec.clif:]~\\
760 \item[\texttt{-g}, \texttt{-{}-gui}] shows the development graph in a GUI window
761 \item[\texttt{-u}, \texttt{-{}-uncolored}] no colours in shown graphs
767 \item[\texttt{-A}, \texttt{-{}-apply-automatic-rule}] apply the automatic
770 \item[\texttt{-N}, \texttt{-{}-normal-form}] compute all normal forms for nodes
803 \item[Importation] \label{descr:link_import}
828 \item[Relative interpretation]
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}.
861 \item[Inclusion]
891 \item[upper.clif:]~\\
898 \item[lower.clif:]~\\
1051 \item Heterogeneous specification allows for reusing the OpenAAL OWL ontology, but at the same time formalizing a first-order spatial calculus.
1052 \item In particular, the compact representation of mutual disjointness chosen here makes use of Common Logic's sequence markers.
1053 \item As Common Logic module extends the previously imported OWL ontology, it has access to all entities of the OWL ontology by name; in particular, we can specify that two rooms are connected (in terms of the OpenAAL terminology) if certain conditions in terms of our Common Logic module, or certain conditions in terms of OpenAAL hold.
1198 \item The button `Display' shows the selected goals in the ASCII syntax of
1200 \item By pressing the `Proof details' button a window is opened where for each
1203 \item With the `Prove' button the actual prover is launched. The provers are described
1205 \item The list `Pick Theorem Prover:' lets you choose one of the connected
1210 \item The pop-up choice box below `Selected comorphism path:' lets you pick a
1215 \item Since the amount and kind of sentences sent to an ATP system is a major
1223 \item If you press the bottom-right `Close' button the window is closed and
1226 \item All other buttons control selecting list entries.
1372     \item[a]
1442 \item[\texttt{-i ITYPE}, \texttt{-{}-input-type=ITYPE}] Specify \texttt{ITYPE}
1473 \item[\texttt{-O DIR}, \texttt{-{}-output-dir=DIR}]
1476 \item[\texttt{-o OTYPES}, \texttt{-{}-output-types=OTYPES}]
1567 \item[\texttt{-t TRANS}, \texttt{-{}-translation=TRANS}]
1571 \item[\texttt{-n SPECS}, \texttt{-{}-spec=SPECS}]
1574 \item[\texttt{-w NVIEWS}, \texttt{-{}-view=NVIEWS}]
1577 \item[\texttt{-R}, \texttt{-{}-recursive}] output also imported libraries
1579 \item[\texttt{-I}, \texttt{-{}-interactive}] run \Hets in interactive mode
1581 \item[\texttt{-X}, \texttt{-{}-server}] run \Hets as web server (see
1584 \item[\texttt{-x}, \texttt{-{}-xml}] use XML-PGIP\footnote{Proof General Interface Protocol} packets to communicate with
1587 \item[\texttt{-S PORT}, \texttt{-{}-listen=PORT}] communicate
1590 \item[\texttt{-c HOSTNAME:PORT}, \texttt{-{}-connect=HOSTNAME:PORT}] communicate
1594 \item[\texttt{-d STRING}, \texttt{-{}-dump=STRING}] produces implementation
1616 \item[\texttt{-v[Int]}, \texttt{-{}-verbose[=Int]}]
1618 \item[\texttt{-q}, \texttt{-{}-quiet}]
1620 \item[\texttt{-V}, \texttt{-{}-version}] Print version number and exit.
1621 \item[\texttt{-h}, \texttt{-{}-help}, \texttt{-{}-usage}]
1623 \item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
1626 \item[\texttt{-l LOGIC}, \texttt{-{}-logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
1628 \item[\texttt{-e ENCODING}, \texttt{-{}-encoding=ENCODING}] Read input files using latin1 or utf8 encoding. The default is still latin1.
1629 \item[\texttt{-{}-unlit}] Read literate input files.
1630 \item[\texttt{-{}-relative-positions}] Just uses the relative library name in positions of warning or errors.
1631 \item[\texttt{-U FILE}, \texttt{-{}-xupdate=FILE}] update a development graph according to special XML update information (still experimental).
1632 \item[\texttt{-m FILE}, \texttt{-{}-modelSparQ=FILE}] model check a qualitative calculus given in SparQ lisp notation \cite{SparQ06} against a \CASL specification

Indexes created Tue Jul 24 14:28:13 CEST 2018