Re: log:Truth rule

On 27 Apr 2010, at 08:55, Story Henry wrote:

> 
> On 26 Apr 2010, at 23:52, jos.deroo@agfa.com wrote:
> 
>> Henry, good to see your running rule!
>> I tried to independently test it and indeed got what you wrote:
>> 
>> eye --nope henry.n3 --pass
>> starting 4 [msec cputime] 0 [msec walltime]
>> GET henry.n3
>> networking 0 [msec cputime] 4 [msec walltime]
>> #Processed by $Id: euler.yap 3401 2010-04-26 14:27:18Z josd $
>> 
>> @prefix log: <http://www.w3.org/2000/10/swap/log#>.
>> @prefix : <#>.
>> @prefix var: <http://localhost/var#>.
>> @prefix e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>.
>> @prefix r: <http://www.w3.org/2000/10/swap/reason#>.
>> @prefix n3: <http://www.w3.org/2004/06/rei#>.
>> 
>> {:joe :loves :jane. :jane :loves :jack} a log:Truth.
>> :joe :loves :jane.
>> :jane :loves :jack.
>> 
>> 
>> Have to think about how close this is with Tarksi's truth..
>> All I know at this moment is:
>> 
>> whenever, in a sentence, we wish to say something
>> about a certain thing, we have to use, in this
>> sentence, not the thing itself but its name or
>> designation -- Alfred Tarski
> 
> I found the following interesting quite in the article "Truth and Meaning" by 
> Gabriel Segal that appeared in the "Oxford Handbook of the Philosophy of Language"
> http://ukcatalogue.oup.com/product/9780199259410.do
> 
> (calling this 1000 page volume a handbook is a very British understatement)
> 
> "Tarski's semantics came in the form of truth definitions (or "T-theories"). A
> truth definition for a particular language, L, is the definition of a predicate, 
> say "is T", that is true of all and only the true sentences of L."
> 
> This sentence comes with the interesting footnote
> 
> "Contemporary theorists are using "is T" to instantiate the predicate and I will continue
> the tradition, though Tarski used either "is true" or "is a member of the class Tr".
> 
> clearly Tarski meant the class log:Truth :-)
> 
>> So I believe that all those "certain things" are
>> rdfs resources, wether they be literal values
>> or URI referenced things, the names are just
>> different designations.
>> 
>> 
>> Tarski's famous T-schema
>> 
>> T: "P" is true iff P
>> 
>> where
>> 
>> "P" is a statement in the object language
>> 
>> P is a statement in the meta-language

Ok, I think I see where you may be getting at.

That is we think of what is inside the { } brackets as the meaning of the sentence, 
(the set of possible worlds in which the sentences inside the brackets are true), then
"is True" is perhaps the wrong predicate, as far as it does not seem to be getting us from
meta language to object language but from meaning to object language. Ie, instead of 
having a relation that goes from sentences to meaning, we have something that goes from 
meaning to fact. (what is in my graph is a fact for the person believing the graph).

In that case log:Truth is more like a modal concept, and really means "is Actual". 
So from the perspective of any graph, what is stated therein is something that is 
thought to be True in the actual world, and so which could have direct behavioural 
implications. Being Actual is an indexical into possible worlds, just like 'here' 
is an indexical in space, and 'now' in time, and 'I' for the subject.

So perhaps { jack loves jane } a log:Actual is what we want (interesting how the word
Act appears in Actual)




