(=>
(agreementRevisionDate ?AGR ?DATE ?CHANGE)
(exists (?TIME)
(and
(instance ?TIME ?DATE)
(or
(and
(holdsDuring
(ImmediatePastFn ?TIME)
(not
(subProposition ?CHANGE ?AGR)))
(holdsDuring
(ImmediateFutureFn ?TIME)
(subProposition ?CHANGE ?AGR)))
(and
(holdsDuring
(ImmediatePastFn ?TIME)
(subProposition ?CHANGE ?AGR))
(holdsDuring
(ImmediateFutureFn ?TIME)
(not
(subProposition ?CHANGE ?AGR)))))))) |
Government.kif 705-726 |
If X agreement revision date Y for Z, then there exists W such that W is an instance of Y, Z is not a sub-proposition of X holds during immediately before W, Z is a sub-proposition of X holds during immediately after W or Z is a sub-proposition of X holds during immediately before W, and Z is not a sub-proposition of X holds during immediately after W |