Equality in conclusion 3

From RIF

Revision as of 15:01, 8 July 2009 by StellaMitchell (Talk | contribs)
(diff) ←Older revision | Current revision (diff) | Newer revision→ (diff)
Jump to: navigation, search



Test TypePositiveEntailmentTest
ContributorMichael Kifer
StatusProposed
Record
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 XML
Conclusion
Presentation SyntaxAnd ( 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 XML
Retrieved from "http://www.w3.org/2005/rules/wiki/Equality_in_conclusion_3"