Enter a formula below and choose a logic and interpolant to compute.
Result:
Usage instructions. We support four logics:
- intuitionistic logic (IL),
- Gödel-Löb logic (GL),
- basic modal logic (K), and
- intuitionistic Strong Löb logic (iSL).
| → | -> | implication |
| ↔ | <-> | equivalence |
| ¬ | ~ | negation |
| ∧ | & | conjunction (and) |
| ∨ | | | disjunction (or) |
| □ | [] | necessity (box) |
| ⋄ | <> | possibility (diamond) |
| ⊤ | T | verum |
| ⊥ | F, # | falsum |
| p | propositional variable to be quantified | |
| q, r, … | other propositional variables (in [a-z][a-z A-Z 0-9]*) |
The quantifiers are always with respect to the variable p.
Disclaimer: This page is only for the purpose of easy demonstration of the formally verified implementation in Coq (more information on this implementation can be found by clicking the links above). The parsing library and the OCaml to JS compiler that were used for building this page are not verified formally. The functions have not yet been optimized; high run-time may occur even on small examples.