6. Introduction to Higher Order Logic in Isabelle Flashcards
1
Q
Define lambda abstraction
A
Terms that denote functions directly by the rules that define them.
(λx. x * x) 3 = 9
2
Q
What are the two primitive functions in HOL?
A
3
Q
How are predicates represented in HOL?
A
functions of type (alpha => bool)
4
Q
How are sets represented in HOL?
A
As predicates
5
Q
How is true defined in HOL?
A
6
Q
How is universal quantification represented in HOL?
A
7
Q
How is conjunction represented in HOL?
A
8
Q
How is disjunction defined in HOL?
A
