Information Technology Reference
In-Depth Information
Fig. 14.7
Sample Output from Handle
jazz
etc.); these are used for comparisons during theorem-proving, replacing the ordinary
arithmetic operators which SNARK cannot reason over.
The following are some key examples of premises in FOL used to define the music
states [
27
], some of which are visible as SNARK axioms in Fig.
14.8
.
1. A person has a solo iff they have the highest level and there are no other players
within one level.
∀
p
1
:
Person
Solo
(
p
1
)
↔∃
l
1
:
Level
MaxLevel
(
p
1
,
l
1
)
∧
∃
Level
p
2
:
Person
(
p
2
,
l
2
)
∧
WithinOne
(
l
1
,
l
2
)
¬
∃
l
2
:
Level
∧
(
p
1
=
p
2
)
Search WWH ::
Custom Search