ГОСТ Р ИСО 18629-44 - 2011
до начала выполнения данного действия равнялось нулю.
(forall (?а ?r) (iff (creates ?а ?г)
(exists (?q1)
(and (produces_quantity ?a ?r ?q1)
(forall (?q2 ?occ)
(implies (and (occurrence._of ?occ ?a)
(prior (resource_point ?r ?q2) ?occ)
(=?q2 zero_quantity)))))))
8.5.7 destroys
Некоторое действие уничтожает какой-либо ресурс тогда и только тогда,
когда оно потребляет некоторое количество ресурса, и количество данного
ресурса после завершения данного действия равно нулю.
(forall (?а ?r) (iff (destroys ?а ?г)
(exists (?q1)
(and (consumes_quantity ?a ?r ?q1)
(forall (?q2 ?occ)
(implies (and (occurrence ?occ ?a)
(prior (resource_point ?r ?q2) ?occp)
(= ?q2zero_quantity))))))))
8.5.8 fixed_quantity
Какой-либо ресурс имеет фиксированное количество ?q тогда и только
тогда, когда предоставление ресурса неизменно и одно и то же во всех случаях.
(forall (?r ?q) (iff (fixed_quantity ?r ?q)
(forall (?occ)
(holds (resource_point ?r ?q) ?occ)))))
8.5.9 nonreplenishable
Какой-либо ресурс является непополняемым тогда и только тогда, когда
предоставление ресурса не может увеличиваться после завершения действия,
потребляющего данный ресурс.
(forall (?r) (iff (nonreplenishable ?r)
(forall (?a ?q1 ?q2 ?occ1 ?occ2 ?occ3)
(implies (and (implies(do ?a ?occ1 ?occ2)
(holds (resource_point ?r ?q1) ?occ2))
(precedes ?occ2 ?occ3)
(holds (resource_point ?r ?q2) ?occ3)))
(or (greater ?q1 ?q2)
(= ?q
1
?q2)))))
8.5.10 uses
Некоторое действие использует какой-либо ресурс тогда и только тогда,
когда оно использует некоторое количество данного ресурса.
20