subst in n3

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 

Received on Thursday, 8 January 2004 15:10:53 UTC