>> 
>> which lets us finitely define truth in an uninterpreted
>> object language given an already understood meta-language.
>> 
>> -- http://computationaltruth.net/blog/logic_and_language/
>> 
> 
> The logic that ties this together with N3 is I believe Guha's 
> "Contexts: a Formalisation and Some Applications"
> http://www-formal.stanford.edu/guha/
> 
> where he shows quite clearly how we can interpret statements in a context. That is what
> the N3 lifting rules are ( http://blogs.sun.com/bblfish/date/20060404 ). Usually we apply a 
> simple truth theory in RDF land, ie, we interpret what was is said in a context
> to be in the same language (RDF) as what is outside the context. But sometimes we may need to 
> do weird translations, say if we know that someone uses the RDF word for food:Cheese whenever they
> mean clothing:Shoe. In which case we may need to define a specific log:TruthForJoe .
> 
> 
>> Anyhow, thanks a lot and keep up the good work!
> 
> Thanks, I'll be trying the same rules I am putting together on euler soon.... keep tuned.
> 
> Henry
> 
>> 
>> Jos
>> 
>> 
>> Kind regards,
>> 
>> Jos De Roo | Agfa HealthCare
>> Senior Researcher | HE/Advanced Clinical Applications Research
>> T  +32 3444 7618
>> http://www.agfa.com/w3c/jdroo/
>> 
>> Quadrat NV, Kortrijksesteenweg 157, 9830 Sint-Martens-Latem, Belgium
>> http://www.agfa.com/healthcare
>> 
>> 
>> 
>> 
>> Story Henry <henry.story@bblfish.net> 
>> Sent by: public-cwm-talk-request@w3.org
>> 04/26/2010 09:38 PM
>> 
>> To
>> public-cwm-talk@w3.org
>> cc
>> 
>> Subject
>> log:Truth rule
>> 
>> 
>> 
>> 
>> 
>> 
>> 
>> I wrote out the following rule
>> 
>> 
>> ---------✁---------✂-----------------✃-----------------------
>> $  cat test.n3
>> 
>> @prefix log: <http://www.w3.org/2000/10/swap/log#> .
>> @prefix : <#> .
>> 
>> @forAll :G, :s, :r, :o .
>> {  :G a log:Truth;
>>     log:includes {:s :r :o. } } => { :s :r :o. } .
>> 
>> { :joe :loves :jane .
>> :jane :loves :jack. } a log:Truth . 
>> ---------✁---------✂-----------------✃-----------------------
>> 
>> 
>> ( Thanks to DanC for pointing out the importance of @forAll here )
>> This works
>> 
>> ---------✁---------✂-----------------✃-----------------------
>> $ cwm  test.n3 --think 
>> #Processed by Id: cwm.py,v 1.197 2007/12/13 15:38:39 syosi Exp 
>> #[snip]
>> 
>>    @prefix : <#> .
>>   @prefix log: <http://www.w3.org/2000/10/swap/log#> .
>> 
>>    @forAll :G,
>>               :o,
>>               :r,
>>               :s .
>> 
>>   :jane     :loves :jack .
>> 
>>   :joe     :loves :jane .
>>   {
>>       :jane     :loves :jack .
>>       :joe     :loves :jane .
>> 
>>       }     a log:Truth .
>>   {
>>       :G     a log:Truth;
>>            log:includes {:s     :r :o .
>>           } .
>> 
>>       }     log:implies {:s     :r :o .
>>       } .
>> ---------✁---------✂-----------------✃-----------------------
>> 
>> 
>> Ie we get :jane :loves :jack as a fact.
>> This is close to Tarski's definition of truth, so I think we could add 
>> this to 
>> the log: rules no?
>> 
>> As a side note, I found that the same command with '--mode=rse' does not 
>> work. It gives the error. Not sure if --mode=rse is still needed
>> 
>> ---------✁---------✂-----------------✃-----------------------
>> $ cwm  --mode=rse test.n3 --think 
>> #Processed by Id: cwm.py,v 1.197 2007/12/13 15:38:39 syosi Exp 
>>       #    using base 
>> file:///Users/hjs/Programming/FoafSSL/foafssl-java/papers/spot2009/n3/test.n3
>> 
>>       Traceback (most recent call last):
>> File "/Users/hjs/Programming/w3.org/2000/10/swap/cwm.py", line 750, in 
>> <module>
>>   doCommand()
>> File "/Users/hjs/Programming/w3.org/2000/10/swap/cwm.py", line 617, in 
>> doCommand
>>   think(workingContext, mode=option_flags["think"])
>> File "/Users/hjs/Programming/w3.org/2000/10/swap/query.py", line 89, in 
>> think
>>   return InferenceTask(knowledgeBase, ruleFormula, mode=mode, why=why, 
>> repeat=1).run()
>> File "/Users/hjs/Programming/w3.org/2000/10/swap/query.py", line 184, in 
>> run
>>   return self.runBrilliant()
>> File "/Users/hjs/Programming/w3.org/2000/10/swap/query.py", line 208, in 
>> runBrilliant
>>   total = scheduler.run(int.__add__)
>> File "/Users/hjs/Programming/w3.org/2000/10/swap/query.py", line 1964, 
>> in run
>>   retVal = self.next()
>> File "/Users/hjs/Programming/w3.org/2000/10/swap/query.py", line 1958, 
>> in next
>>   return retVal.thunk()
>> File "/Users/hjs/Programming/w3.org/2000/10/swap/query.py", line 160, in 
>> addRule
>>   return Rule(task, subj, obj, statement, variables).once()
>> File "/Users/hjs/Programming/w3.org/2000/10/swap/query.py", line 474, in 
>> once
>>   total = query.resolve()
>> File "/Users/hjs/Programming/w3.org/2000/10/swap/query.py", line 804, in 
>> resolve
>>   k = self.matchFormula(self.statements, self.variables, 
>> self._existentialVariables)
>> File "/Users/hjs/Programming/w3.org/2000/10/swap/query.py", line 975, in 
>> matchFormula
>>   nbs = item.doIncludes(queue, existentials, variables, bindings)
>> File "/Users/hjs/Programming/w3.org/2000/10/swap/query.py", line 1505, 
>> in doIncludes
>>   unmatched=more_unmatched, mode=item.query.mode):
>> File "/Users/hjs/Programming/w3.org/2000/10/swap/query.py", line 1417, 
>> in setup
>>   schema = pred.dereference(mode, self.query.workingContext)
>> AttributeError: 'AnonymousUniversal' object has no attribute 'dereference'
>> ---------✁---------✂-----------------✃-----------------------
>> 
>> But the following works, but I am not sure if it is going to do the right 
>> thing.
>> 
>> ---------✁---------✂-----------------✃-----------------------
>> hjs@bblfish-2:2$ cwm  test.n3 --think  --mode=rse
>> #Processed by Id: cwm.py,v 1.197 2007/12/13 15:38:39 syosi Exp 
>>       #    using base 
>> file:///Users/hjs/Programming/FoafSSL/foafssl-java/papers/spot2009/n3/test.n3
>> 
>> 
>> #  Notation3 generation by
>> #       notation3.py,v 1.200 2007/12/11 21:18:08 syosi Exp
>> 
>> #   Base was: 
>> file:///Users/hjs/Programming/FoafSSL/foafssl-java/papers/spot2009/n3/test.n3
>> 
>>    @prefix : <#> .
>>   @prefix log: <http://www.w3.org/2000/10/swap/log#> .
>> 
>>    @forAll :G,
>>               :o,
>>               :r,
>>               :s .
>> 
>>   :jane     :loves :jack .
>> 
>>   :joe     :loves :jane .
>>   {
>>       :jane     :loves :jack .
>>       :joe     :loves :jane .
>> 
>>       }     a log:Truth .
>>   {
>>       :G     a log:Truth;
>>            log:includes {:s     :r :o .
>>           } .
>> 
>>       }     log:implies {:s     :r :o .
>>       } .
>> ---------✁---------✂-----------------✃-----------------------
>> 
>> 
>> Henry
>> 
>> 
>> 
>> 
>> 
>> 
>> 
>

Received on Tuesday, 27 April 2010 08:26:59 UTC