Equality in conclusion 3



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
Last modified on 2 March 2010, at 01:34