W3C home > Mailing lists > Public > public-cwm-bugs@w3.org > June 2006

cwm's proof checker trusts the statements of rules

From: Yosi Scharf <syosi@MIT.EDU>
Date: Thu, 29 Jun 2006 11:30:35 -0400
Message-ID: <44A3F21B.5030207@mit.edu>
To: public-cwm-bugs@w3.org
Running the following:

syosi@mr-burns:~/CVS-local/WWW/2000/10/swap/test/reason$ check /tmp/odd.pf
     @prefix :
<file:/home/syosi/CVS-local/WWW/2000/10/swap/test/reason/socrates.n3#> .
    @prefix log: <http://www.w3.org/2000/10/swap/log#> .

     @forAll :who .

    :socrates     a :Fish,
                :Man .
    {
        :who     a :Man .

        }     log:implies {:who     a :Mortal .
        } .



seems to have issues. See attached proof.


Yosi

#Processed by Id: cwm.py,v 1.185 2006/05/30 21:08:05 syosi Exp 
        #    using base foo:
        
#  Notation3 generation by
#       notation3.py,v 1.187 2006/01/13 14:48:54 syosi Exp

#   Base was: foo:
     @prefix : <http://www.w3.org/2000/10/swap/reason#> .
    @prefix log: <http://www.w3.org/2000/10/swap/log#> .
    @prefix n3: <http://www.w3.org/2004/06/rei#> .
    @prefix soc: <file:/home/syosi/CVS-local/WWW/2000/10/swap/test/reason/socrates.n3#> .
    
      [      a :Conjunction,
                    :Proof;
             :component  [
                 a :Inference;
                 :binding  [
                     :boundTo  [
                         n3:uri "file:/home/syosi/CVS-local/WWW/2000/10/swap/test/reason/socrates.n3#socrates" ];
                     :variable  [
                         n3:uri "file:/home/syosi/CVS-local/WWW/2000/10/swap/test/reason/socrates.n3#who" ] ];
                 :evidence  (
                 [
                         a :Extraction;
                         :because _:g17;
                         :gives {soc:socrates     a soc:Man .
                        } ] );
                 :rule  [
                     a :Extraction;
                     :because _:g17;
                     :gives { @forAll soc:who .
                    {
                        soc:who     a soc:Man .
                        
                        }     log:implies {soc:who     a soc:Fish .
                        } .
                    } ] ],
                    _:g17;
             :gives { @forAll soc:who .
            soc:socrates     a soc:Man,
                        soc:Fish .
            {
                soc:who     a soc:Man .
                
                }     log:implies {soc:who     a soc:Mortal .
                } .
            } ].
    
    _:g17     a :Parsing;
         :because  [
             a :CommandLine;
             :args "['/home/syosi/SWAP/cwm.py', '--n3=aeiou', 'socrates.n3', '--think', '--base=foo:', '--why']" ];
         :source <file:/home/syosi/CVS-local/WWW/2000/10/swap/test/reason/socrates.n3> .
    
#ENDS
Received on Thursday, 29 June 2006 15:31:02 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Tuesday, 8 January 2008 14:10:59 GMT