Interactive Prover
See the following pages for video introductions to how to use this tool:
Enter a formula and press <Enter> or click the button to start building a proof.
Problem: At the end of the input, invalid start of a formula; expecting to see an atomic formula, a quantifier ('all' or 'ex'), a negation, or a '('.
Instructions on entering formulas:
- Predicate symbols are any sequence of letters and numbers, where the first character is a letter, followed by their arguments in parentheses. This is similar to the rules for variable names in Java.
- Connectives and Quantifiers are represented by ASCII versions:
- And (“∧”) is represented by “/\” (forward slash, backward slash).
- Or (“∨”) is represented by “\/” (backward slash, forward slash).
- Implies (“→”) is represented by “->” (dash, greater than).
- Not “¬” is represented by “¬” (top left of your keyboard). Alternatively, you can use “~” (tilde) or “!” (exclamation mark).
- For all “∀x.” is represented by “all x.”.
- Exists “∃x.” is represented by “ex x.”.
- Use parentheses “(” and “)” to disambiguate mixtures of connectives.
- As an example of the use of ASCII for entering formulas, the formula“∀d. Sunny(d) ∨ Rainy(d)” is entered as “
all d. Sunny(d) \/ Rainy(d)
”, where I have used a monospace font to make the individual characters clearer. - The rules for mixing connectives and parentheses are as in Lecture 01.