From: Benjamin Grosof (bgrosof@MIT.EDU)
Date: 06/24/03
Hi folks,
Here are my notes from today's JC telecon: whose topics were rules roadmap
and explicit equality and semantics.
In-line'd below, and attached too for convenience.
Benjamin
% 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!)
________________________________________________________________________________________________
Prof. Benjamin Grosof
Web Technologies for E-Commerce, Business Policies, E-Contracting, Rules,
XML, Agents, Semantic Web Services
MIT Sloan School of Management, Information Technology group
http://ebusiness.mit.edu/bgrosof or http://www.mit.edu/~bgrosof
This archive was generated by hypermail 2.1.4 : 06/24/03 EST