/
dtv_dur_interval.clif
55 lines (41 loc) · 2.16 KB
/
dtv_dur_interval.clif
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
/*******************************************************************************
* Copyright (c) University of Toronto and others. All rights reserved.
* The content of this file is licensed under the Creative Commons Attribution-
* ShareAlike 4.0 Unported license. The legal text of this license can be
* found at http://creativecommons.org/licenses/by-sa/4.0/legalcode.
*
* Contributors:
* Michael Gruninger - initial implementation
*******************************************************************************/
(cl-text http://colore.oor.net/dtv_dur_interval/dtv_dur_interval.clif
(cl-imports http://colore.oor.net/dtv_interval/dtv_interval.clif)
(cl-imports http://colore.oor.net/dtv_plus/dtv_plus.clif)
(cl-imports http://colore.oor.net/dtv_duration/dtv_duration.clif)
(forall ((t 'time interval') (d1 duration) (d2 duration))
(if (and ('time interval has duration' t d1)
('time interval has duration' t d2))
(= d1 d2)))
(forall ((t 'time interval'))
(gt ('duration of' t) D0))
(forall ((t 'time interval'))
(not (= ('duration of' t) D0)))
(forall ((t1 'time interval') (t2 'time interval'))
(not (= D0 (+ ('duration of' t1) ('duration of' t2)))))
(forall ((t1 'time interval') (t2 'time interval'))
(if ('time interval1 is part of time interval2' t1 t2)
(leq ('duration of time interval' t1) ('duration of time interval' t2))))
(forall ((t1 'time interval') (t2 'time interval'))
(if ('time interval1 meets time interval2' t1 t2)
(exists ((t3 'time interval') (d3 duration))
(and ('time interval3 equals time interval1 plus time interval2' t3 t1 t2)
('duration3 equals duration1 plus duration2' d3 ('duration of' t1) ('duration of' t2))
(= d3 ('duration of' t3))))))
(forall ((t1 'time interval') (t2 'time interval'))
(exists ((t3 'time interval'))
(if ('time interval1 starts time interval2 complementing time interval3' t1 t2 t3)
(= ('duration of' t2) (+ ('duration of' t3) ('duration of' t1))))))
(forall ((t1 'time interval') (t2 'time interval'))
(exists ((t3 'time interval'))
(if ('time interval1 finishes time interval2 complementing time interval3' t1 t2 t3)
(= ('duration of' t2) (+ ('duration of' t3) ('duration of' t1))))))
)