Jitpro Exercises 3: Refuing PLNc Formulas

In each example, you will refute a set A of closed PLN formulas. The elements of A are given as axioms. To put each formula on the branch, press the button that says Import Axiom or Lemma and choose the formula to import. (You can ignore "claim false" which will put ¬false on the branch.)

Jitpro Exercise 3.1

Jitpro Exercise 3.2

Jitpro Exercise 3.3

Jitpro Exercise 3.4

This exercise is probably too hard. Don't be disappointed if you have trouble. Ask for hints!