Searched refs:axioms (Results 1 - 11 of 11) sorted by relevance

/hets/OWL2/java/de/unibremen/informatik/locality/
H A DLocalityChecker.java20 private static Set<OWLAxiom> axioms; field in class:LocalityChecker
61 Iterator<OWLAxiom> it = axioms.iterator();
77 Iterator<OWLAxiom> it = axioms.iterator();
102 axioms = ontology.getAxioms();
/hets/doc/
H A Dcollected_proposals.tex32 axioms. If such theories are translated to Isabelle for proving
33 several axioms have the same label. For this problem the \CASL
H A DUserGuideCommonLogic.tex293 | 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 abou
[all...]
H A Dhs2isa.tex352 further specified using a set of axioms; for example, the class
354 order axioms. Of course, such axiomatizations are not possible in
371 satisfy the axioms of the class. Since our translation only generates
372 classes without axioms (beyond those of $pcpo$), proofs are trivial
1000 that satisfy the monadic axioms. This solution can be expressed in terms of
1002 signatures and axioms to theorems in ways that preserve operations and
1008 axioms, constants and type declarations. Building a theory morphism from
1019 respectively) and the relevant axioms (in \emph{MonadAxms}). To show that a
1024 the axioms. The following gives an example. \\
1103 \emph{Tx}, the user needs to prove the monad axioms a
[all...]
H A DUserGuide.tex520 axioms for all proof goals \\\hline
850 associated with a signature and some set of local axioms. The axioms
862 postulates that all axioms of the source node (including the inherited
864 that the local axioms of the source node hold in the target node.
1211 origin of the node and the local theory i.e. axioms declared locally.
1213 \item[Show theory] Shows the theory of the node (including axioms
1214 imported from other nodes). Notice that axioms imported via hiding links
1234 consistency checkers. Other goals will be treated like axioms if ``Include
1583 proved goal the used axioms, it
[all...]
/hets/Isabelle/export/
H A Dexport_helper.ml356 val axioms = e (content "axioms") #> many ((p name)
430 in oneOf [dt_type,consts,axioms,cls,
637 (* name * fixes * in-locale axioms *
638 ex-locale axioms * parents *)
658 (* axioms * theorems * consts *)
668 (* name * axioms * theorems * consts * datatypes *
691 (* name * axioms * theorems * consts * datatypes *
827 val axioms' = List.map (fn (n,t) => (n,(HOLogic.dest_Trueprop o #2
835 val axioms
[all...]
H A Dparser.ml312 ("axioms",Scan.repeat1 Parse_Spec.spec >> Axioms), (* line 173 *)
/hets/OWL2/java/de/unibremen/informatik/FactProver/
H A DFactProver.java105 Set<OWLAxiom> axioms = ontology.getAxioms();
106 for (Iterator<OWLAxiom> i = axioms.iterator(); i.hasNext();) {
111 if (axioms.size() == 1) {
112 Iterator<OWLAxiom> it = axioms.iterator();
115 throw new OWLOntologyCreationException("Too many axioms for conjecture");
/hets/Maude/doc/
H A Ddg.tex19 no local axioms and stands for the free models of the theory.
316 The axioms $\psi^K$ of the node $K$ consist of:
418 is given by the free types axioms (i.e. sorts are interpreted as set of terms,
442 Notice that the first three types of axioms of the node $K$ hold by construction and also
452 axioms of $K$ fix the interpretation of $\iota(\Sigma_M)$ and therefore $ker(k'_h)$ and
H A Dmaude.tex9 axioms characterizing the elements of a sort. In the following sections we
32 \emph{membership axioms} of the form $t : s$, where the term $t$
299 have sorts, subsort relationships, operators, variables, membership axioms,
/hets/OWL2/java/lib/
H A Dowlapi-osgidistribution-3.5.2.jar ... .OWLClassExpression unsatClass java.util.Set axiomWindow Object[] axioms int windowCount int remainingAxiomsCount private void performSlowPruning (org.semanticweb ...

Completed in 36 milliseconds