CS208 Logic & Algorithms

Semester 1: Logic

Interactive Prover

See the following pages for video introductions to how to use this tool:

  1. Natural Deduction and the rules for And

  2. Proof rules for Implication

  3. Proof rules for Or and Not

  4. Proof rules for Predicate Logic

  5. Proof rules for Equality

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.