-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathctl_rule
56 lines (41 loc) · 2.8 KB
/
ctl_rule
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
cnf(empty_def, axiom, ~ in(X1, nil)).
cnf(con_p1, axiom, in(X1, con(X1, Z))).
cnf(con_p2, axiom, in(X1, con(Y1, Z)) | ~in(X1, Z)).
cnf(par0, axiom, ~ pi0(not(P), X1) | ~ pi0(P, X1)).
cnf(par1, axiom, ~ pi0(or(P, Q), X1) | pi0(P, X1) | pi0(Q, X1)).
cnf(par3, axiom, ~ pi0(and(P, Q), X1) | pi0(Q, X1)).
cnf(par2, axiom, ~ pi0(and(P, Q), X1) | pi0(P, X1)).
cnf(ctl_ax, axiom, ~ pi0(ax(P), X1) | ~r(X1, con(Z1, Z)) | pi1(land(P), con(Z1, Z))).
cnf(ctl_ex, axiom, ~ pi0(ex(P), X1) | ~r(X1, con(Z1, Z)) | pi1(lor(P), con(Z1, Z))).
cnf(ctl_eg1, axiom, ~ pi0(eg(P), X1) | ~r(X1, con(Z1, Z)) | pi1(lor(eg(P)), con(Z1, Z))).
cnf(ctl_eg2, axiom, ~ pi0(eg(P), X1) | pi0(P, X1)).
cnf(ctl_ag1, axiom, ~ pi0(ag(P), X1) | ~r(X1, con(Z1, Z)) | pi1(land(ag(P)), con(Z1, Z))).
cnf(ctl_ag2, axiom, ~ pi0(ag(P), X1) | pi0(P, X1)).
cnf(ctl_af1, axiom, ~ pi0(af(P), X1) | pi2(af(P), X1, nil)).
cnf(ctl_af2, axiom, ~ pi2(af(P), X1, Y)| pi0(P, X1) | ~r(X1, con(Z1, Z)) | pi3(land(af(P)), con(Z1, Z), con(X1, Y))).
cnf(ctl_af3, axiom, ~ pi2(af(P), X1, Y) | ~in(X1,Y)).
cnf(ctl_ef1, axiom, ~ pi0(ef(P), X1) | pi2(ef(P), X1, nil)).
cnf(ctl_ef2, axiom, ~ pi2(ef(P), X1, Y) |pi0(P, X1) | ~r(X1, con(Z1, Z)) | pi3(lor(ef(P)), con(Z1, Z), con(X1, Y))).
cnf(ctl_ef3, axiom, ~ pi2(ef(P), X1, Y) | ~in(X1,Y)).
cnf(ctl_au1, axiom, ~ pi0(au(P, Q), X1) | pi2(au(P, Q), X1, nil)).
cnf(ctl_au2, axiom, ~ pi2(au(P, Q), X1, Y)| pi0(Q, X1) | ~r(X1, con(Z1, Z)) | pi3(land(au(P, Q)), con(Z1, Z), con(X1, Y))).
cnf(ctl_au2, axiom, ~ pi2(au(P, Q), X1, Y)| pi0(Q, X1) | pi0(P, X1)).
cnf(ctl_au3, axiom, ~ pi2(au(P, Q), X1, Y) | ~in(X1,Y)).
cnf(ctl_eu1, axiom, ~ pi0(eu(P, Q), X1) | pi2(eu(P, Q), X1, nil)).
cnf(ctl_eu2, axiom, ~ pi2(eu(P, Q), X1, Y)| pi0(Q, X1) | ~r(X1, con(Z1, Z)) | pi3(lor(eu(P, Q)), con(Z1, Z), con(X1, Y))).
cnf(ctl_eu2, axiom, ~ pi2(eu(P, Q), X1, Y)| pi0(Q, X1) | pi0(P, X1)).
cnf(ctl_eu3, axiom, ~ pi2(eu(P, Q), X1, Y) | ~in(X1,Y)).
cnf(ctl_er1, axiom, ~ pi0(er(P, Q), X1) | pi0(P, X1) | ~r(X1, con(Z1, Z)) | pi1(lor(er(P, Q)), con(Z1, Z))).
cnf(ctl_er2, axiom, ~ pi0(er(P, Q), X1) | pi0(Q, X1)).
cnf(ctl_ar1, axiom, ~ pi0(ar(P, Q), X1) | pi0(P, X1) |~r(X1, con(Z1, Z)) | pi1(land(ar(P, Q)), con(Z1, Z))).
cnf(ctl_ar2, axiom, ~ pi0(ar(P, Q), X1) | pi0(Q, X1)).
cnf(ctl_land1, axiom, ~ pi1(land(P), con(X1, Z)) | pi1(land(P), Z)).
cnf(ctl_land2, axiom, ~ pi1(land(P), con(X1, Z)) | pi0(P, X1)).
cnf(ctl_land3, axiom, ~ pi3(land(P), con(X1,Z), Y) | pi3(land(P), Z, Y)).
cnf(ctl_land4, axiom, ~ pi3(land(P), con(X1,Z), Y) | pi2(P, X1, Y)).
cnf(ctl_lor1, axiom, ~ pi1(lor(P), con(X1, Z)) | pi0(P, X1) | pi1(lor(P), Z)).
cnf(ctl_lor2, axiom, ~ pi1(lor(P), nil)).
cnf(ctl_lor3, axiom, ~ pi3(lor(P), con(X1, Z), Y) | pi2(P, X1, Y) | pi3(lor(P), Z, Y)).
cnf(ctl_lor4, axiom, ~ pi3(lor(P), nil, Y)).
cnf(neq1, axiom, neq(b(ff,tt), b(tt,ff))).
cnf(neq2, axiom, neq(b(tt,ff), b(ff,tt))).