Re: log:Truth rule

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
> 
> 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 07:55:46 UTC