Output for modal formulas should be improved.

[johannesmarti]

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]

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]

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.