Dear William,
What you are looking for is IKL.
https://www.ihmc.us/users/phayes/IKL/GUIDE/GUIDE.html
It introduces the “that” operator which exactly allows you to make statements about propositions.
Regards
Matthew West
--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info/
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CALuUwtD5R%2Boc6ZTMUbYDb4a-tgN%2BtrbiW%2Bbyk7BydpWHYg9XnA%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/02e401d7c516%241e2fa3f0%245a8eebd0%24%40gmail.com.
William,
I have implemented your use cases in pure OWL in the spirit of my MELO project. The implementation consists of three tiny ontologies: the common inference ontology, General Smith ontology, and Sally ontology. The last two ontologies import the first one. Those ontologies are accessible from my MELO project in RDF/XML format: https://sourceforge.net/p/meloproject/code/ci/master/tree/OWL/examples/existing_things/ . Here I describe those ontologies in Manchester syntax.
The common inference ontology just states that all things in the range of is_in property are existing things:
ObjectProperty: is_in
Range: existing_thing
Class: existing_thing
Individual: US_Army
General Smith ontology states that General Smith is in the US Army:
Individual: General_Smith
Facts: is_in US_Army
The Sally ontology describes what Sally thinks:
Individual: John
Facts: is_in US_Army
To test the use cases:
-- download the three ontologies to a local folder;
-- open the second or the third ontology in Protege;
-- run a reasoner, and you will see the inference: US_Army is an existing_thing.
Note that US_Army is an “elevated” thing in both cases.
Cheers,
Igor
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CALuUwtD2AsA_cdPcJSOkcwYuk1uD1prKM2nHQZhfTQOtFQVX6w%40mail.gmail.com.
Dear William,
Well, I would not go that far. There is a way to say much the same thing using possible worlds.
For a statement such as “Peter believes that John loves Mary.”
This gets transposed to:
“There is a possible world X in which John loves Mary.”
“Peter believes possible world X is the actual world.”
Of course you have to admit possible worlds to make that move.
--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info/
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CALuUwtD5R%2Boc6ZTMUbYDb4a-tgN%2BtrbiW%2Bbyk7BydpWHYg9XnA%40mail.gmail.com.
--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info/
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/02e401d7c516%241e2fa3f0%245a8eebd0%24%40gmail.com.
--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info/
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CALuUwtD2AsA_cdPcJSOkcwYuk1uD1prKM2nHQZhfTQOtFQVX6w%40mail.gmail.com.
--
William,About your zero question "Is there a formal language that enables these kinds of inferences?"First of all, we need to write sentences themselves and then look for derivation possibilities."necessary" and, "thinks" may be a special kind of concept (class) and relation of(to) a sentence
and to get statement itself as an entity we have in RDF a reification.
But I am not sure about derivation rules there. Using reification in OWL2 may give some derivations if we can axiomatize "necessary" and, "thinks" in DL fully.
And a little bit about your "first question: does this criterion for the adequacy of a translation seem reasonable? "From my point of view, unfortunately, in general adequacy of translation from human language to formal language may be checked only by human.
For example if we have some CNL (like ACE) and we have hand-written compiler like APE to translate to OWL2 or TPTP, your criteria would be for the author a conclusion: I have done compiler well hence WF-criteria of course satisfied. As we have no possibility to check it:-)
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROTeSqVUg72-ZZctvuqR5Z1cfZA5FF67Uaovh7WFDqHTxg%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CALuUwtAjDWKEbQ2xCY1n6Ky7n%3DX00sYoGTyRf9gyvg%2BBjQmUTw%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROTt9ASdi9JWm-7Xxx4wXEJmaEu33HDJOaRK67fVCMrwxQ%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/4b725c84-d7a1-4bd3-fd6c-2336a8f91607%40iks.cs.ovgu.de.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROQhCmNgB_LUTNp7wg%2BctU1ZfPh5pAKv%3DqcZVLiSnLSt%3DA%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/d3dbf3b4-bc6e-563f-f901-4082db60a61a%40iks.cs.ovgu.de.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxRORM5qFwuNWqfcuJrKP2Zi9M%2Bx3MMqgs-jracfg4wMMDDw%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/f53b7411-4d08-ccf0-d72c-46dd70490efb%40iks.cs.ovgu.de.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROTA8CFtCzT%2B-3Od61ChmNcT9cMfo3mQ9OFE5%2B8dYCmHkA%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/fefb669e-dbeb-3199-65a4-b94502cf433f%40iks.cs.ovgu.de.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROS1JMMis-XBsRbcHPbG%3Dg2Ay4DXU_N%3DaYXO9a0OUQLhQA%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/4310f57f-5421-d00c-e4db-243d2738011a%40iks.cs.ovgu.de.
Alex,
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/4310f57f-5421-d00c-e4db-243d2738011a%40iks.cs.ovgu.de.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROQ-NT%3DSae0B0xY8pWswEqM7-kaVy186qtkkgCDD%3DgQYNw%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/6e8267e2-5629-f783-b8da-f057da5633b0%40iks.cs.ovgu.de.
Till,
"semantically, Possible is just a predicate on {T,F}" for me this proposition is very very doubtable.
of course, your *intended* predicate Possible is not just
a predicate on {T,F}.
However, in standard HOL (see [1]), Possible would have type
Possible : o -> o
and in standard HOL, the semantics of o -> o is the function space {T,F} -> {T,F}. This follows from
"By a standard model, we mean a family of
domains, one for each type-symbol, as follows: D_\iota is
an arbitrary set of elements called inviduals, D_o ist the
set consisting of two truth values, T and F, and
D_{\beta->\alpha} is the set of all functions defined
over D_\beta with values in D_\alpha." [1], p.83, where in
the original, instead of D_{\beta->\alpha},
the old-fashioned notation D_{\alpha\beta}
is used.
This shows that your
intended predicate Possible cannot be expressed in standard HOL as
an operator on formulas.
Best, Till
[1]
Leon Henkin: Completeness in the Theory of Types. The Journal of
Symbolic Logic Vol.
15, No. 2 (Jun., 1950), pp. 81-91
https://www.jstor.org/stable/2266967
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROSuH0oysLz_CJsPwBc3NCg4uY3mWpNYTdemJ6iy4TjaSw%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/a93ecc09-8a6d-a0f6-15c5-ec4c4c684975%40iks.cs.ovgu.de.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROTFJcW08qyOhkrjw8TqZD6HO2iDy_RVMJwFtkHvuDTpWg%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/c9ff994f-ad32-5a98-0705-7c1b08d686bb%40iks.cs.ovgu.de.
--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info/
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/6198ef47b030410ca6eb0320b7d83f4c%40bestweb.net.