ГОСТ Р ИС0 18629-41—2011
- (branch_mono ?s1 ?s2 ?s3 ?s4 ?a);
- (reptree ?s?occ),
- (repetitive ?occ);
- (nondet_repetitive ?occ);
- (partial_repetitive ?occ).
- (amorphous ?occ).
Каждое понятиеопределяется неформальнойсемантикой и аксиомой KIF.
9.3 Теории, обусловленные повторяющейся структурой ветвей
Дляданной теории необходимы:
- act_occ.th:
- complex.th;
- atomic.th;
- subactivity.th;
- occtree.th;
- psl_core.th.
9.4 Дофинициональныо расширения, обусловленные повторяющейся структурой вотвой
Для повторяющейся структуры ветвей дефинициональмые расширения нетребуются.
9.5 Определения повторяющейся структуры ветвей
Для повторяющейся структуры ветвей определены нижеследующие понятия.
9.5.1 Branch_mono
Подветвь некоторого минимального действия сначальным событием ?s1 изаключительным собы
тием ?s2 является событийно изоморфическойдля подветви с начальным событием ?s3 и заключитель
ным событием ?s4.
(forall (?s1 ?s2 ?s3 ?s4 ?a) (iff(branch_mono ?s1 ?s2 ?s3 ?s4 ?a)
(forall(?s5 ?s6)
(implies (and (min_precedes ?s1 ?s5 ?a)
(min_precedes ?s6 ?s2 ?a)
(next_subocc ?s5 ?s6 ?a))
(exists (?s7 ?s8)
(and (min_precedes ?s3 ?s7 ?a)
(min_precedes ?s8 ?s4 ?a)
(next_subocc ?s7 ?s8 ?a)
(iso_occ ?s5 ?s7)
(iso_occ?s6 ?s8)))))))
9.5.2 Reptree
Каждое событие ?occ может быть встроено в некоторую ветвь поддерева с корневым событием ?s.
(forall (?s ?осс) (iff(reptree ?s ?occ)
(forall (?s1 ?a)
(implies (and (occurrence ?occ?a)
(subactivity„occurrence ?s1 ?occ))
(exists (?s2 ?s3 ?s4 ?occ1)
(and (same_tree ?o?o1)
(leaf_occ ?s2 ?occ1)
(<_min ?s3 ?s1 ?a)
(<_min ?s1 ?s4 ?a)
(branch_mono ?s3 ?s4 ?s ?s2 ?a)))))))
9.5.3 Repetitive
Событие является повторяющимся тогда и только тогда, когда каждая ветвь на этом же дереве
действий можетбытьвстроена вуникальное поддерево. Интуитивно ясно, чтоэто эквивалентносущество
ванию уникального повторяющегося поддерева.
(forall (?осс) (iff (repetitive ?осс)
(exists (?s1 ?осс2)
13