jonaprieto/prop-pack

TPTP problems and TSTP solutions of problems in classical propositional logic.

Prop-Pack

prop-pack is a collection of TPTP problems and solutions in classical propositional logic.

• Compendiums of Problems and Solutions in PDF
• Problems
  • Basics
  • Conjunction
  • Implication
  • Disjunction
  • Biconditional
  • Negation
  • Additional Propositional Problems
• References

Compendiums of Problems and Solutions in PDF

• Problems: PDF Version

The solutions are derivations generated by Metis, a theorem prover for first-order logic with equality with good support for TPTP and TSTP file formats.

• Solutions: PDF Version

Problems

Basics

1. ⊢ ⊤
2. ⊢ ¬ ⊥
3. ⊢ p ∨ ¬ p
4. p ⊢ p

Conjunction

1. p , q ⊢ p ⋀ q
2. (p1 ⋀ p2) ⋀ p3 ⊢ p2
3. p ⋀ q ⊢ q ⋀ p
4. q ⋀ p , r ⊢ p ⋀ (r ⋀ q)
5. p1 ⋀ p2 , (q1 ⋀ q2) ⋀ r ⊢ (p1 ⋀ q2) ⋀ r
6. p ⋀ (q ⋀ r) ⊢ (r ⋀ p) ⋀ q

Implication

1. ⊢ p ⇒ p
2. ⊢ p ⇒ (q ⇒ p)
3. p ⇒ q , q ⇒ r ⊢ p ⇒ r
4. ⊢ p ⇒ ((p ⇒ q) ⇒ q)
5. (p ⇒ q) ⇒ (p ⇒ r) ⊢ q ⇒ (p ⇒ r)
6. (p ⇒ q) ⇒ p ⊢ q ⇒ p
7. p ⇒ (q ⇒ r) ⊢ q ⇒ (p ⇒ r)
8. p ⇒ (q ⇒ r) , p ⇒ q ⊢ p ⇒ r
9. (p ⇒ p) ⇒ q ⊢ (q ⇒ r) ⇒ r
10. ⊢ (p ⇒ (q ⇒ r)) ⇒ ((p ⇒ q) ⇒ (p ⇒ r))

Mixed problems with conjunction

11. p ⋀ q ⊢ p ⇒ q
12. ⊢ p ⋀ q ⇒ p
13. p ⇒ (q ⋀ r) ⊢ p ⇒ q
14. ((p ⋀ q) ⇒ p) ⇒ (q ⇒ p) ⊢ q ⇒ p
15. (p ⋀ q) ⇒ r ⊢ p ⇒ (q ⇒ r)
16. (p ⇒ q) ⋀ (p ⇒ r) ⊢ p ⇒ (q ⋀ r)
17. p ⇒ (q ⋀ r) ⊢ (p ⇒ q) ⋀ (p ⇒ r)
18. (((p1 ⋀ p2) ⋀ p3) ⋀ p4) ⋀ p5 ⊢ p1 ⋀ p1

Disjunction

