- From: Dan Connolly <connolly@w3.org>
- Date: Thu, 25 Sep 2003 11:18:18 -0500
- To: Jos De_Roo <jos.deroo@agfa.com>, Pat Hayes <phayes@ai.uwf.edu>
- Cc: www-rdf-logic@w3.org
On Wed, 2003-09-24 at 18:41, Jos De_Roo wrote:
[...]
> Also triggered by your chump
> http://rdfig.xmlhack.com/2003/09/23/2003-09-23.html#1064349895.329315
> (which reminded me about what I read some years ago
> http://www.cs.gc.cuny.edu/~sartemov/publications/spinoza.ps)
<- http://www.cs.gc.cuny.edu/~sartemov/publ.html
I'm studying this stuff, but I don't see how it deals
with universal quantification. The basic inference
step that cwm uses is generalized modus ponens, e.g.
{ ?X a :Man } => { ?X a :Mortal }.
:socrates a :Man.
===========>
:socratese a :Mortal.
What's the analog in Artemov's LP?
> I'm not understanding how consistency can be proved -
> for inconsistency tests I can understand that the proof is a
> construction like {triples} => {{triples} inconsistentWith theory}
> where {} is more or less like box-ing but for consistency ???
Exhibiting a model is one (constructive?) way to prove consistency.
>
> --
> Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
--
Dan Connolly, W3C http://www.w3.org/People/Connolly/
Received on Thursday, 25 September 2003 12:18:19 UTC