teaching.bb-ai.net/KRR/Prover9

Propositional Logic Exercises for Prover9

This is a set of formative exercises designed to teach you the skills of encoding problems into propositional logic representation and solving them using an automated theorem prover.

Note that what is called propositional logic is a logical language that only has propositional letter symbols (representing atomic statements that are either true or false) and truth-functional connectives.

The Problems:

  1. The Stolen Diamond (10 marks)
  2. The Lost Key (10 marks)
  3. Rembrandt's Picture (8 marks)
  4. Sunday is a Holiday (12 marks)
  5. Tarquin's Wisdom (12 marks)
  6. The Tennis Lover (8 marks)
  7. An Appointment (8 marks)
  8. Dry Thunder (8 marks)
  9. Angry Dragons (10 marks)

Total marks available: 86

Gradescope
If you are taking one of Brandon's KRR modules, your solutions can be checked and marked automatically using software that has been implemented by embedding Prover9 within the Gradescope platform. Follow the link to Gradescope on the 'Submit My Work' page of the module's Minerva web pages, and look for the assignment: Propositional Logic Exercises