pcarbonn · February 10, 2022 16:46
diff --git a/!Intensions.md b/!Intensions.md
diff --git a/DMN_community_challenge b/DMN_community_challenge
 #! IDP-Z3 0.9.2
 vocabulary {
    type Severity := {0,1,2,3}

    young: () → 𝔹
    temperature: () → ℝ
    coughing : () → 𝔹
    sneezing : () → 𝔹
    fever    : () → 𝔹
    symptom : Concept[() → 𝔹] → 𝔹
    severity : () → Severity
    furtherTest: () → 𝔹
 }

 theory {
    symptom := {`coughing, `sneezing, `fever}.

    [Definition of fever]
    { [A young has fever above 37.2°]
      fever() ← young() ∧ 37.2 < temperature().
      [An adult has fever above 38°]
      fever() ← ¬young() ∧ 38.0 < temperature(). }

    [The severity is the number of symptoms]
    severity() = #{s ∈ symptom: $(s)()}.
    
    [More tests are needed if there are more than 2 symptoms]
    { furtherTest() ← 2 ≤ severity(). }

    severity()=0 ∨ severity()=1 ∨ severity()=2 ∨ severity()=3.
 }

 display {
    goal_symbol := {`furtherTest}.
    view()=expanded.
 }
diff --git a/International_law b/International_law
 #! IDP-Z3 0.9.2
 vocabulary {
    type Country := {Belgium, France}
    amount_thresholdEU, periodEU:    ()   → ℤ
    amount_threshold, period:     Country → ℤ
    obligation: Concept[Country→ℤ] → 𝔹
    mapping:    Concept[Country→ℤ] → Concept[()→ℤ]
 }
 theory {
    obligation := {`amount_threshold, `period}.
    mapping := {`amount_threshold → `amount_thresholdEU, 
                `period           → `periodEU}.
                
    ∀ o ∈ obligation: ∀c ∈ Country: $(o)(c) ≤  $(mapping(o))().
 }
 procedure main() {
    pretty_print(model_expand(T))
 }
diff --git a/Symptoms b/Symptoms
 #! IDP-Z3 0.9.2
 vocabulary V {
  type Patient := {Bob}
  
  coughing : Patient → 𝔹
  sneezing : Patient → 𝔹
  fever    : Patient → 𝔹
  highRisk : Patient → 𝔹

  riskFactor : Concept[Patient → 𝔹] → 𝔹
  severity   : Patient → ℤ
  test     : Patient → 𝔹
 }

 theory T:V {
    riskFactor := {`coughing, `sneezing, `fever, `highRisk}.
    ∀x ∈ Patient: severity(x) = #{rf ∈ riskFactor: $(rf)(x)}.
    ∀x ∈ Patient: test(x) ⇔ 3 ≤ severity(x).
 }

 procedure main() {
    pretty_print(model_expand(T))
 }
diff --git a/Template b/Template
 #! IDP-Z3 0.9.2
 vocabulary { 
    type Node := {a}
    g1, g2: Node ⨯ Node → 𝔹
    TransClos: Concept[Node ⨯ Node → 𝔹] ⨯ Node ⨯ Node → 𝔹
 }
 theory {
    {∀r ∈ Concept[Node ⨯ Node → 𝔹]: ∀x,y ∈ Node: TransClos(r, x, y) ← $(r)(x,y).
     ∀r ∈ Concept[Node ⨯ Node → 𝔹]: ∀x,z ∈ Node: TransClos(r, x, z) ← ∃y ∈ Node: TransClos(r, x, y) ∧ TransClos(r, y, z). 
    }
 }

 procedure main() {
    pretty_print(model_expand(T))
 }

