blob: fa6a036caac4643339dc81167c114ef0e17a567b [file] [log] [blame]
# 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