<html>
<head>
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">Dear Vit,<br>
<br>
many thanks for this useful suggestion!<br>
Indeed it seems that the main problem is not to find and integrate
tools that will provide answers to queries (like "what is 2+4"?),
but to extend the DOL language with queries in a semantic clean
way that is valid for all the DOL-conformant logics.<br>
<br>
Best, Till<br>
<br>
Am 06.06.2016 um 12:33 schrieb Koksa, Vit:<br>
</div>
<blockquote
cite="mid:B2ADAC13EB485944801892D44509A23D81488AA6@DE08W1302.global.ds.honeywell.com"
type="cite">
<meta http-equiv="Context-Type" content="text/html;
charset=us-ascii">
<meta name="Generator" content="Microsoft Word 15 (filtered
medium)">
<div class="WordSection1">
<p class="MsoNormal">Dear Till,</p>
<p class="MsoNormal"> </p>
<p class="MsoNormal">Thank you a lot for summarizing the status
of the querying capabilities.</p>
<p class="MsoNormal"> </p>
<p class="MsoNormal">I guess then that some ontology reasoner
integrated with Hets (e.g. Pellet) will accept queries about a
DOL ontology and provide the answers.</p>
<p class="MsoNormal"> </p>
<p class="MsoNormal">As for the natural numbers, if the
specification could be translated to the language of Princess,
this prover might respond with some valid value of the
existentially quantified variable.</p>
<p class="MsoNormal">When Princess is run (using Java Webstart
from over here <a moz-do-not-send="true"
href="http://www.philipp.ruemmer.org/princess-examples.shtml">
http://www.philipp.ruemmer.org/princess-examples.shtml</a> )
with the following (simplified as compared to the original
CASL spec) problem specification</p>
<p class="MsoPlainText"> </p>
<p class="MsoPlainText">\existentialConstants {</p>
<p class="MsoPlainText"> /* Declare existentially quantified
constants of the problem */</p>
<p class="MsoPlainText"> int peachesTogether;</p>
<p class="MsoPlainText">}</p>
<p class="MsoPlainText"> </p>
<p class="MsoPlainText">\problem {</p>
<p class="MsoPlainText">\forall int peachesAllan, peachesJake; (</p>
<p class="MsoPlainText"> peachesAllan = 2</p>
<p class="MsoPlainText"> -> peachesJake = 4</p>
<p class="MsoPlainText"> -> peachesTogether = peachesAllan +
peachesJake</p>
<p class="MsoPlainText">)</p>
<p class="MsoPlainText">}</p>
<p class="MsoPlainText"> </p>
<p class="MsoPlainText">, the resulting model x = 6 is reported
by the tool as follows:</p>
<p class="MsoPlainText"> </p>
<p class="MsoPlainText">Loading ...</p>
<p class="MsoPlainText">Preprocessing ...</p>
<p class="MsoPlainText">Constructing satisfying assignment for
the existential constants ...</p>
<p class="MsoPlainText">VALID</p>
<p class="MsoPlainText">Under the assignment:</p>
<p class="MsoPlainText">peachesTogether = 6</p>
<p class="MsoPlainText">27ms</p>
<p class="MsoNormal"> </p>
<p class="MsoNormal">Maybe the integration with Princess might
therefore be suitable for generating a valid model of an
integer arithmetic problem.</p>
<p class="MsoNormal"> </p>
<p class="MsoNormal">With regards,</p>
<p class="MsoNormal">Vit</p>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Hets-users mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Hets-users@informatik.uni-bremen.de">Hets-users@informatik.uni-bremen.de</a>
<a class="moz-txt-link-freetext" href="https://mailman.informatik.uni-bremen.de/mailman/listinfo/hets-users">https://mailman.informatik.uni-bremen.de/mailman/listinfo/hets-users</a>
</pre>
</blockquote>
<br>
</body>
</html>