proofcheck for witch

gistfile1.txt

$ proofcheck --report http://josd.github.io/eye/reasoning/witch/witch-proof.n3

.. list-table:: Proof
   :widths: 2 70 20 20
   :header-rows: 1

   * - Step
     - Formula
     - Justification
     - Bindings
   * - 1
     - ...
     - parsing <witch.n3>
     - 
   * - 2
     - :DUCK a :FLOATS .
     - erasure from step 1
     - 
   * - 3
     - ...
     - parsing <witch.n3>
     - 
   * - 4
     - :DUCK :SAMEWEIGHT :GIRL .
     - erasure from step 3
     - 
   * - 5
     - ...
     - parsing <witch.n3>
     - 
   * - 6
     - @forAll :x_0, :x_1 . { :x_0 a witch:FLOATS; witch:SAMEWEIGHT :x_1 . } => {:x_1 a witch:FLOATS . } .
     - erasure from step 5
     - 
   * - 7
     - :GIRL a :FLOATS .
     - rule from step 6 applied to steps (2, 4)
     - {'x_0': u'<http://josd.github.io/eye/reasoning/witch#DUCK>', 'x_1': u'<http://josd.github.io/eye/reasoning/witch#GIRL>'}
   * - 8
     - ...
     - parsing <witch.n3>
     - 
   * - 9
     - @forAll :x_0 . { :x_0 a witch:FLOATS . } => {:x_0 a witch:ISMADEOFWOOD . } .
     - erasure from step 8
     - 
   * - 10
     - :GIRL a :ISMADEOFWOOD .
     - rule from step 9 applied to steps (7,)
     - {'x_0': u'<http://josd.github.io/eye/reasoning/witch#GIRL>'}
   * - 11
     - ...
     - parsing <witch.n3>
     - 
   * - 12
     - @forAll :x_0 . { :x_0 a witch:ISMADEOFWOOD . } => {:x_0 a witch:BURNS . } .
     - erasure from step 11
     - 
   * - 13
     - :GIRL a :BURNS .
     - rule from step 12 applied to steps (10,)
     - {'x_0': u'<http://josd.github.io/eye/reasoning/witch#GIRL>'}
   * - 14
     - ...
     - parsing <witch.n3>
     - 
   * - 15
     - :GIRL a :WOMAN .
     - erasure from step 14
     - 
   * - 16
     - ...
     - parsing <witch.n3>
     - 
   * - 17
     - @forAll :x_0 . { :x_0 a witch:BURNS, witch:WOMAN . } => {:x_0 a witch:WITCH . } .
     - erasure from step 16
     - 
   * - 18
     - :GIRL a :WITCH .
     - rule from step 17 applied to steps (13, 15)
     - {'x_0': u'<http://josd.github.io/eye/reasoning/witch#GIRL>'}
   * - 19
     - ...
     - parsing <witch-goal.n3>
     - 
   * - 20
     - @forAll :x_0 . { :x_0 a witch:WITCH . } => {:x_0 a witch:WITCH . } .
     - erasure from step 19
     - 
   * - 21
     - :GIRL a :WITCH .
     - rule from step 20 applied to steps (18,)
     - {'x_0': u'<http://josd.github.io/eye/reasoning/witch#GIRL>'}
   * - 22
     - :GIRL a :WITCH .
     - conjoining steps (21,)
     - 


Conclusion::

  @prefix : <http://josd.github.io/eye/reasoning/witch#> .
  
  :GIRL     a :WITCH .