Warning:
This wiki has been archived and is now read-only.

Equality in conclusion 3

From RIF
Jump to: navigation, search



Test TypePositiveEntailmentTest
ContributorMichael Kifer
StatusApproved
RecordFebruary 16, 2010 telecon
DialectBLD
PurposeTest substitutivity in the context of equality.
DescriptionThis test case verifies that the substitutivity axiom for equality is implemented. In particular, it checks that substitutivity applies to terms nested deeply inside other terms. In this test case, g(c) must be substituted by f(b) at nesting levels 1 and 2 in order for the test to check out. Substitutivity is hard to implement properly and efficiently.
SeeAlso
SpecRefhttp://www.w3.org/2005/rules/wiki/BLD#Terms

http://www.w3.org/2005/rules/wiki/BLD#Formulas

http://www.w3.org/2005/rules/wiki/BLD#Interpretation_of_Non-document_Formulas
Premises
Presentation SyntaxDocument( Prefix(ex <http://example.org/example#>) Group ( Forall ?x ?y ?z ( ex:f(?y)=ex:g(?z) :- And ( ex:p(?x ?y) ex:p(?x ?z) ) ) ex:p(ex:a ex:b) ex:p(ex:a ex:c) ex:q(ex:h(ex:g(ex:c))) ) )
XMLview RIF/XML
Conclusion
Presentation SyntaxAnd ( ex:f(ex:b) = ex:g(ex:c) ex:q(ex:h(ex:f(ex:b))) ex:s(ex:s(ex:f(ex:b))) = ex:s(ex:s(ex:g(ex:c))) )
XMLview RIF/XML
Retrieved from "https://www.w3.org/2005/rules/wiki/index.php?title=Equality_in_conclusion_3&oldid=12183"