- From: Dan Brickley <danbri@w3.org>
- Date: Mon, 9 Apr 2001 16:29:08 -0400 (EDT)
- To: pat hayes <phayes@ai.uwf.edu>
- cc: <jos.deroo.jd@belgium.agfa.com>, <www-rdf-logic@w3.org>
On Mon, 9 Apr 2001, pat hayes wrote:
> >it's OK now
> >the URI is http://www.w3.org/2001/02/rdfig-f2f/formalSys
> >(and it would be nice to speak that way)
>
> Maybe this was intended, but that URL requires a password. Maybe you
> guys shouldnt be discussing this on a public email forum, or
> something?
Odd, I made the resource world readable. Maybe it didn't propagate to all
the w3.org mirrors or something. Or it could be the RDF-based access
control system ;-)
Anyway,
http://www.w3.org/2001/02/rdfig-f2f/formalSys content negotiates to
http://www.w3.org/2001/02/rdfig-f2f/formalSys.txt copied below for info.
Dan
----------------------------------------------------------------------
What 'model' means in the formal systems literature
(for details, see http://www.w3.org/XML/9711theory/
esp http://www.w3.org/XML/9711theory/FormalSystem)
term ::= constantI
| variable
| constantF(term, term, ...)
atom ::= constantP(term, term, ...)
formula ::= atom
| forumula AND formula
| formula OR formula
| NOT fomula
| FORALL(variable) formula
| THEREEXISTS(variable) formula
An _interpretation_ is
-- a set of _objects_, often called the domain, D
-- a mapping of constantI's to D
-- a mapping of constantF's to (DxDxDx...)->D i.e. functions over D
-- a mapping of constantP's to DxDxDxDx... i.e. relations over D
e.g.
D = { objDan, objTim, objUs }
constantI(Dan) = objDan
constantI(Tim) = objTim
constantI(Us) = objUs, i.e. ... the set of folks in the room...
constantP(in) = {<objDan,objUs>, <objTim, objUs>}
so... in(Dan, Us) is interpreted as true.
a formula is satisfyable if there are _objects_ from D
that (to paraphrase) can be plugged into the formula in the
right places to make it work out.
and interpretation is a _model_ for a set of formulas
if each of the formulas is satisfyable in that interpretation.
folks specify logics by specifying what constitutes a model;
i.e. which formulas should be regarded as true.
$Log: formalSys.txt,v $
Revision 1.2 2001/04/09 16:34:49 connolly
fixed a few typos and
refined the 'see also' link
----------------------------------------------------------------------
Received on Monday, 9 April 2001 16:29:10 UTC