Information Technology Reference
In-Depth Information
The following propositions provide means for recursively deducing the bounds of variables:
Proposition A.1
(Deduction rules to determine the bounds for ∀
x
.
p
)
1. (
p
= ¬
q
) ∧
e
= ↑
x
(∃
x.q
) ⇒ e = ↑
x
(∀
x.p
)
2. (
p
= ¬
q
) ∧
e
= ↓
x
(∃
x.q
) ⇒ e = ↓
x
(∀
x.p
)
3. (
p
=
q
→
r
) ∧
e
= ↑
x
(∃
x.q
) ⇒ e = ↑
x
(∀
x.p
)
4. (
p
=
q
→
r
) ∧
e
= ↓
x
(∃
x.q
) ⇒ e = ↓
x
(∀
x.p
)
5. (
p
=
q
→
r
) ∧
e
= ↑
x
(∀
x.r
) ⇒ e = ↑
x
(∀
x.p
)
6. (
p
=
q
→
r
) ∧
e
= ↓
x
(∀
x.r
) ⇒ e = ↓
x
(∀
x.p
)
7. (
p
=
q
∧
r
) ∧
e
1
= ↑
x
(∀
x.q
) ∧
e
2
= ↑
x
(∀
x.r
) ⇒
max
(
e
1
,
e
2
) = ↑
x
(∀
x.p
)
8. (
p
=
q
∧
r
) ∧
e
1
= ↓
x
(∀
x.q
) ∧
e
2
= ↓
x
(∀
x.r
) ⇒
min
(
e
1
,
e
2
) = ↓
x
(∀
x.p
)
9. (
p
=
q
∨
r
) ∧
e
1
= ↑
x
(∀
x.q
) ∧
e
2
= ↑
x
(∀
x.r
) ⇒
min
(
e
1
,
e
2
) = ↑
x
(∀
x.p
)
10. (
p
=
q
∨
r
) ∧
e
1
= ↓
x
(∀
x.q
) ∧
e
2
= ↓
x
(∀
x.r
) ⇒
max
(
e
1
,
e
2
) = ↓
x
(∀
x.p
)
11. (
p
=
q
∨
r
) ∧
e
= ↑
x
(∀
x.q
) ⇒ e = ↑
x
(∀
x.p
)
12. (
p
=
q
∨
r
) ∧
e
= ↓
x
(∀
x.q
) ⇒ e = ↓
x
(∀
x.p
)
13. (
p
=
q
↔
r
) ∧
e
1
= ↑
x
(∀
x.q
) ∧
e
2
= ↑
x
(∀
x.r
) ⇒
max
(
e
1
,
e
2
) = ↑
x
(∀
x.p
)
14. (
p
=
q
↔
r
) ∧
e
1
= ↓
x
(∀
x.q
) ∧
e
2
= ↓
x
(∀
x.r
) ⇒
min
(
e
1
,
e
2
) = ↓
x
(∀
x.p
)
15. (
p
=
q
↔
r
) ∧
e
1
= ↑
x
(∃
x.q
) ∧
e
2
= ↑
x
(∃
x.r
) ⇒
max
(
e
1
,
e
2
) = ↑
x
(∀
x.p
)
16. (
p
=
q
↔
r
) ∧
e
1
= ↓
x
(∃
x.q
) ∧
e
2
= ↓
x
(∃
x.r
) ⇒
min
(
e
1
,
e
2
) = ↓
x
(∀
x.p
)
Proposition A.2
(Deduction rules to determine the bounds for ∃
x
.
p
)
17. (
p
= ¬
q
) ∧
e
= ↑
x
(∀
x.q
) ⇒ e = ↑
x
(∃
x.p
)
18. (
p
= ¬
q
) ∧
e
= ↓
x
(∀
x.q
) ⇒ e = ↓
x
(∃
x.p
)
19. (
p
=
q
→
r
) ∧
e
1
= ↑
x
(∀
x.q
) ∧
e
2
= ↑
x
(∃
x.r
) ⇒
max
(
e
1
,
e
2
) = ↑
x
(∃
x.p
)
20. (
p
=
q
→
r
) ∧
e
1
= ↓
x
(∀
x.q
) ∧
e
2
= ↓
x
(∃
x.r
) ⇒
min
(
e
1
,
e
2
) = ↓
x
(∃
x.p
)
21. (
p
=
q
∧
r
) ∧
e
= ↑
x
(∃
x.q
) ⇒ e = ↑
x
(∃
x.p
)
22. (
p
=
q
∧
r
) ∧
e
= ↓
x
(∃
x.q
) ⇒ e = ↓
x
(∃
x.p
)
23. (
p
=
q
∨
r
) ∧
e
1
= ↑
x
(∃
x.q
) ∧
e
2
= ↑
x
(∃
x.r
) ⇒
max
(
e
1
,
e
2
) = ↑
x
(∃
x.p
)
24. (
p
=
q
∨
r
) ∧
e
1
= ↓
x
(∃
x.q
) ∧
e
2
= ↓
x
(∃
x.r
) ⇒
min
(
e
1
,
e
2
) = ↓
x
(∃
x.p
)
25. (
p
=
q
↔
r
) ∧
e
1
= ↑
x
(∀
x.q
) ∧
e
2
= ↑
x
(∃
x.r
) ⇒
max
(
e
1
,
e
2
) = ↑
x
(∃
x.p
)
26. (
p
=
q
↔
r
) ∧
e
1
= ↓
x
(∀
x.q
) ∧
e
2
= ↓
x
(∃
x.r
) ⇒
min
(
e
1
,
e
2
) = ↓
x
(∃
x.p
)
Search WWH ::
Custom Search