search

hferee / UIML

Uniform Interpolation for Modal Logics
Other
4 stars 1 forks source link

Output for modal formulas should be improved. #6

Open johannesmarti opened 2 months ago

johannesmarti commented 2 months ago

When I am asking for the uniform interpolant of p & q & [](p & q) I get ¬ ((⊤ → (⊤ → (⊤ → ⋄ ⊥))) → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((⊤ → (⊤ → (⊤ → ⋄ ⊥))) → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((⊤ → (⊤ → (⊤ → ⋄ ⊥))) → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((⊤ → (⊤ → (⋄ ((⊤ → (⊤ → (⊤ → ⋄ ⊥))) → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((⊤ → (⊤ → (⊤ → ⋄ ⊥))) → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ⊥)))))))))) → ⋄ ⊥))) → (⊤ → ((⊤ → (⊤ → (⋄ ((⊤ → (⊤ → (⊤ → ⋄ ⊥))) → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((⊤ → (⊤ → (⊤ → ⋄ ⊥))) → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ⊥)))))))))) → ⋄ ⊥))) → (⊤ → ((⊤ → (⊤ → (⊤ → ⋄ ⊥))) → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((⊤ → (⊤ → (⊤ → ⋄ ⊥))) → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((⊤ → (⊤ → (⊤ → ⋄ ⊥))) → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((⊤ → (⊤ → (⋄ ((⊤ → (⊤ → (⊤ → ⋄ ⊥))) → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((⊤ → (⊤ → (⊤ → ⋄ ⊥))) → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ⊥)))))))))) → ⋄ ⊥))) → (⊤ → ((⊤ → (⊤ → (⋄ ((⊤ → (⊤ → (⊤ → ⋄ ⊥))) → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((⊤ → (⊤ → (⊤ → ⋄ ⊥))) → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ((¬ q → (⊤ → (⊤ → ⋄ ⊥))) → (⊤ → ⊥)))))))))) → ⋄ ⊥))) → (⊤ → ⊥))))))))))))))))))))))))))))))))))))))))))))))))))

Would be nice to have some post-processing that cleans up this formula using obvious equivalences.

hferee commented 2 months ago

Thank you for your comment.

Yes, this feature is planned. It can be very easily done in an unverified way as a post-processing in ocaml, but we were hoping to do it in Coq beforehand.

hferee commented 2 hours ago

Progress: we have made (provably correct) simplifications in the cases of iSL/IPC.

Porting it to K/GL would be not so trivial ; and we want to keep the demo provably correct.

After the command line tool is perfected (#21), it would be easy to add unverified simplifications in OCaml.