Sentences — enter one or more English sentences to translate. Use Add sentence for multiple sentences. Toggle Show answer key to enter the reference translation and intended key (hidden from students).
Worksheet — build your translation key by listing predicates (with arity and English clause template) and constants (with their English names).
Translation — type the symbolic translation of each sentence using your key. Hit Check to compare your formula with the reference (up to bound-variable renaming). Hit Reveal to see the reference answer.
| Symbol | ASCII | Unicode |
|---|---|---|
| Negation | ~ or - | ¬ |
| Conjunction | & or /\ | ∧ |
| Disjunction | | or \/ | ∨ |
| Conditional | -> or => | → |
| Biconditional | <-> | ↔ |
| Universal | Ax or @x | ∀x |
| Existential | Ex or #x | ∃x |
Predicates: uppercase letter followed by variable/constant letters, e.g. Px, Rxy, Rab.
Quantifiers: ∀x φ or ∃x φ. Variables are single lowercase letters.
Constants: lowercase letters a–e (and others not used as variables).
Enter sentences above to begin.
Enter sentences above to begin.