[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [List Home]
Subject: monadic predicate calculus (was: Re: [xdi] Rough notes ondecidability/semantic reasoning thoughts I expressed during the telecontoday)
Dear Bill, dear All,
Thank you Bill for posting your proposal. I've had some thoughts on
it, which I report below. Obviously feel free to correct me if I get
wrong somewhere!Main issues is that there are limitations in monadic
predicate calculus and we need to evaluate whether they are acceptable
or not for the goals we want to achieve with XDI.
Our challenge is to turn XDI into 'something' which can be used for
'reasoning' (broadest term). This has actually two subchallenges:
1) identify which kind of logic we want to target
2) find the correct XDI syntax for the various constructs
Proposal is that 1) can be identified with monadic predicate calculus
(http://en.wikipedia.org/wiki/Monadic_predicate_calculus). Therefore,
if this is our choice, we will only need to identify the correct XDI
constructs and their syntax to use, and prove that all the resulting
productions can be expressed within monadic predicate calculus.
But, before going on this way, let's investigate some implications
that come from restricting XDI to monadic predicates calculus.
Monadic predicate calculus extends propositional calculus, and was
known in forms of a collection of "syllogisms" since Aristotle. Till
recently (late 19th century, when logic of relations was introduced)
it was the sole form of logical calculus!
Here is a quick schema I have drawn to roughly illustrate a comparison
of various forms of logical calculus (see also attached image which is
indeed much more clear):
<-- decidable
--> | <-- undecidable -->
propositional calculus < monadic predicate calculus <
description logic < first order logic ...
<-- no nested quantifiers in normal form --> | <--
quantifiers can nest usefully -->
Drawbacks of monadic predicate calculus are that it "severely
restricts what can be expressed..." (wikipedia) and obviously what can
be inferred.
To understand why, here is an example.
In DL I can express the fact that there is a class of individuals that
have human parents, and, given facts such as =bob is a human, I can
infer that =bob's father is a human too:
[1] humanChild={x|for each y parent(x,y) -> human(y)} AXIOM
[2] humanChild(=bob), parent(=bob,=nigel) ==> human(=nigel) FACTS
NOTE: I have used parent(x,y) whereas in OWL they would reccomend
hasParent(x,y), to stress the fact that it is a property not a class;
but let's use a syntax close to the desired one for XDI :-)
However in monadic predicate calculus:
- I cannot define class humanChild, as there is no way to express the
relation parent(x,y)
- by substituting parent(x,y) with x_parent(y) ("Every XDI non $
predicate for form $S/$P/$O is a monadic predicate expression of the
form $S$P($O)"):
I can express that all bob's parents are humans: for each y
=bob_parent(y)->human(y) AXIOM
I can express that bob's parent is nigel and infer that nigel is a
human =bob_parent(=nigel) ==> human(=nigel) FACT
As you see, we have now a very specific predicate =bob_parent. To
achieve inferences with a different individual than =bob, say =peter,
I should have a different predicate =peter_parent and one more axiom
=peter_parent(y)->human(y). This is costly, because our reasoner
cannot generalize the predicates =bob_parent, =peter_parent, ...
To see what we are missing, for example, assume that you have a fact
saying that =spike.dog (a fellow of =tom.cat and =jerry.mouse in the
famous cartoon series) is not a human being. Using axiom [1] then you
realize that none of spike's child can be a humanChild:
NOT human(=spike.dog), parent(x,=spike.dog) ==> !humanChild(x)
but this realization cannot be achieved in terms of monadic predicate
calculus as there is no such a predicate as parent(x,y) but only
predicates =const_parent where =const is a fixed term (=bob, =peter,
etc.)
For example, from axioms like
=bob_parent(x)->human(x) AXIOM
=peter_parent(x)->human(x) AXIOM
you can infer that neither =bob nor =peter have =spike.dog as parent,
however this is much weaker than saying that there is a whole class of
individuals (humanChild) which cannot be children of =spike.dog.
Summarizing, what we need to assess: could this loss be acceptable for
XDI, or, in aiming at keeping things so simple, are we paying a too
high price that we risk to loose too much expressivity and inference
power?
Looking forward to hear your comments..
Thank you,
Giovanni
Def. Quota "Barnhill, William [USA]" <barnhill_william@bah.com>:
> Could XDI be decidable?
> Looking at it one way XDI can't be decidable without resolving the
> issue of XRI being usable as both a role and a concept.
> This is true, if we say XDI has n-ary predicates where n > 1,
> predicates that take 2 or more arguments.
> For example the $p in $s/$p/$o is a binary predicate, i.e. $p($s,$o)
>
> But...
> .. Every XDI $ predicate is a form of some kind of $is$a expression
> or a negation of such an expression
> .. Every $is$a negation is a $is$a of the complement of the object
> .. Every $is$a statement can be viewed as a monadic predicate for
> set membership of the object, essentially the
> object is the predicate
> .. Every XDI non $ predicate for form $S/$P/$O is a monadic
> predicate expression of the form $S$P($O)
> .. Every one of the monadic predicates above is a test for set
> membership, which matched XDI model because we've said it is based
> on set membership
> .. Essentially this turns XDI into a monadic predicate calculus
> .. As a result I propose we can say XDI is decidable
>
> Need a proof from me and Giovanni and I need to get with Giovanni
> and discuss how difficult this proof would be. There are existing
> proofs for a monadic predicate calculus being decidable, so we would
> I think only need to prove that XDI was a monadic predicate calculus
> and decidability would follow.
>
> Why us decidability important/useful? Because it's necessary to do
> reasoning that's guaranteed to complete without hanging, and
> complete in a usable time frame.
>
> Why is semantic reasoning useful?
> http://videolectures.net/eswc08_blanco_sr/
> http://www.ibm.com/developerworks/web/library/wa-semweb/
> http://encyclopedia.jrank.org/articles/pages/6898/Semantic-Web.html
> http://www.semanticoverflow.com/questions/74/what-are-the-benefits-of-the-semantic-web-to-publishers
>
> In short:
> .. You can mine your data for new knowledge much more efficiently
> and garner knowledge you couldn't without reasoning
> .. You can automate data mediation from one data structure to
> another (e.g. PDX Person to FOAF Person)
> .. You can easily add metadata to your data, or extend your data,
> without breaking or rewriting existing data processing
> .. Your search, visualization, and reporting tools now can present
> you with the needles of knowledge that you need, rather than
> haystacks of raw data you need to sift through - saving you time,
> money, and manpower.
>
> "I'll believe it when I see it, who's actually using this semantic
> stuff now?", I've heard that in many forms many times over the last
> year, but...
> .. Netflix
> .. Google
> .. Twitter
> .. US Government
> .. Best Buy
> .. and the number is growing (see this for some use cases:
> http://www.scientificamerican.com/article.cfm?id=semantic-web-in-actio)
>
> From the third article above, the ways semantic reasoning can be used:
> * Consistency - determine if the model is consistent. For example,
> presents an OWL model containing the facts: (a) cows are vegetarian,
> (b) sheep are animals, and (c) a 'mad cow' is one that has eaten
> sheep brain. From these facts a computational reasoning engine can
> infer that 'mad cows' are inconsistent since any cow eating sheep
> violates (a). The following (incomplete, but informative) OWL
> snippets help illustrate some salient issues. Informally, note the
> description of mad_cow (line 1). Note that mad_cow is an
> intersection class (line 4) defined as any cow (line 5) that has a
> property 'eats' (line 6) such that the range of that property (i.e.
> what it eats) is a part_of a sheep (lines 11, 13) and that part is a
> 'brain' (line 16). Below note that the 'sheep' class is defined as
> subclass of 'animal' while 'cow' is a subclass of 'vegetarian'.
> * Subsumption - infer knowledge structure, mostly hierarchy; the
> notion of one artifact being more general than another. For example,
> presents a model incorporating the notions (a) 'drivers drive
> vehicles', (b) 'bus drivers drive buses', and (b) a bus is a
> vehicle, and subsumption reasoning allows the inference that 'bus
> drivers are drivers' (since 'vehicle' is more general than 'bus').
> * Equivalence - determine if classes in the model denote the same
> set of instances
> * Instantiation - determine if an individual is an instance of a
> given Class. This is also known as 'classification' - that is,
> determine the instance of a given Class.
> * Retrieval - determine the set of individuals that instantiate a
> given Class
>
>
>
----------------------------------------------------------------
Invito da parte dell'Ateneo:
Il tuo futuro e quello della Ricerca Scientifica hanno bisogno del
tuo aiuto. Dona il 5 x mille all'Universita' di Roma Tor Vergata
codice fiscale: 80213750583 http://5x1000.uniroma2.it
different kinds of logical calculus.png
[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [List Home]