diff --git a/Word_disambiguation b/Word_disambiguation
 #! IDP-Z3 0.9.2
 vocabulary V {
    type Person := {Bob, Alice}
    biologicalChildof, legalChildOf, feeds: Person ⨯ Person → 𝔹

    childConcept: () → Concept[Person ⨯ Person → 𝔹]
 }
 theory T:V {
    childConcept() ∈ {`biologicalChildof, `legalChildOf}.
        
    [Parents must feed their children]
    ∀p1, p2 ∈ Person: 
      ∀y ∈ Concept[Person ⨯ Person → 𝔹]: y=childConcept() ∧ $(y)(p1, p2) ⇒ 
        feeds(p1, p2).  
 }
	#! IDP-Z3 0.9.2
	vocabulary {
	type Severity := {0,1,2,3}

	young: () → 𝔹
	temperature: () → ℝ
	coughing : () → 𝔹
	sneezing : () → 𝔹
	fever : () → 𝔹
	symptom : Concept[() → 𝔹] → 𝔹
	severity : () → Severity
	furtherTest: () → 𝔹
	}

	theory {
	symptom := {`coughing, `sneezing, `fever}.

	[Definition of fever]
	{ [A young has fever above 37.2°]
	fever() ← young() ∧ 37.2 < temperature().
	[An adult has fever above 38°]
	fever() ← ¬young() ∧ 38.0 < temperature(). }

	[The severity is the number of symptoms]
	severity() = #{s ∈ symptom: $(s)()}.

	[More tests are needed if there are more than 2 symptoms]
	{ furtherTest() ← 2 ≤ severity(). }

	severity()=0 ∨ severity()=1 ∨ severity()=2 ∨ severity()=3.
	}

	display {
	goal_symbol := {`furtherTest}.
	view()=expanded.
	}
	#! IDP-Z3 0.9.2
	vocabulary {
	type Country := {Belgium, France}
	amount_thresholdEU, periodEU: () → ℤ
	amount_threshold, period: Country → ℤ
	obligation: Concept[Country→ℤ] → 𝔹
	mapping: Concept[Country→ℤ] → Concept[()→ℤ]
	}
	theory {
	obligation := {`amount_threshold, `period}.
	mapping := {`amount_threshold → `amount_thresholdEU,
	`period → `periodEU}.

	∀ o ∈ obligation: ∀c ∈ Country: $(o)(c) ≤ $(mapping(o))().
	}
	procedure main() {
	pretty_print(model_expand(T))
	}
	#! IDP-Z3 0.9.2
	vocabulary V {
	type Patient := {Bob}

	coughing : Patient → 𝔹
	sneezing : Patient → 𝔹
	fever : Patient → 𝔹
	highRisk : Patient → 𝔹

	riskFactor : Concept[Patient → 𝔹] → 𝔹
	severity : Patient → ℤ
	test : Patient → 𝔹
	}

	theory T:V {
	riskFactor := {`coughing, `sneezing, `fever, `highRisk}.
	∀x ∈ Patient: severity(x) = #{rf ∈ riskFactor: $(rf)(x)}.
	∀x ∈ Patient: test(x) ⇔ 3 ≤ severity(x).
	}

	procedure main() {
	pretty_print(model_expand(T))
	}
	#! IDP-Z3 0.9.2
	vocabulary {
	type Node := {a}
	g1, g2: Node ⨯ Node → 𝔹
	TransClos: Concept[Node ⨯ Node → 𝔹] ⨯ Node ⨯ Node → 𝔹
	}
	theory {
	{∀r ∈ Concept[Node ⨯ Node → 𝔹]: ∀x,y ∈ Node: TransClos(r, x, y) ← $(r)(x,y).
	∀r ∈ Concept[Node ⨯ Node → 𝔹]: ∀x,z ∈ Node: TransClos(r, x, z) ← ∃y ∈ Node: TransClos(r, x, y) ∧ TransClos(r, y, z).
	}
	}

	procedure main() {
	pretty_print(model_expand(T))
	}
	#! IDP-Z3 0.9.2
	vocabulary V {
	type Person := {Bob, Alice}
	biologicalChildof, legalChildOf, feeds: Person ⨯ Person → 𝔹

	childConcept: () → Concept[Person ⨯ Person → 𝔹]
	}
	theory T:V {
	childConcept() ∈ {`biologicalChildof, `legalChildOf}.

	[Parents must feed their children]
	∀p1, p2 ∈ Person:
	∀y ∈ Concept[Person ⨯ Person → 𝔹]: y=childConcept() ∧ $(y)(p1, p2) ⇒
	feeds(p1, p2).
	}