Searched refs:prove (Results 1 - 7 of 7) sorted by relevance

/hets/OWL2/java/de/unibremen/informatik/FactProver/
H A DProve.java20 boolean res = prover.prove();
H A DFactProver.java119 public boolean prove() throws FaCTPlusPlusException { method in class:FactProver
/hets/Maude/doc/
H A Ddg.tex194 \cite{MAH-05-a}. This can be used to prove Maude views, like e.g.\
195 ``natural numbers are a total order.'' For example, we could prove
408 Let $n$ be a $N$-model. To prove that $n$ is also a $N'$-model,
/hets/doc/
H A DUserGuide.tex727 check (\texttt{cell} option), but may prove more efficient in case
1226 \item[Prove] Try to prove the local proof goals. See Section~\ref{sec:Proofs}
1522 entries. \url{http://localhost:8000/123456789?prove=Nat\_\_E1\&prover=SPASS\&timeout=5}
1523 would try to prove the goals of the node \texttt{Nat\_\_E1} using the prover
1847 have no satisfying assignment, to prove theorems with zChaff. That is why you see
H A DUserGuideCommonLogic.tex403 is essential if you want to prove inductive theorems about
783 With choosing Edit→Proofs→Auto-DG prover, you can can prove red theorem
1229 In order to prove or disprove a theorem, it needs to be declared as proof
H A Dhs2isa.tex585 \noindent With these, it is now easy to prove, via induction, that map
1103 \emph{Tx}, the user needs to prove the monad axioms as HOL lemmas (in this
/hets/CASL/Termination/
H A DAProVE.jarMETA-INF/ META-INF/MANIFEST.MF aprove/ aprove/CommandLineInterface/ aprove/Framework/ aprove/Framework/Algebra/ aprove/Framework/ ...

Completed in 28 milliseconds