1. p ∨ q ⊢ q ∨ p
2. p ∨ q ⊢ p ∨ (q ∨ r)
3. (p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
4. (p ∨ q) ∨ (r ∨ p1) ⊢ (p ∨ p1) ∨ (r ∨ q)

Mixed problems with conjunction

5. p ⋀ (q ∨ r) ⊢ (p ⋀ q) ∨ (p ⋀ r)
6. (p ∨ q) ⋀ (p ∨ r) ⊢ p ∨ (q ⋀ r)
7. (p ⋀ q) ∨ (p ⋀ r) ⊢ p ⋀ (q ∨ r)
8. p ∨ (q ⋀ r) ⊢ (p ∨ q) ⋀ (p ∨ r)

Mixed problems with implication

9. (p ⇒ q) ∨ q ⊢ p ⇒ q
10. p ∨ q ⊢ (p ⇒ q) ⇒ q
11. (p ⇒ q) ⇒ (p ⇒ r) ⊢ (p ∨ r) ⇒ (q ⇒ r)
12. (p ⇒ q) ∨ (p ⇒ r) ⊢ p ⇒ (q ∨ r)

Mixed problems with conjunction and implication

13. (p ⇒ q) ⋀ (q ⇒ p) ⊢ (p ∨ q) ⇒ (p ⋀ q)
14. (p ∨ q) ⇒ (p ⋀ q) ⊢ (p ⇒ q) ⋀ (q ⇒ p)
15. (q ⇒ r) ⋀ (q ∨ p) ⊢ (p ⇒ q) ⇒ (r ⋀ r)

Biconditional

1. p ⇔ q ⊢ q ⇔ p
2. p , (p ⇔ q) ⇔ r ⊢ q ⇔ r
3. ⊢ (p ⇔ q) ⇔ (q ⇔ p)

Mixed problems

4. (p ∨ q) ⇔ q ⊢ p ⇒ q
5. (p ⋀ q) ⇔ p ⊢ p ⇒ q
6. p ⇒ q ⊢ (p ∨ q) ⇔ q
7. p ⇒ q ⊢ (p ⋀ q) ⇔ p
8. (p ⇒ q) ⋀ (q ⇒ p) ⊢ p ⇔ q
9. ⊢ (p ⋀ q) ⇒ ((p ⇒ q) ⇒ p)
10. ⊢ ((p ⇒ q) ⇒ p) ⇒ (p ⇔ q)
11. ((p ∨ q) ⇔ q) ⇔ p ⊢ p ⇔ q
12. p ⇒ (q ⇔ r) ⊢ (p ⋀ q) ⇔ (p ⋀ r)
13. ⊢ (p ⋀ (q ∨ r)) ⇔ ((p ∨ q) ⋀ (p ∨ r))

Negation

Negation introduction

1. p ⊢ ¬ (¬ p)
2. ¬ p ⊢ ¬ (p ⋀ q)
3. p ⇒ ¬ p ⊢ ¬ p
4. ¬ (p ⇒ q) ⊢ ¬ q
5. ¬ (p ⋀ q) ⊢ p ⇒ ¬ q
6. p ⇒ q ⊢ ¬ q ⇒ ¬ p
7. ⊢ ¬ ((p ⋀ ¬ p) ∨ (q ⋀ ¬ q))
8. ¬ (p ∨ q) ⊢ ¬ p ⋀ ¬ q
9. ¬ p ∨ ¬ q ⊢ ¬ (p ⋀ q)

Ex falso quodlibet

10. ¬ p ⊢ p ⇒ q
11. p ⋀ ¬ p ⊢ q
12. p ∨ q ⊢ ¬ p ⇒ q
13. p ⇒ q , p ⋀ ¬ q ⊢ r
14. p ∨ q , p ⇔ r , ¬ (p ⋀ q) ⊢ r

Indirect proofs

15. ¬ (¬ p) ⊢ p
16. ⊢ p ∨ ¬ p
17. ¬ p ⇒ q ⊢ p ∨ q
18. ¬ (¬ p ∨ ¬ q) ⊢ p ⋀ q
19. ¬ (p ⋀ q) ⊢ ¬ p ∨ ¬ q

Mixed problems

20. ¬ (p ⇒ q) ⊢ p
21. (p ⇒ q) ⇒ p ⊢ p
22. p ⇔ ¬ (¬ q) ⊢ p ⇔ q
23. (p ⇒ q) ⇒ q ⊢ ¬ q ⇒ p
24. ¬ p ⋀ ¬ q ⊢ ¬ (p ∨ q)
25. ⊢ p ∨ (p ⇒ q)
26. ⊢ (p ⇒ q) ∨ (q ⇒ r)
27. ¬ p ⇒ q , r ∨ ¬ q , p ⇒ (q1 ∨ q2) , ¬ r ⋀ ¬ q2 ⊢ q1
28. p ⇒ (q ∨ r) ⊢ (p ⇒ q) ∨ (p ⇒ r)
29. ⊢ ¬ (p ⋀ q) ⇔ (¬ p ∨ ¬ q)
30. ¬ (¬ (¬ p)) ⊢ (¬ p)
31. p ⊢ ¬ (¬ p)
32. ¬ (¬ p) ∧ ¬ (¬ q) ⊢ p ∧ q

Additional Propositional Problems

From Metis sources (some could be repeated from the lists above):

1. ⊢ (p ⇒ q) ⇔ (¬ q ⇒ ¬ p)
2. ⊢ (¬ (¬ p)) ⇔ p
3. ⊢ ¬ (p ⇒ q) ⇒ (q ⇒ p)
4. ⊢ (¬ p ⇒ q) ⇔ (¬ q ⇒ p)
5. ⊢ ((p ∨ q) ⇒ (p ∨ r)) ⇒ (p ∨ (q ⇒ r))
6. ⊢ p ∨ ¬ p
7. ⊢ p ∨ ¬ (¬ (¬ p))
8. ⊢ ((p ⇒ q) ⇒ p) ⇒ p
9. ⊢ ((p ∨ q) ⋀ (¬ p ∨ q) ⋀ (p ∨ ¬ q)) ⇒ (¬ (¬ q ∨ ¬ q))
10. ⊢ ((q ⇒ r) ⋀ (r ⇒ (p ⋀ q)) ⋀ (p ⇒ (q ⋀ r))) ⇒ (p ⇔ q)
11. ⊢ p ⇔ p
12. ⊢ ((p ⇔ q) ⇔ r) ⇔ (p ⇔ (q ⇔ r))
13. ⊢ (p ∨ (q ⋀ r)) ⇔ ((p ∨ q) ⋀ (p ∨ r))
14. ⊢ (p ⇔ q) ⇔ ((q ∨ ¬ p) ⋀ (¬ q ∨ p))
15. ⊢ (p ⇒ q) ⇔ (¬ p ∨ q)
16. ⊢ (p ⇒ q) ∨ (q ⇒ p)
17. ⊢ ((p ⋀ (q ⇒ r)) ⇒ s) ⇔ ((¬ p ∨ q ∨ s) ⋀ (¬ p ∨ ¬ r ∨ s))
18. ⊢ (((a ∨ ¬ k) ⇒ g) ⋀ (g ⇒ q) ⋀ ¬ q) ⇒ k
19. ⊢ ((p ⇒ r) ⋀ (¬ p ⇒ ¬ q) ⋀ (p ∨ q)) ⇒ (p ⋀ r)
20. ⊢ (¬ (¬ (p ⇔ q) ⇔ r)) ⇔ ¬ (p ⇔ ¬ (q ⇔ r))
21. ⊢ ((p ∨ q ∨ r) ⋀ (p ∨ q ∨ ¬ r) ⋀ (p ∨ ¬ q ∨ r) ⋀ (p ∨ ¬ q ∨ ¬ r) ⋀ (¬ p ∨ q ∨ r) ⋀ (¬ p ∨ q ∨ ¬ r) ⋀ (¬ p ∨ ¬ q ∨ r) ⋀ (¬ p ∨ ¬ q ∨ ¬ r)) ⇒ ⊥
22. ⊢ (lit ⇒ clause) ⇒ ((lit ∨ clause) ⇔ clause)
23. ⊢ (¬ (p ⇔ q)) ⇒ ((p ⇒ ¬ q) ⋀ (q ⇒ ¬ p))

References

Many problems have been taken from:

• Carr Alastair, (2017). The Natural Deduction Pack.
• Hurd, John. (2017). Metis Repository. http://gihub.com/gilith/metis