BibSonomy ::  tag ::

order by ( date | folkrank )

ProofWeb is a system for practising natural deduction on the computer based on the Coq proof assistant and runs in browser. ProofWeb one runs logic exercises on a web server. ProofWeb comes with a database of basic logic exercises that are graded according to difficulty. The ProofWeb system automatically grades the exercises of the students. user talks to the Coq system on the server without any translation. There just are a few additional tactics to make Coq's behavior follow the logic textbooks. This means that in ProofWeb the full power of Coq is available, even to beginner students. On the other hand ProofWeb tries hard to present deductions exactly the way they look in the textbooks. In particular ProofWeb exactly follows the conventions of a well-known logic textbook Logic in Computer Science: Modelling and Reasoning about Systems by Michael Huth and Mark Ryan.