- From: Wagner, G.R. <G.R.Wagner@tm.tue.nl>
- Date: Fri, 12 Oct 2001 09:32:26 +0200
- To: "'Pat Hayes'" <phayes@ai.uwf.edu>
- Cc: www-rdf-rules@w3.org
> > > I always liked the example that was given in the KIF > documentation > >> (KIF 3.0 Ref. Manual, > >> http://logic.stanford.edu/kif/Hypertext/node37.html): > >> > >> ... On the other hand, in some cases, replacing <<= by <= would be > >> semantically unacceptable. For instance, the rules > >> > >> (<<= (status-known ?x) (citizen ?x)) > >> (<<= (status-known ?x) (not (citizen ?x))) > >> > >> allow us to infer (status-known Joe) only if one of the sentences > >> > >> (citizen Joe), (not (citizen Joe)) > >> > >> can be inferred. Replacing the rules by implications would make > >> (status-known ?x) identically true." > > > >But according to classical (2-valued) logic, there is no difference > >here between these rules and the corresponding implications. > > Why not? The 2-valued status of the logic says nothing about how to > interpret *rules*. Notice that we can associate a model-theoretic semantics with rules in a natural way: an interpretation I satisfies a rule (is a model of it) if it satisfies its consequent whenever it satisfies its antecedcent. > >The sentence (status-known Joe) could also be inferred from the > >two rules alone, > > From the two implications, but not from the rules. In fact, strictly > speaking, nothing can be inferred *from* a rule, only *by* a rule. Yes, we can infer from a rule set: using the above definition of a model of a rule, we can define that a rule set R entails a sentence F if all models of R satisfy F (in logic programming we say that R entails F if all stable models of R satisfy F). > >since every classical (i.e. total and coherent) > >model of the two rules would satisfy it, simply because it would > >either satisfy (citizen Joe) or (not (citizen Joe)), and in both > >cases, as it satisfies both rules, it would also have to satisfy > >(status-known Joe). > > (I think you mean, as it satisfies *one of the* rules?). But merely > being satisfiable in a single interpretation is not sufficient to > trigger a rule. I think you confuse something here: Triggering a rule is a different (proof-procedural) thing than the model-theoretic semantics of rules. Again: Let M be a classical model of the two rules (that is, it satisfies their consequent if it satisfies their antecequent). Then either M satisfies (citizen Joe), in which case it has to satisfy (status-known Joe) because it satisfies the first rule, or it satisfies (not (citizen Joe)), in which case it has to satisfy (status-known Joe) because it also satisfies the second rule. So, the author of this text on KIF seems to make a mistake here. In fact, he unintentionally describes the behavior of rules in extended logic programs where "not" corresponds to the strong (monotonic) negation of partial logic, where models are partial and the "tertium non datur" (= law of the excluded middle) does not hold. -Gerd -------------------------------------------- Gerd Wagner Email: G.Wagner@tm.tue.nl http://tmitwww.tm.tue.nl/staff/gwagner Eindhoven University of Technology Faculty of Technology Management Department of Information & Technology P.O. Box 513 5600 MB Eindhoven Tel: (+31 40) 247 26 17 The Netherlands Fax: (+31 40) 243 26 12
Received on Friday, 12 October 2001 03:32:30 UTC