teaching.bb-ai.net/KRR/Prover9

Introductory First-Order Logic Exercises for Prover9

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

The Problems:

  1. A Famous Syllogism (6 marks)
  2. Furry Reptiles (6 marks)
  3. Homework is Fun (6 marks)
  4. Web sites (6 marks)
  5. Greedy Rabbits (6 marks)
  6. Young Rabbits (8 marks)
  7. An Invalid Syllogism (6 marks)
  8. Socrates (8 marks)
  9. Porky (10 marks)
  10. Jabberwock (8 marks)
  11. Balloonig Pigs (22 marks)

Total marks available: 92

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: 1st-Order Logic Exercises