Skip to content
This repository has been archived by the owner on Jul 1, 2020. It is now read-only.
/ prop-pack Public archive

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

License

Notifications You must be signed in to change notification settings

jonaprieto/prop-pack

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

51 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Prop-Pack DOI

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

Compendiums of Problems and Solutions in PDF

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.

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

  1. p ⋀ q ⊢ p ⇒ q
  2. ⊢ p ⋀ q ⇒ p
  3. p ⇒ (q ⋀ r) ⊢ p ⇒ q
  4. ((p ⋀ q) ⇒ p) ⇒ (q ⇒ p) ⊢ q ⇒ p
  5. (p ⋀ q) ⇒ r ⊢ p ⇒ (q ⇒ r)
  6. (p ⇒ q) ⋀ (p ⇒ r) ⊢ p ⇒ (q ⋀ r)
  7. p ⇒ (q ⋀ r) ⊢ (p ⇒ q) ⋀ (p ⇒ r)
  8. (((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

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

Mixed problems with implication

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

Mixed problems with conjunction and implication

  1. (p ⇒ q) ⋀ (q ⇒ p) ⊢ (p ∨ q) ⇒ (p ⋀ q)
  2. (p ∨ q) ⇒ (p ⋀ q) ⊢ (p ⇒ q) ⋀ (q ⇒ p)
  3. (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

  1. (p ∨ q) ⇔ q ⊢ p ⇒ q
  2. (p ⋀ q) ⇔ p ⊢ p ⇒ q
  3. p ⇒ q ⊢ (p ∨ q) ⇔ q
  4. p ⇒ q ⊢ (p ⋀ q) ⇔ p
  5. (p ⇒ q) ⋀ (q ⇒ p) ⊢ p ⇔ q
  6. ⊢ (p ⋀ q) ⇒ ((p ⇒ q) ⇒ p)
  7. ⊢ ((p ⇒ q) ⇒ p) ⇒ (p ⇔ q)
  8. ((p ∨ q) ⇔ q) ⇔ p ⊢ p ⇔ q
  9. p ⇒ (q ⇔ r) ⊢ (p ⋀ q) ⇔ (p ⋀ r)
  10. ⊢ (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

  1. ¬ p ⊢ p ⇒ q
  2. p ⋀ ¬ p ⊢ q
  3. p ∨ q ⊢ ¬ p ⇒ q
  4. p ⇒ q , p ⋀ ¬ q ⊢ r
  5. p ∨ q , p ⇔ r , ¬ (p ⋀ q) ⊢ r

Indirect proofs

  1. ¬ (¬ p) ⊢ p
  2. ⊢ p ∨ ¬ p
  3. ¬ p ⇒ q ⊢ p ∨ q
  4. ¬ (¬ p ∨ ¬ q) ⊢ p ⋀ q
  5. ¬ (p ⋀ q) ⊢ ¬ p ∨ ¬ q

Mixed problems

  1. ¬ (p ⇒ q) ⊢ p
  2. (p ⇒ q) ⇒ p ⊢ p
  3. p ⇔ ¬ (¬ q) ⊢ p ⇔ q
  4. (p ⇒ q) ⇒ q ⊢ ¬ q ⇒ p
  5. ¬ p ⋀ ¬ q ⊢ ¬ (p ∨ q)
  6. ⊢ p ∨ (p ⇒ q)
  7. ⊢ (p ⇒ q) ∨ (q ⇒ r)
  8. ¬ p ⇒ q , r ∨ ¬ q , p ⇒ (q1 ∨ q2) , ¬ r ⋀ ¬ q2 ⊢ q1
  9. p ⇒ (q ∨ r) ⊢ (p ⇒ q) ∨ (p ⇒ r)
  10. ⊢ ¬ (p ⋀ q) ⇔ (¬ p ∨ ¬ q)
  11. ¬ (¬ (¬ p)) ⊢ (¬ p)
  12. p ⊢ ¬ (¬ p)
  13. ¬ (¬ 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:

About

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

Topics

Resources

License

Stars

Watchers

Forks

Packages

No packages published