Re: [isabelle] Semantic Web

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.

On Dec 11, 2007, at 12:51 AM, Cristiano Longo wrote:

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:
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:
   this appears in mark maybury's collection:

in biological question answering: 0000339


On Dec 7, 2007, at 3:06 AM, Cristiano Longo wrote:
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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.