http://ontologforum.org/index.php?title=Blog:Formal_theory,_finite_model_and_DL_reasoner/Second_Statement&feed=atom&action=historyBlog:Formal theory, finite model and DL reasoner/Second Statement - Revision history2022-01-17T19:38:27ZRevision history for this page on the wikiMediaWiki 1.19.2http://ontologforum.org/index.php?title=Blog:Formal_theory,_finite_model_and_DL_reasoner/Second_Statement&diff=24627&oldid=prevAshkotin at 16:27, 19 February 20182018-02-19T16:27:02Z<p></p>
<table class='diff diff-contentalign-left'>
<col class='diff-marker' />
<col class='diff-content' />
<col class='diff-marker' />
<col class='diff-content' />
<tr valign='top'>
<td colspan='2' style="background-color: white; color:black;">← Older revision</td>
<td colspan='2' style="background-color: white; color:black;">Revision as of 16:27, 19 February 2018</td>
</tr><tr><td colspan="2" class="diff-lineno">Line 1:</td>
<td colspan="2" class="diff-lineno">Line 1:</td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins style="color: red; font-weight: bold; text-decoration: none;">Henson Graves STATEMENT:</ins></div></td></tr>
<tr><td class='diff-marker'> </td><td style="background: #eee; color:black; font-size: smaller;"></td><td class='diff-marker'> </td><td style="background: #eee; color:black; font-size: smaller;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background: #eee; color:black; font-size: smaller;"><div>Here are some subtopics of the overall problem of how to realize the axiom set-theory-interpretation paradigm in everyday practice.</div></td><td class='diff-marker'> </td><td style="background: #eee; color:black; font-size: smaller;"><div>Here are some subtopics of the overall problem of how to realize the axiom set-theory-interpretation paradigm in everyday practice.</div></td></tr>
</table>Ashkotinhttp://ontologforum.org/index.php?title=Blog:Formal_theory,_finite_model_and_DL_reasoner/Second_Statement&diff=24621&oldid=prevAshkotin at 12:40, 19 February 20182018-02-19T12:40:33Z<p></p>
<table class='diff diff-contentalign-left'>
<col class='diff-marker' />
<col class='diff-content' />
<col class='diff-marker' />
<col class='diff-content' />
<tr valign='top'>
<td colspan='2' style="background-color: white; color:black;">← Older revision</td>
<td colspan='2' style="background-color: white; color:black;">Revision as of 12:40, 19 February 2018</td>
</tr><tr><td colspan="2" class="diff-lineno">Line 1:</td>
<td colspan="2" class="diff-lineno">Line 1:</td></tr>
<tr><td class='diff-marker'>−</td><td style="background: #ffa; color:black; font-size: smaller;"><div><del class="diffchange diffchange-inline">HensonGraves:</del></div></td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div> </div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins class="diffchange diffchange-inline">Here are some subtopics of the overall problem of how to realize the axiom set-theory-interpretation paradigm in everyday practice.</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div> </div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins class="diffchange diffchange-inline">1. What is the tradeoff between KR languages in which classification is by sets or types which are terms vs those which classification is represented by predicates?</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div> </div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins class="diffchange diffchange-inline">2. What are the appropriate modular units for reuse?</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div> </div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins class="diffchange diffchange-inline">3. How can formal approaches best exploit graphics based modeling languages?</ins></div></td></tr>
<tr><td class='diff-marker'> </td><td style="background: #eee; color:black; font-size: smaller;"></td><td class='diff-marker'> </td><td style="background: #eee; color:black; font-size: smaller;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background: #eee; color:black; font-size: smaller;"><div>The paradigm that I am suggesting is exactly the same one that is in John's diagram. For this audience I will stick to logician's terminology. Engineers develop artifacts which are naturally axiom sets even if they don't always recognize it. The axiom sets generate a theory depending on the logic the axiom set is embedded in. The axiom sets are finitely presented. The theory generated by the axiom set are the conclusions which can be derived from the axioms in the logic. As any axiom set or theory there are natural definitions of a valid model of the theory generated by the axiom set. Depending on the axiom set there may possibly be both finite or infinite models. Following John's diagram there are two general kinds of models, the ones in the physical world and simulation models. To me what is important in both cases is not finiteness of the model but its constructivity. This requires a lot more discussion which I will not do here. Following the usual logic paradigm you expect the reasoning to be "true" in all valid models, at least when the theory is sound.</div></td><td class='diff-marker'> </td><td style="background: #eee; color:black; font-size: smaller;"><div>The paradigm that I am suggesting is exactly the same one that is in John's diagram. For this audience I will stick to logician's terminology. Engineers develop artifacts which are naturally axiom sets even if they don't always recognize it. The axiom sets generate a theory depending on the logic the axiom set is embedded in. The axiom sets are finitely presented. The theory generated by the axiom set are the conclusions which can be derived from the axioms in the logic. As any axiom set or theory there are natural definitions of a valid model of the theory generated by the axiom set. Depending on the axiom set there may possibly be both finite or infinite models. Following John's diagram there are two general kinds of models, the ones in the physical world and simulation models. To me what is important in both cases is not finiteness of the model but its constructivity. This requires a lot more discussion which I will not do here. Following the usual logic paradigm you expect the reasoning to be "true" in all valid models, at least when the theory is sound.</div></td></tr>
</table>Ashkotinhttp://ontologforum.org/index.php?title=Blog:Formal_theory,_finite_model_and_DL_reasoner/Second_Statement&diff=24530&oldid=prevAshkotin at 13:06, 7 February 20182018-02-07T13:06:28Z<p></p>
<table class='diff diff-contentalign-left'>
<col class='diff-marker' />
<col class='diff-content' />
<col class='diff-marker' />
<col class='diff-content' />
<tr valign='top'>
<td colspan='2' style="background-color: white; color:black;">← Older revision</td>
<td colspan='2' style="background-color: white; color:black;">Revision as of 13:06, 7 February 2018</td>
</tr><tr><td colspan="2" class="diff-lineno">Line 1:</td>
<td colspan="2" class="diff-lineno">Line 1:</td></tr>
<tr><td class='diff-marker'>−</td><td style="background: #ffa; color:black; font-size: smaller;"><div><del class="diffchange diffchange-inline">bla-bla</del></div></td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins class="diffchange diffchange-inline">HensonGraves:</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div> </div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins class="diffchange diffchange-inline">The paradigm that I am suggesting is exactly the same one that is in John's diagram. For this audience I will stick to logician's terminology. Engineers develop artifacts which are naturally axiom sets even if they don't always recognize it. The axiom sets generate a theory depending on the logic the axiom set is embedded in. The axiom sets are finitely presented. The theory generated by the axiom set are the conclusions which can be derived from the axioms in the logic. As any axiom set or theory there are natural definitions of a valid model of the theory generated by the axiom set. Depending on the axiom set there may possibly be both finite or infinite models. Following John's diagram there are two general kinds of models, the ones in the physical world and simulation models. To me what is important in both cases is not finiteness of the model but its constructivity. This requires a lot more discussion which I will not do here. Following the usual logic paradigm you expect the reasoning to be "true" in all valid models, at least when the theory is sound.</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div> </div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins class="diffchange diffchange-inline">For now only one more idea.</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div> </div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="background: #cfc; color:black; font-size: smaller;"><div><ins class="diffchange diffchange-inline">The axioms sets that engineers produce generally have a lot more valid models than the engineer intended. So a lot of practical engineering work is identifying the additional assumptions needed to constrain the valid models. One could view these additional assumptions as "context" for the axiom sets. That is in some domain all of these assumptions could be added automatically to a proof assistant (aka engineer's model development tool) without the axiom set developer even being aware of it. For example in the paper reference above we were modeling both the aircraft and its operational environment. For the axiom set to generate the 3D simulations that we produced we had to add an immense amount of assumptions about physics regarding aerodynamics, sensor performance etc.</ins></div></td></tr>
<tr><td class='diff-marker'> </td><td style="background: #eee; color:black; font-size: smaller;"><div>{{wl-publish: 2018-02-05 12:35:06 -0500 | Ashkotin }}</div></td><td class='diff-marker'> </td><td style="background: #eee; color:black; font-size: smaller;"><div>{{wl-publish: 2018-02-05 12:35:06 -0500 | Ashkotin }}</div></td></tr>
</table>Ashkotinhttp://ontologforum.org/index.php?title=Blog:Formal_theory,_finite_model_and_DL_reasoner/Second_Statement&diff=24523&oldid=prevAshkotin: Created page with "bla-bla {{wl-publish: 2018-02-05 12:35:06 -0500 | Ashkotin }} "2018-02-05T17:35:06Z<p>Created page with "bla-bla {{wl-publish: 2018-02-05 12:35:06 -0500 | Ashkotin }} "</p>
<p><b>New page</b></p><div>bla-bla<br />
{{wl-publish: 2018-02-05 12:35:06 -0500 | Ashkotin }}</div>Ashkotin