From: Richard Waldinger <waldinger@AI.SRI.COM>
this uses the theorem prover snark (not isabelle) to access web pages
(not necessarily in OWL) and other sources to answer questions.
questions are phrased as conjectures; answers are extracted from
(sufficiently constructive) proofs:
in geographical question answering:
http://www.ai.sri.com/pubs/files/986.pdf
this appears in mark maybury's collection:
http://www.mitpressjournals.org/doi/abs/10.1162/089120105774321055
in biological question answering:
http://www.aifb.uni-karlsruhe.de/WBS/phi/RoW06/procs/waldinger.pdf
http://www.plosone.org/article/info:doi%2F10.1371%2Fjournal.pone.0000339
---richard
From: Cristiano Longo <cristiano.longo@tvblob.com>
Thank you Richard. Seems that OWL(expecially OWL DL) insists on SHIQ logic,
that belongs to the family of description logics. So the question becomes,
there is an implementation of SHIQ(or other DL logic) in isabelle?
If not, SHIQ semantic is expressed using the Set theory. So should be correct
to implements SHIQ logic in isabelle using set theory? (i think no).
Thank you in advance,
Cristiano Longo
Il Tuesday 11 December 2007 04:16:16 Richard Waldinger ha scritto:
From: Richard Waldinger <waldinger@AI.SRI.COM>
i don't know the answer to your question.
the work i was referring to uses full first-order logic, not OWL, for
the most part.
there is software (by daniel elenius) mapping OWL into the SNARK
flavor of first-order logic.
---richard
From: Cristiano Longo <cristiano.longo@tvblob.com>
Hi all, i'm lookig for some application of isabelle to the semantic web, and
ontologies, or viceversa some experiments to use semantic web features with
isabelle or some other prover.
Sorry for my english,
Cristiano Longo
Last updated: Nov 21 2024 at 12:39 UTC