Created
November 5, 2019 00:12
-
-
Save josd/0602211c0a73bbbccb16d5f7f3c6601f to your computer and use it in GitHub Desktop.
proofcheck for witch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
$ 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 . |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment