Gamen.jl logo Gamen.jl / Notebooks

Health Application Notebooks

Clinical applications of modal logic for health informatics graduate students. Each notebook parallels a B&D chapter but uses guideline formalization, deontic obligations, and automated conflict detection as the running examples. No prior logic background assumed. Browse below or run interactively on Binder.

Chapters

  1. Ch 0 Clinical Rules and Propositional Logic MYCIN production rules, IF-THEN reasoning, and why propositional logic falls short for guidelines
  2. Ch 1 Clinical Obligations Formalizing "must," "may," and "must not" as □ and ◇; guideline obligations as Kripke models
  3. Ch 2 Guideline Properties Seriality (achievable obligations), reflexivity, transitivity — choosing frame properties for clinical norms
  4. Ch 3 Deontic Systems for Guidelines KD as the logic of clinical guidelines; why K alone is insufficient; the D axiom and "ought implies can"
  5. Ch 4 Completeness and Consistency What it means for a guideline set to be provably consistent; soundness, completeness, and CDS guarantees
  6. Ch 5 Decidability for Guideline Checking Filtrations make automated guideline checking tractable; decidability as a computational guarantee
  7. Ch 6 Guideline Conflict Detection Automated detection of conflicts between clinical guidelines using modal tableaux
  8. Ch 14 Temporal Clinical Protocols "Blood cultures before antibiotics," "reassess at 48 hours" — temporal operators in clinical sequencing
  9. Ch 15 Clinician Knowledge and Information Asymmetry What the attending knows vs. what the EHR records; Ka operators for multi-agent clinical reasoning

Extension

  1. Ext Multi-Guideline Conflict Detection Detecting conflicts across full guideline sets; why pairwise checking is insufficient; the 60–30–10 challenge
→ B&D Companion Notebooks