- From: Tim Berners-Lee <timbl@w3.org>
- Date: Thu, 8 Jan 2004 15:10:51 -0500
- To: Public W3C <www-archive@w3.org>
- Cc: Dan Connolly <connolly@w3.org>
DanCon { C setofall (V F) } <=> { this log:forall X. { X a C } <=> (X V
F).subst }.
timbl M setofall ( `x` { ?x :member W3C }).
DanCon my motivation for subst had much to do with figuring out how N3
works; e.g. variables and quoting levels.
timbl M setofall ( `x` { foo!log:semantics log:includes {?x :member W3C
}}).
DanCon motivation came from proof checking, probably.
DanCon the list of things that log:includes finds is another RFE that
I'm interested in, independently.
DanCon DanC: substitution is a concept that you're allowed to use
without explanation in logic papers
DanCon up to simultaneous substituion of N exprs for N vars in F.
DanCon (usually called theta, I think)
DanCon (and rho)
timbl ( "x" "1".literal { ?x p o }) subst { 1 p o }.
timbl ( "x" "foo"^uri { ?x p o }) subst { <foo> p o }.
timbl ( "x" "foo"^uriq { ?x p o }) subst { <foo> p o }.
timbl <foo> = <bar>
timbl ( "x" "bar"^uri { ?x p o }) subst { <foo> p o }.
timbl NOT ( "x" <bar> { ?x p o }) subst { <foo> p o }.
timbl hence ^uriq not ^uri
timbl Challenges:
timbl 1. Define eth .literal etc vocabulary once and for all -
arvbitrary chocei
timbl 2. Define the param paters for subst, substN etc -- arbitrary
choice
Received on Thursday, 8 January 2004 15:10:53 UTC