| # Test of interactions of qualifiers with log:includes |
| # |
| # $Id: quantifiers.n3,v 1.1 2006-12-09 20:39:25 andy_seaborne Exp $ |
| # |
| # Usage: cwm quantifiers.n3 -think -purge |
| # Should give 18 successes and no failures. |
| # |
| |
| @prefix log: <http://www.w3.org/2000/10/swap/log#>. |
| |
| @prefix : <#>. |
| @prefix qu: <#>. |
| |
| |
| # |
| # Basically, forall x G(x) implies G(x) which implies forSome X G(x). |
| # log:includes should allow the stronger statement to "include" the weaker one. |
| # |
| {{ :foo :bar :baz } log:includes { this log:forSome :foo. :foo :bar :baz }} |
| log:implies { :testa2 a :success }. # Originally failed |
| |
| |
| |
| {{ this log:forSome :foo. :foo :bar :baz } log:includes {this log:forSome :foo. :foo :bar :baz }} |
| log:implies { :testb2 a :success }. |
| |
| {{ this log:forAll :foo. :foo :bar :baz } log:includes {this log:forSome :foo. :foo :bar :baz }} |
| log:implies { :testc2 a :success }. # Originally failed |
| |
| |
| |
| {{ :foo :bar :baz } log:includes { :foo :bar :baz }} |
| log:implies { :testa1 a :success }. |
| |
| {{ this log:forSome :foo. :foo :bar :baz } log:includes { :foo :bar :baz }} |
| log:implies { :testb1 a :FAILURE }. # Originally failed, STILL FAILS. |
| |
| {{ this log:forAll :foo. :foo :bar :baz } log:includes { :foo :bar :baz }} |
| log:implies { :testc1 a :success }. |
| |
| |
| |
| {{ :foo :bar :baz } log:includes {this log:forAll :foo. :foo :bar :baz }} |
| log:implies { :testa3 a :FAILURE }. |
| |
| {{ this log:forSome :foo. :foo :bar :baz } log:includes {this log:forAll :foo. :foo :bar :baz }} |
| log:implies { :testb3 a :FAILURE }. |
| |
| {{ this log:forAll :foo. :foo :bar :baz } log:includes {this log:forAll :foo. :foo :bar :baz }} |
| log:implies { :testc3 a :success }. |
| |
| |
| # Negative tests: |
| |
| |
| |
| {{ :foo :bar :baz } log:notIncludes { this log:forSome :foo. :foo :bar :baz }} |
| log:implies { :testa2n a :FAILURE }.# Originally failed |
| |
| {{ this log:forSome :foo. :foo :bar :baz } log:notIncludes {this log:forSome :foo. :foo :bar :baz }} |
| log:implies { :testb2n a :FAILURE }. |
| |
| {{ this log:forAll :foo. :foo :bar :baz } log:notIncludes {this log:forSome :foo. :foo :bar :baz }} |
| log:implies { :testc2n a :FAILURE }. # Originally failed |
| |
| |
| |
| {{ :foo :bar :baz } log:notIncludes { :foo :bar :baz }} |
| log:implies { :testa1n a :FAILURE }. |
| |
| {{ this log:forSome :foo. :foo :bar :baz } log:notIncludes { :foo :bar :baz }} |
| log:implies { :testb1n a :success }. |
| |
| {{ this log:forAll :foo. :foo :bar :baz } log:notIncludes { :foo :bar :baz }} |
| log:implies { :testc1n a :FAILURE }. |
| |
| |
| |
| {{ :foo :bar :baz } log:notIncludes {this log:forAll :foo. :foo :bar :baz }} |
| log:implies { :testa3n a :success }. |
| |
| {{ this log:forSome :foo. :foo :bar :baz } log:notIncludes {this log:forAll :foo. :foo :bar :baz }} |
| log:implies { :testb3n a :success }. |
| |
| {{ this log:forAll :foo. :foo :bar :baz } log:notIncludes {this log:forAll :foo. :foo :bar :baz }} |
| log:implies { :testc3n a :FAILURE }. |
| |
| |
| |
| ######################## Versions with different identifiers: |
| |
| |
| {{ :fee :bar :baz } log:includes { this log:forSome :foo. :foo :bar :baz }} |
| log:implies { :testa2d a :success }. # Originally failed |
| |
| {{ this log:forSome :fee. :fee :bar :baz } log:includes {this log:forSome :foo. :foo :bar :baz }} |
| log:implies { :testb2d a :success }. |
| |
| {{ this log:forAll :fee. :fee :bar :baz } log:includes {this log:forSome :foo. :foo :bar :baz }} |
| log:implies { :testc2d a :success }. # Originally failed |
| |
| |
| |
| {{ :fee :bar :baz } log:includes { :foo :bar :baz }} |
| log:implies { :testa1d a :FAILURE }. |
| |
| {{ this log:forSome :fee. :fee :bar :baz } log:includes { :foo :bar :baz }} |
| log:implies { :testb1d a :FAILURE }. # Originally failed |
| |
| {{ this log:forAll :fee. :fee :bar :baz } log:includes { :foo :bar :baz }} |
| log:implies { :testc1d a :success }. |
| |
| |
| |
| {{ :fee :bar :baz } log:includes {this log:forAll :foo. :foo :bar :baz }} |
| log:implies { :testa3d a :FAILURE }. |
| |
| {{ this log:forSome :fee. :fee :bar :baz } log:includes {this log:forAll :foo. :foo :bar :baz }} |
| log:implies { :testb3d a :FAILURE }. |
| |
| {{ this log:forAll :fee. :fee :bar :baz } log:includes {this log:forAll :foo. :foo :bar :baz }} |
| log:implies { :testc3d a :success }. |
| |
| |
| # Negative tests: |
| |
| |
| |
| {{ :fee :bar :baz } log:notIncludes { this log:forSome :foo. :foo :bar :baz }} |
| log:implies { :testa2nd a :FAILURE }. # Originally failed |
| |
| {{ this log:forSome :fee. :fee :bar :baz } log:notIncludes {this log:forSome :foo. :foo :bar :baz }} |
| log:implies { :testb2nd a :FAILURE }. |
| |
| {{ this log:forAll :fee. :fee :bar :baz } log:notIncludes {this log:forSome :foo. :foo :bar :baz }} |
| log:implies { :testc2nd a :FAILURE }. # Originally failed |
| |
| |
| {{ :fee :bar :baz } log:notIncludes { :foo :bar :baz }} |
| log:implies { :testa1nd a :success }. |
| |
| {{ this log:forSome :fee. :fee :bar :baz } log:notIncludes { :foo :bar :baz }} |
| log:implies { :testb1nd a :success }. |
| |
| {{ this log:forAll :fee. :fee :bar :baz } log:notIncludes { :foo :bar :baz }} |
| log:implies { :testc1nd a :FAILURE }. # Originally failed, STILL FAILS |
| |
| |
| |
| {{ :fee :bar :baz } log:notIncludes {this log:forAll :foo. :foo :bar :baz }} |
| log:implies { :testa3nd a :success }. |
| |
| {{ this log:forSome :fee. :fee :bar :baz } log:notIncludes {this log:forAll :foo. :foo :bar :baz }} |
| log:implies { :testb3nd a :success }. |
| |
| {{ this log:forAll :fee. :fee :bar :baz } log:notIncludes {this log:forAll :foo. :foo :bar :baz }} |
| log:implies { :testc3nd a :FAILURE }. |
| |
| |
| |
| log:implies a log:Chaff. # Purge input rules |
| |
| # ENDS |
| |