ГОСТ Р И С 018629-11 — 2010
(forall (?осс ?t) (iff(is-occuring-at ?осс ?t)
(and (activity_occurrence ?occ)
(betweenEq (beginof?occ) ?t (endof?occ)))))
6.4Аксиомы
Основными аксиомами ядра PSL являются axiom 1— axiom 17.
П р и м е ч а н и е — Термины defrelation’. exists’, ‘forall’. and’, ’or’, ’not’.’iff. и ’implies’ определены в
Руководстве формата обмена знаниями [8].
10
6.4.1 Аксиома 1
Отношение before происходит только между моментами времени (timepo»nts).
(forall (?t1 ?t2)
(implies (before ?t1 ?t2)
(and (timepoint ?t1)
(timepoint ?t2))))
6.4.2 Аксиома 2
Отношение before представляет собой нестрогий порядок.
(forall (?t1 ?t2)
(implies (and (timepoint ?t1)
(timepoint ?t2))
(or {= ?t1 ?t2)
(before ?t1 ?t2)
(before ?t2?t1))))
6.4.3 Аксиома 3
Отношение before является иррефлексивным.
(forall (?t) (not (before ?t ?t)))
6.4.4 Аксиома 4
Отношение before является транзитивным (переходным).
(forall (?t1 ?t2 ?t3)
(implies (and (before ?t1 ?t2)
(before ?t2?t3))
(before ?t1 ?t3)))
6.4.5 Аксиома 5
Отрицательная бесконечность момента времени (timepoint tnf-) существует перед всеми другими мо
ментами времени.
(forall (?t)
(implies (and (timepoint ?t) (not (= ?t inf-)))
(before inf- ?t))
6.4.6 Аксиома 6
Перед положительной бесконечностью (inf-*-)существуют все остальные моменты времени.
(forall (?t)
(implies (and (timepoint ?t) (not (= ?t inf*-)))
(before ?t inf-*-))
6.4.7 Аксиома 7
Момент времени между inf- и t наступает при любом моменте времени t. не являющимся отрицатель
ной бесконечностью (inf-).
(forall (?t)
(implies (and (timepoint ?t)
(not (= ?t inf-)))
(exists (?u)
(between inf- ?u ?t))))
6.4.8 Аксиома 8
Момент времени между inf-*- и t наступает при любом моменте времени t. не являющимся положи
тельной бесконечностью (inf-*).
(forall (?t)
(implies (and (timepoint ?t)
(not (= ?t inf*-)))
(exists (?u)
(between ?t ?u inf-*-))))