% notes from JC telecon 6/24/03 % by Benjamin Grosof agenda planned: - update and status check on roadmap for V1 - discussion on explicit equality in relation to semantics participants: Michael Dean Benjamin Grosof Ian Horrocks Sandro Hawke Said Tabet Ora Lassila Stefan Decker Peter Patel-Schneider Gerd Wagner o Update and status check on roadmap: Benj: let's try to move into a mode wrt roadmap with more definite schedules and make some decisions, e.g., decide on timing for syntax, semantics, use cases and requirements. Mike: Yes. I have some suggestions, will post them. Also would like to get back to requirements and use cases. Benj: suggestion: please integrate your suggestions into the earlier roadmap document that I posted in 3 versions, and with your earlier roadmap suggestions posting from that time. Mike: OK, will plan to do that. Ian: does it make sense to move to a full set of documents (cf. WebOnt's set) immediately, or do some intermediate form that we can get some feedback on. E.g., would like to see a single strawman document on it, with roughing out of syntax, semantics, how it relates to OWL. Benj: how about we begin by merging, with a bit more coherence, the RuleML V0.8 Horn LP XML DTD and abstract syntax, and Horn LP semantics draft, that we already have, and add a bit on the story of how it relates to OWL Action item: Benj and Said volunteer to do a draft of that, have it ready for discussion at the 7/8 JC telecon (2 weeks from now) %%%% o explicit equality Benj initial presentation (verbal): motivation: overcome limitation of Unique Names Axiom (UNA) in Herbrand models only, esp. once we later introduce ability to specify negation and default reasoning -- to specify selective default distinctness - ex.: specify joe and joseph are equal, or two URI's are equal, but all other names (e.g., fred, sue) are distinct (not-equal) from these and from each other it (say, the predicate ee) can be axiomatized via: - ee is transitive and symmetric - there's substitutivity of equals, for every predicate and logical function: . need to state this as set of axioms (i.e., overall axiom schema(s)) need to dig up logic literature on how this is axiomatized for FOL and LP MIke: similar to sameIndividualAs in OWL Ian: can implicitly specify equality in OWL, e.g., via equivalence of cardinality-1 classes [There was then some more discussion] Benj: summarizing where we are after that discussion: no one has raised any obstacle to the plausibility of the following story: - we can introduce explicit equality into the Horn LP rule language, and it will pretty much correspond semantically to equality in OWL-DL - and then we can extend that to default distinctness, when negation-as-failure / defaults are introduced later into the rule language - but we need to do our homework to dig up relevant theoretical results from the logical KR literature Sandro: wrt possible objections to least Herbrand model semantics for Horn case: a use case that distinguishes it from behavior of Horn FOL Ian: are we designing (1) a rule extension to OWL/DAML+OIL (say OWL-DL) or designing (2) a rule language that is compatible/overlapping with OWL/DAML+OIL? Benj: (2). OWL-DL goes way beyond Horn. For (1), what we know how to do from fundamental previous research is simply to move to FOL. For (2), tho', can view it as an extension of roughly the Description Logic Programs or Description Horn Logic subset of OWL. There are lots of use cases for (2), more than for (1). (1) requires fundamental new research if it's anything other than FOL. Sandro: would like to be clearer wrt even the distinction between (1) and (2). Mike: objectives for a rules language that some have articulated include: - can we have a complex OWL class as RDF type, within a rule system? - can we kind of fill in the gaps in OWL-DL, e.g., property chaining? Ian: i.e., some hoping from us to get "a better OWL", tho' that may not be very realistic Benj: can approach this as follows: - permit rules in Horn FOL or Horn LP as well as ontology axioms in OWL-DL, then do inferencing in FOL or LP, then bring some of the conclusions from that back into OWL-DL - problem is that this is not well understood at a fundamental reasoning level Ian: e.g., should be straightforward to translate (OWL-)DL into a FOL theorem-prover, e.g., TPTP, e.g., using the CADE conference's competition's standard syntax - in preliminary experiments, a FOL theorem-prover can be reasonably efficient on DL axioms/tasks Benj: then query it for DL expressions as queries, or to test overall consistency/satisfiability Stefan and all: but this is not decidable Ora: would like developers when getting rules too to still have a choice about using OWL-Lite or OWL-DL Mike: how about we consider the computational processing model? Ian: i.e., "how would we build one" Mike: also, some test cases would help Peter: it will definitely help to get a written proposal document on this Ian: don't want to have two different semantics, e.g., one LP and one FOL Agenda: for next week, discussion of requirements and test cases - Mike volunteers to collect some for two weeks from now: discuss strawman document that Benjamin and Said will be drafting (others very welcome to help them!)