blob: ca4d0daac3146decac673ddd82450e1c4129c48a (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
import Mathematics
-- Knowledge Base domain: SocietyCulture
opaque Person : Type
-- Person extends Entity
axiom Person.val : Person → Entity
opaque Place : Type
-- Place extends Entity
axiom Place.val : Place → Entity
opaque City : Type
-- City extends Place
axiom City.val : City → Place
opaque athens : City
opaque birthyear : Person → Nat
opaque bornIn : Person → Place → Prop
axiom fact_bornIn_socrates_athens : bornIn socrates athens
|
