293 \item[CASL] extends many sorted first-order logic with partial
311 \item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
315 \item[ModalCASL] \cite{ModalCASL}
321 \item[ExtModal] is an extended modal logic, subsuming and replacing ModalCASL.
326 \item[HasCASL] is a higher order extension of \CASL allowing
334 \item[Haskell] is a modern, pure and strongly typed functional programming
341 \item[CspCASL] \cite{Roggenbach06} is a combination of \CASL
344 \item[CommonLogic] \url{http://en.wikipedia.org/wiki/Common_logic}
346 \item[ConstraintCASL] is an experimental logic for the specification
349 \item[OWL 2] is the Web Ontology Language (OWL 2) recommended by the
362 \item[CASL-DL] \cite{OWL-CASL-WADT2004}
373 \item[Propositional] is classical propositional logic, with
376 \item[QBF] are quantified boolean formulas, with
379 \item[RelScheme] is a logic for relational databases \cite{DBLP:journals/ao/SchorlemmerK08}.
381 \item[SoftFOL] \cite{LuettichEA06a} offers several automated theorem
384 \item \SPASS
386 \item Vampire \cite{RiazanovV02} see \url{http://www.vprover.org};
387 \item Darwin \cite{Baumgartner:etal:Darwin:IJAIT:2005}, see \url{http://combination.cs.uiowa.edu/Darwin};
388 \item Eprover \cite{Schulz:AICOM-2002}, see \url{http://www.eprover.org};
389 \item E-KRHyper \cite{DBLP:conf/cade/PelzerW07}, see \url{http://www.uni-koblenz.de/~bpelzer/ekrhyper}, and
390 \item
399 \item[THF] simply typed lambda calculus, is an interchange language for
405 \item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover
408 \item[HolLight] \url{http://www.cl.cam.ac.uk/~jrh13/hol-light/}
412 \item[VSE] is an interactive theorem prover, see \ref{subsec:VSE}.
414 \item[DMU] is a dummy logic to read output of ``Computer Aided
417 \item[FreeCAD] is a logic to read design files of the CAD system
420 \item[Maude] is a rewrite system \url{http://maude.cs.uiuc.edu/} for
426 \item[DFOL] is an extension of first-order logic with dependent types \cite{rabe:dfol:06}.
428 \item [LF] is the dependent type theory of Twelf \url{http://twelf.plparty.org/}. Hets
436 \item[Framework] is a dummy logic added for declarative logic definitions \cite{CHK+2011a}.
438 \item[Adl] is ``A Description Language'' based on relational algebra originally
442 \item[Fpl] is a ``logic for functional programs'' as an extension of a
445 \item[EnCL] is an ``engineering calculation language'' based on first
451 \item[Hybrid] HybridCASL \cite{DBLP:conf/calco/NevesMMB13} extends ModalCASL by implementing
584 \item
619 \item For Mac OSX we provide disk images \texttt{Hets-<date>.dmg} without GTK support.
621 \item
700 \item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing
702 \item[\texttt{-s}, \texttt{--just-structured}] Do the parsing and the
709 \item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
712 \item[\texttt{-a ANALYSIS}, \texttt{--casl-amalg=ANALYSIS}]
719   \item[\texttt{sharing}] perform sharing analysis for sorts,
721   \item[\texttt{cell}] perform cell condition check; implies
724   \item[\texttt{colimit-thinness}] perform colimit thinness check;
893 \item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window
894 \item[\texttt{-u}, \texttt{--uncolored}] no colors in shown graphs
900 \item[\texttt{-A}, \texttt{--apply-automatic-rule}] apply the automatic
903 \item[\texttt{-N}, \texttt{--normal-form}] compute all normal forms for nodes
1084 \item[Named nodes] correspond to a named specification.
1085 \item[Unnamed nodes] correspond to an anonymous specification.
1086 \item[Elliptic nodes] correspond to a specification in the current library.
1087 \item[Rectangular nodes] are external nodes corresponding to a specification
1089 \item[Red nodes] have open proof obligations.
1090 \item[Yellow nodes] have an open conservativity proof obligations.
1091 \item[Green nodes] have all proof obligations resolved.
1092 \item[Black links] correspond to reference to other specifications (definition
1094 \item[Red links] correspond to open proof obligations (theorem links).
1095 \item[Green links] correspond to proven theorem links.
1096 \item[Yellow links] correspond to proven theorem links with open
1098 \item[Blue links] correspond to hiding, free, or cofree definition links.
1099 \item[Violett links] correspond to a mixture of links becoming visible after
1101 \item[Solid links] correspond to global (definition or theorem)
1103 \item[Dashed links] correspond to local (theorem) links in the sense of
1107 \item[Single line links] have homogeneous signature morphisms (staying within
1109 \item[Double line links] have heterogeneous signature morphisms (moving
1123 \item[Edit] This menu has the following submenus:
1125 \item[Undo] Undo the last development graph proof step (see under Proofs)
1126 \item[Redo] Restore the last undone development graph proof step (see
1128 \item[Hide/show names/nodes/edges]
1149 \item[Focus node]
1156 \item[Select Linktypes]
1164 \item[Consistency checker]
1170 \item[Proofs] This menu allows to apply some of the deduction rules
1187 \item[Dump Development Graph] This option is available only for
1191 \item[Show Library Graph] This menu displays the library graph, in a separate
1195 \item[Save Graph for uDrawGraph] Saves the development graph in a .udg file
1198 \item[Save proof-script] This menu saves the proof rules that have been applied
1204 \item[Pop-up menu for nodes]
1208 \item[Show node info] Shows the local informations of the node: the internal
1213 \item[Show theory] Shows the theory of the node (including axioms
1219 \item[Translate theory] Translates the theory of a node to another logic.
1222 \item[Taxonomy graphs] (Only available for some logics) Shows the subsort graph
1225 \item[Show proof status] Show open and proven local proof goals.
1226 \item[Prove] Try to prove the local proof goals. See Section~\ref{sec:Proofs}
1229 \item[Prove VSE structured] Allows to send a development graph below the
1233 \item[Disprove] Negates selected goals and tries to disprove them using
1238 \item[Add sentence] This menu allows to add a sentence on the fly. The
1241 \item[Check consistency] Simply calls the global ``Consistency checker'' menu
1244 \item[Check conservativity] Checks conservativity of the inclusion
1256 \item[Pop-up menu for links]
1259 \item[Show info] Shows informations about the edge: internal number and
1267 \item[Check conservativity] (Experimental) Check whether the
1270 \item[Expand]This menu is available only for paths going through unnamed
1279 \item[Edit] This menu for library graphs has the following submenus:
1281 \item[Reload Library] Reloads all \HetCASL sources in order to avoid closing
1285 \item[Experimental reload changed Library] This button is supposed to
1288 \item[Translate Library] Translates a library along a comorphism to be chosen.
1293 \item[Show Logic Graph] Shows the graph of logics and logic comorphisms
1297 \item[Show detailed logic graph] Shows the important sublogics and comorphims
1309 \item[\texttt{-i ITYPE}, \texttt{--input-type=ITYPE}] Specify \texttt{ITYPE}
1345 \item[\texttt{-O DIR}, \texttt{--output-dir=DIR}]
1348 \item[\texttt{-o OTYPES}, \texttt{--output-types=OTYPES}]
1448 \item[\texttt{-t TRANS}, \texttt{--translation=TRANS}]
1452 \item[\texttt{-n SPECS}, \texttt{--spec=SPECS}]
1455 \item[\texttt{-w NVIEWS}, \texttt{--view=NVIEWS}]
1458 \item[\texttt{-R}, \texttt{--recursive}] output also imported libraries
1460 \item[\texttt{-I}, \texttt{--interactive}] run \Hets in interactive mode
1462 \item[\texttt{-X}, \texttt{--server}] run \Hets as web server (see
1465 \item[\texttt{-x}, \texttt{--xml}] use xml-pgip packets to communicate with
1468 \item[\texttt{-S PORT}, \texttt{--listen=PORT}] communicate
1471 \item[\texttt{-c HOSTNAME:PORT}, \texttt{--connect=HOSTNAME:PORT}] communicate
1475 \item[\texttt{-d STRING}, \texttt{--dump=STRING}] produces implementation
1535 \item[\texttt{-v[Int]}, \texttt{--verbose[=Int]}]
1537 \item[\texttt{-q}, \texttt{--quiet}]
1539 \item[\texttt{-V}, \texttt{--version}] Print version number and exit.
1540 \item[\texttt{-h}, \texttt{--help}, \texttt{--usage}]
1542 \item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
1545 \item[\texttt{-l LOGIC}, \texttt{--logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
1547 \item[\texttt{-e ENCODING}, \texttt{--encoding=ENCODING}] Read input files using latin1 or utf8 encoding. The default is still latin1.
1548 \item[\texttt{--unlit}] Read literate input files.
1549 \item[\texttt{--relative-positions}] Just uses the relative library name in positions of warning or errors.
1550 \item[\texttt{-U FILE}, \texttt{--xupdate=FILE}] update a development graph according to special xml update information (still experimental).
1551 \item[\texttt{-m FILE}, \texttt{--modelSparQ=FILE}] model check a qualitative calculus given in SparQ lisp notation \cite{SparQ06} against a \CASL specification
1580 \item The button `Display' shows the selected goals in the ASCII syntax of
1582 \item By pressing the `Proof details' button a window is opened where for each
1585 \item With the `Prove' button the actual prover is launched. This is described
1587 \item The list `Pick Theorem Prover:' lets you choose one of the connected
1592 \item The pop-up choice box below `Selected comorphism path:' lets you pick a
1594 \item Since the amount and kind of sentences sent to an ATP system is a major
1602 \item If you press the bottom-right `Close' button the window is closed and
1605 \item All other buttons control selecting list entries
1704     \item[a]
1960 \item There is no proof support for architectural specifications.
1961 \item Distributed libraries are always downloaded from the local disk,
1963 \item Version numbers of libraries are not considered properly.
1964 \item The proof engine for development graphs provides only experimental

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