Lines Matching refs:axioms
293 | SPEC then SPEC %% extension of a spec with new symbols and axioms
453 axioms for all proof goals \\\hline
719 associated with a signature and some set of local axioms. The axioms
731 postulates that all axioms of the source node (including the inherited
733 that the local axioms of the source node hold in the target node.
791 important ones. With ``Add sentence'', you can add axioms and
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}.
887 \texttt{lower.clif}; these can be found in the \texttt{CommonLogic/Examples} directory in the \Hets library \cite{hets-library:URL}. The only difference in the actual axioms is that
931 The COLORE \cite{Colore} module \texttt{Region\-Boolean\-Contact\-Algebra} relatively interprets the module \texttt{Atomless\-Boolean\-Lattice}. These two modules specify axioms about booleans; thus, they have the same signature. In the graph of imports, they have several common imported modules (e.g.\ \texttt{Bounded\-Distributive\-Lattice}), but no common importing module, as can be seen from Fig.~\ref{fig:colore-graph}.
1201 proved goal the used axioms, its proof script, and its proof are shown ---
1217 the bottom lists the axioms and proven theorems that will comprise the