Welcome to the epiSAT page

epiSAT is a satifiability solver for the logic of epistemic hierarchies. Internally, epiSAT uses a prefixed tableau calculus that incrementally translated into a Boolean satisfiability problem. epiSAT supports bounded quantification over groups of modalities.

Examples

• epiSAT supports default reasoning.
  s > p; s > q; ∀ x, x ≤ {p,q}. (⟨x⟩⊤ → ⟨x⟩keepRight) → [s]keepRight;
  — System s will keep on the right whenever it is consistent with its components p and q.
• epiSAT supports non-monotonic reasoning with conditionals. The following Goodman example is satisfiable.
  s0 > s1; s1 > s2; — s0 is the innermost of three spheres.
  ⟨s0⟩⊤; — To avoid trivial, vacuous models, we assume that the innermost sphere is consistent.
  [s2]( scratch ∧ oxygen → light ); — Everywhere the physical law holds: if I scratch a match and enough oxygene is present it will light.
  [s1]oxygen; — In the middle sphere enough oxygene is present.
  [s0]¬scratch; — Actually, I did not scratch the match.
  [s0]¬light; — And the match did not light.
  scratch []=> light; — If I had scratched the match, it would have lighted.
  ¬( scratch ∧ ¬oxygene []=> light ); — However, it is not true, that if I had scratched the match and there was not enough oxygene, the match would have lighted.
  
  Hence, the conditional []=> is non-monotonic.

epiSAT is written in C++ and uses minisat for the Boolean satisfiability problem. Currently, epiSAT is an early prototype and lacks of a user interface. This will change soon. Here you can download the first prototype from May 11, 2021.

Update (June 6, 2021): Here you can download a new version that supports parsing.

Update (June 11, 2021): Here you can download a new version with improved output and parsing.

Update (August 17, 2021): Here you can download a new version that allows nested variable modalities. I.e., both occurences of the variable x in Ex x. [x][x]phi are assigned to a single instance.

Materials

• Preliminary paper on epistemic hierarchies: paper
• Talk held on 1st of October, 2021 on epistemic hierarchies and their relationship to the "metamodel": talk
• Talk held on 22nd of October, 2021 on justifications and justifiability at the Third Workshop on Formal Methods for Autonomous Systems: talk