ProofWeb : logic education through the web

Cezary Kaliszyk, Freek Wiedijk, Femke van Raamsdonk Radboud University Nijmegen & Free University Amsterdam SURF Foundation

FORMED

ETAPS 2008, Budapest, Hungary 2008 03 29, 15: 20 teaching logic with the computer logic course for math/computer science students :

propositional logic predicate logic predicate logic with equality

practising natural deduction proofs

• on paper students does not learn to be precise

• with the computer

student does not learn to do it all himself both necessary: complement each other features

• built on top of serious proof system: Coq – students work with an industrial strength system

– proofs look exactly like in a traditional textbook compatible with: Huth & Ryan, Login in Computer Science

• web-based – students don’t need to install anything

– students can access their work from anywhere

– teacher has at all times full info on student’s work

• comes with a manual explaining the system

• comes with a set of graded exercises Coq proof assistant based on constructive logic developed at INRIA, France 1984 until today used for impressive proofs :

• four color theorem, Georges Gonthier

• verified C compiler, Xavier Leroy power of Coq also makes ProofWeb attractive for education

natural deduction (Fitch style)

1  ∃x(P (x) ∨ ¬Q(a))  assumption
2  Q(a)  assumption
3  b P (b) ∨ ¬Q(a)  assumption
4  P (b)  assumption
5  ∃x P (x)  ∃i 4
6  ¬Q(a)  assumption
7  ⊥  ¬e 6,2
8  ∃x P (x)  ⊥e 7
9  ∃x P (x)  ∨e 3,4—5,6—8
10  ∃x P (x)  ∃e 1,3—9
11  Q(a) → ∃x P (x)  →i 2—10
12  ∃x(P (x) ∨ ¬Q(a)) → Q(a) → ∃x P (x) →i 1—11

1           H1: ∃x, (P x ∨ ¬Q a)                     assumption
2           H2:   Q a                                   assumption

            b

3           H3:   P b ∨ ¬Q a                           assumption
4           H4:   P b                                   assumption
5  ∃x, P x  ∃i 4
6           H5: ¬Q a                                 assumption
7  ⊥  ¬e 6,2
8  ∃x, P x  ⊥e 7
9  ∃x, P x  ∨e 3,4-5,6-8
10  ∃x, P x  ∃e 1,3-9
11                 Q a → ∃x, P x  →i 2-10
12  ∃x, (P x ∨ ¬Q a) → Q a → ∃x, P x →i 1-11

natural deduction (Gentzen style)

[∃x(P (x) ∨ ¬Q(a))]^{H1}

[P (b) ∨ ¬Q(a)]^{H3}     \frac{[P (b)]^{H4}}{∃x P (x)}∃i \frac{\frac{_{[¬Q(a)]^{H5} [Q(a)]^{H2}}}{⊥} ; ¬e}{∃x P (x)} ; ⊥e
∃x P (x)

∨e [H4,H5]
∃x P (x)

∃e [H3]
Q(a) → ∃x P (x)

→i [H2]

∃x(P (x) ∨ ¬Q(a)) → Q(a) → ∃x P (x)

→i [H1]

                                                     [¬Q a]^{H5}  [Q a]^{H2} ¬e
                                      [P b]^{H4} ∃i  ⊥  ⊥e
                     [P b ∨ ¬Q a]^{H3} ∃x, P x  ∃x, P x  ∨e[H4,H5]
[∃x, (P x ∨ ¬Q a)]^{H1}  ∃x, P x  ∃e[H3]
                             ∃x, P x  →i[H2]
                          Q a → ∃x, P x  →i[H1]
                ∃x, (P x ∨ ¬Q a) → Q a → ∃x, P x

user input

Require Import ProofWeb.
Variable P Q : D -> Prop.
Variable a : D.
Theorem example : exi x, (P(x) \/ ~Q(a)) -> Q(a) -> exi x, P(x).
Proof.
imp_i H1.
imp_i H2.
f_exi_e H1 b H3.
f_dis_e H3 H4 H5.
f_exi_i H4.
fls_e.
f_neg_e H5 H2.
Qed.

exercise colors

possibilities for an exercise :

• Not touched

• Incomplete

• Correct

• Solved demo

                 http://proofweb.cs.ru.nl/

trying ProofWeb three possibilities :

                http://proofweb.cs.ru.nl/

1. guest access (no registration needed)

2. host course in Nijmegen (free)

3. download (open source) and host course on your own system future plans

• other proof display styles • other logics

– modal logics

– temporal logics

– logic in Dijkstra style • MathWiki