git://colo12-c703.uibk.ac.at
/
hl193./.git
/ blob
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
history
|
raw
|
HEAD
Update from HH
[hl193./.git]
/
Tutorial
/
Propositional_logic.ml
1
TAUT
2
`(~input_a ==> (internal <=> T)) /\
3
(~input_b ==> (output <=> internal)) /\
4
(input_a ==> (output <=> F)) /\
5
(input_b ==> (output <=> F))
6
==> (output <=> ~(input_a \/ input_b))`;;
7
8
TAUT
9
`(i1 /\ i2 <=> a) /\
10
(i1 /\ i3 <=> b) /\
11
(i2 /\ i3 <=> c) /\
12
(i1 /\ c <=> d) /\
13
(m /\ r <=> e) /\
14
(m /\ w <=> f) /\
15
(n /\ w <=> g) /\
16
(p /\ w <=> h) /\
17
(q /\ w <=> i) /\
18
(s /\ x <=> j) /\
19
(t /\ x <=> k) /\
20
(v /\ x <=> l) /\
21
(i1 \/ i2 <=> m) /\
22
(i1 \/ i3 <=> n) /\
23
(i1 \/ q <=> p) /\
24
(i2 \/ i3 <=> q) /\
25
(i3 \/ a <=> r) /\
26
(a \/ w <=> s) /\
27
(b \/ w <=> t) /\
28
(d \/ h <=> u) /\
29
(c \/ w <=> v) /\
30
(~e <=> w) /\
31
(~u <=> x) /\
32
(i \/ l <=> o1) /\
33
(g \/ k <=> o2) /\
34
(f \/ j <=> o3)
35
==> (o1 <=> ~i1) /\ (o2 <=> ~i2) /\ (o3 <=> ~i3)`;;