From c79d48a7dd1735759dcd631bd89559678784ec0b Mon Sep 17 00:00:00 2001 From: Jonathan Prieto-Cubides Date: Mon, 7 Aug 2017 22:47:40 -0500 Subject: [PATCH] Problems added from the sources of Metis. --- Makefile | 29 +++- README.md | 264 +++++++++++++++++++------------ problems/prop-metis/prop-01.tptp | 2 + problems/prop-metis/prop-02.tptp | 2 + problems/prop-metis/prop-03.tptp | 2 + problems/prop-metis/prop-04.tptp | 2 + problems/prop-metis/prop-05.tptp | 2 + problems/prop-metis/prop-06.tptp | 2 + problems/prop-metis/prop-07.tptp | 2 + problems/prop-metis/prop-08.tptp | 2 + problems/prop-metis/prop-09.tptp | 3 + problems/prop-metis/prop-10.tptp | 3 + problems/prop-metis/prop-11.tptp | 2 + problems/prop-metis/prop-12.tptp | 3 + problems/prop-metis/prop-13.tptp | 2 + problems/prop-metis/prop-14.tptp | 2 + problems/prop-metis/prop-15.tptp | 2 + problems/prop-metis/prop-16.tptp | 2 + problems/prop-metis/prop-17.tptp | 3 + problems/prop-metis/prop-18.tptp | 2 + problems/prop-metis/prop-19.tptp | 3 + problems/prop-metis/prop-20.tptp | 3 + problems/prop-metis/prop-21.tptp | 5 + problems/prop-metis/prop-22.tptp | 3 + problems/prop-metis/prop-23.tptp | 3 + tptp.tex | 41 ++++- tstp.tex | 31 +++- 27 files changed, 312 insertions(+), 110 deletions(-) create mode 100644 problems/prop-metis/prop-01.tptp create mode 100644 problems/prop-metis/prop-02.tptp create mode 100644 problems/prop-metis/prop-03.tptp create mode 100644 problems/prop-metis/prop-04.tptp create mode 100644 problems/prop-metis/prop-05.tptp create mode 100644 problems/prop-metis/prop-06.tptp create mode 100644 problems/prop-metis/prop-07.tptp create mode 100644 problems/prop-metis/prop-08.tptp create mode 100644 problems/prop-metis/prop-09.tptp create mode 100644 problems/prop-metis/prop-10.tptp create mode 100644 problems/prop-metis/prop-11.tptp create mode 100644 problems/prop-metis/prop-12.tptp create mode 100644 problems/prop-metis/prop-13.tptp create mode 100644 problems/prop-metis/prop-14.tptp create mode 100644 problems/prop-metis/prop-15.tptp create mode 100644 problems/prop-metis/prop-16.tptp create mode 100644 problems/prop-metis/prop-17.tptp create mode 100644 problems/prop-metis/prop-18.tptp create mode 100644 problems/prop-metis/prop-19.tptp create mode 100644 problems/prop-metis/prop-20.tptp create mode 100644 problems/prop-metis/prop-21.tptp create mode 100644 problems/prop-metis/prop-22.tptp create mode 100644 problems/prop-metis/prop-23.tptp diff --git a/Makefile b/Makefile index c8e930a..b7a50a5 100644 --- a/Makefile +++ b/Makefile @@ -20,13 +20,17 @@ TSTP_BICOND := $(addprefix problems/biconditional/,$(notdir $(TPTP_BICOND:.tptp= TPTP_NEG := $(wildcard problems/negation/*.tptp) TSTP_NEG := $(addprefix problems/negation/,$(notdir $(TPTP_NEG:.tptp=.tstp))) +TPTP_PROP_METIS := $(wildcard problems/prop-metis/*.tptp) +TSTP_PROP_METIS := $(addprefix problems/prop-metis/,$(notdir $(TPTP_PROP_METIS:.tptp=.tstp))) + .PHONY: solutions solutions: $(TSTP_BASIC) \ $(TSTP_CONJ) \ $(TSTP_DISJ) \ $(TSTP_IMPL) \ $(TSTP_BICOND) \ - $(TSTP_NEG) + $(TSTP_NEG) \ + $(TSTP_PROP_METIS) @find . -type f -name "cnf*" -delete @echo "ATP: ${ATP}" @@ -60,6 +64,11 @@ negation: $(TSTP_NEG) @find . -type f -name "cnf*" -delete @echo "ATP: ${ATP}" +.PHONY: prop-metis +prop-metis: $(TSTP_PROP_METIS) + @find . -type f -name "cnf*" -delete + @echo "ATP: ${ATP}" + problems/basic/%.tstp: problems/basic/%.tptp @echo $@ @${ATP} $< > $@ @@ -84,6 +93,20 @@ problems/negation/%.tstp: problems/negation/%.tptp @echo $@ @${ATP} $< > $@ +problems/prop-metis/%.tstp: problems/prop-metis/%.tptp + @echo $@ + @${ATP} $< > $@ + + +.PHONY : tex +tex : + make clean + latexmk -pdf tptp.tex + make solutions + latexmk -pdf tstp.tex + latexmk -c + +.PHONY : clean clean: find . -type f -name "*.aux" -delete find . -type f -name "*.DS_Store" -delete @@ -99,3 +122,7 @@ clean: find . -type f -name "*.synctex.gz(busy)" -delete find . -type f -name "*.toc" -delete find . -type f -name "*.tstp" -delete + +.PHONY : default +default : + make tex diff --git a/README.md b/README.md index 06c9a00..9dc7f1d 100644 --- a/README.md +++ b/README.md @@ -1,20 +1,18 @@ # Prop-Pack [![DOI](https://zenodo.org/badge/85266317.svg)](https://zenodo.org/badge/latestdoi/85266317) -*prop-pack* is a collection of [TPTP](http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html) -problems in Classical Propositional Logic and their TSTP solutions. +*prop-pack* is a collection of [TPTP](http://www.cs.miami.edu/¬tptp/TPTP/SyntaxBNF.html) +problems and solutions in classical propositional logic. -* Problems: [PDF Version][tptp] -* Metis's solutions: [PDF Version][tstp] +* Problems: [PDF Version][tptp] [tptp]: https://github.com/jonaprieto/prop-pack/releases/download/v0.2/tptp.pdf -[tstp]: https://github.com/jonaprieto/prop-pack/releases/download/v0.2/tstp.pdf -Many problems (almost everyone) have been taken from: +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. - - Carr Alastair, (2017). *[The Natural Deduction Pack][nd]*. - +* Solutions: [PDF Version][tstp] -[nd]: https://github.com/Alastair-Carr/Natural-Deduction-Pack +[tstp]: https://github.com/jonaprieto/prop-pack/releases/download/v0.2/tstp.pdf ### Problems @@ -26,10 +24,10 @@ Many problems (almost everyone) have been taken from: 3. [ ⊢ p ∨ ¬ p ][basic-3] 4. [ p ⊢ p ][basic-4] -[basic-1]: https://github.com/jonaprieto/ndpack/blob/master/problems/basic/basic-1.tptp -[basic-2]: https://github.com/jonaprieto/ndpack/blob/master/problems/basic/basic-2.tptp -[basic-3]: https://github.com/jonaprieto/ndpack/blob/master/problems/basic/basic-3.tptp -[basic-4]: https://github.com/jonaprieto/ndpack/blob/master/problems/basic/basic-4.tptp +[basic-1]: https://github.com/jonaprieto/prop-pack/blob/master/problems/basic/basic-1.tptp +[basic-2]: https://github.com/jonaprieto/prop-pack/blob/master/problems/basic/basic-2.tptp +[basic-3]: https://github.com/jonaprieto/prop-pack/blob/master/problems/basic/basic-3.tptp +[basic-4]: https://github.com/jonaprieto/prop-pack/blob/master/problems/basic/basic-4.tptp #### Conjunction @@ -40,12 +38,12 @@ Many problems (almost everyone) have been taken from: 5. [ p1 ⋀ p2 , (q1 ⋀ q2) ⋀ r ⊢ (p1 ⋀ q2) ⋀ r ][conj-5] 6. [ p ⋀ (q ⋀ r) ⊢ (r ⋀ p) ⋀ q ][conj-6] -[conj-1]: https://github.com/jonaprieto/ndpack/blob/master/problems/conjunction/conj-1.tptp -[conj-2]: https://github.com/jonaprieto/ndpack/blob/master/problems/conjunction/conj-2.tptp -[conj-3]: https://github.com/jonaprieto/ndpack/blob/master/problems/conjunction/conj-3.tptp -[conj-4]: https://github.com/jonaprieto/ndpack/blob/master/problems/conjunction/conj-4.tptp -[conj-5]: https://github.com/jonaprieto/ndpack/blob/master/problems/conjunction/conj-5.tptp -[conj-6]: https://github.com/jonaprieto/ndpack/blob/master/problems/conjunction/conj-6.tptp +[conj-1]: https://github.com/jonaprieto/prop-pack/blob/master/problems/conjunction/conj-1.tptp +[conj-2]: https://github.com/jonaprieto/prop-pack/blob/master/problems/conjunction/conj-2.tptp +[conj-3]: https://github.com/jonaprieto/prop-pack/blob/master/problems/conjunction/conj-3.tptp +[conj-4]: https://github.com/jonaprieto/prop-pack/blob/master/problems/conjunction/conj-4.tptp +[conj-5]: https://github.com/jonaprieto/prop-pack/blob/master/problems/conjunction/conj-5.tptp +[conj-6]: https://github.com/jonaprieto/prop-pack/blob/master/problems/conjunction/conj-6.tptp #### Implication @@ -72,24 +70,24 @@ Many problems (almost everyone) have been taken from: 17. [ p ⇒ (q ⋀ r) ⊢ (p ⇒ q) ⋀ (p ⇒ r) ][impl-17] 18. [ (((p1 ⋀ p2) ⋀ p3) ⋀ p4) ⋀ p5 ⊢ p1 ⋀ p1 ][impl-18] -[impl-1]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-1.tptp -[impl-2]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-2.tptp -[impl-3]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-3.tptp -[impl-4]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-4.tptp -[impl-5]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-5.tptp -[impl-6]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-6.tptp -[impl-7]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-7.tptp -[impl-8]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-8.tptp -[impl-9]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-9.tptp -[impl-10]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-10.tptp -[impl-11]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-11.tptp -[impl-12]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-12.tptp -[impl-13]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-13.tptp -[impl-14]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-14.tptp -[impl-15]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-15.tptp -[impl-16]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-16.tptp -[impl-17]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-17.tptp -[impl-18]: https://github.com/jonaprieto/ndpack/blob/master/problems/implication/impl-18.tptp +[impl-1]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-1.tptp +[impl-2]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-2.tptp +[impl-3]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-3.tptp +[impl-4]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-4.tptp +[impl-5]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-5.tptp +[impl-6]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-6.tptp +[impl-7]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-7.tptp +[impl-8]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-8.tptp +[impl-9]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-9.tptp +[impl-10]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-10.tptp +[impl-11]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-11.tptp +[impl-12]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-12.tptp +[impl-13]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-13.tptp +[impl-14]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-14.tptp +[impl-15]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-15.tptp +[impl-16]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-16.tptp +[impl-17]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-17.tptp +[impl-18]: https://github.com/jonaprieto/prop-pack/blob/master/problems/implication/impl-18.tptp #### Disjunction @@ -118,21 +116,21 @@ Many problems (almost everyone) have been taken from: 14. [ (p ∨ q) ⇒ (p ⋀ q) ⊢ (p ⇒ q) ⋀ (q ⇒ p)][disj-14] 15. [ (q ⇒ r) ⋀ (q ∨ p) ⊢ (p ⇒ q) ⇒ (r ⋀ r)][disj-15] -[disj-1]: https://github.com/jonaprieto/ndpack/blob/master/problems/disjunction/disj-1.tptp -[disj-2]: https://github.com/jonaprieto/ndpack/blob/master/problems/disjunction/disj-2.tptp -[disj-3]: https://github.com/jonaprieto/ndpack/blob/master/problems/disjunction/disj-3.tptp -[disj-4]: https://github.com/jonaprieto/ndpack/blob/master/problems/disjunction/disj-4.tptp -[disj-5]: https://github.com/jonaprieto/ndpack/blob/master/problems/disjunction/disj-5.tptp -[disj-6]: https://github.com/jonaprieto/ndpack/blob/master/problems/disjunction/disj-6.tptp -[disj-7]: https://github.com/jonaprieto/ndpack/blob/master/problems/disjunction/disj-7.tptp -[disj-8]: https://github.com/jonaprieto/ndpack/blob/master/problems/disjunction/disj-8.tptp -[disj-9]: https://github.com/jonaprieto/ndpack/blob/master/problems/disjunction/disj-9.tptp -[disj-10]: https://github.com/jonaprieto/ndpack/blob/master/problems/disjunction/disj-10.tptp -[disj-11]: https://github.com/jonaprieto/ndpack/blob/master/problems/disjunction/disj-11.tptp -[disj-12]: https://github.com/jonaprieto/ndpack/blob/master/problems/disjunction/disj-12.tptp -[disj-13]: https://github.com/jonaprieto/ndpack/blob/master/problems/disjunction/disj-13.tptp -[disj-14]: https://github.com/jonaprieto/ndpack/blob/master/problems/disjunction/disj-14.tptp -[disj-15]: https://github.com/jonaprieto/ndpack/blob/master/problems/disjunction/disj-15.tptp +[disj-1]: https://github.com/jonaprieto/prop-pack/blob/master/problems/disjunction/disj-1.tptp +[disj-2]: https://github.com/jonaprieto/prop-pack/blob/master/problems/disjunction/disj-2.tptp +[disj-3]: https://github.com/jonaprieto/prop-pack/blob/master/problems/disjunction/disj-3.tptp +[disj-4]: https://github.com/jonaprieto/prop-pack/blob/master/problems/disjunction/disj-4.tptp +[disj-5]: https://github.com/jonaprieto/prop-pack/blob/master/problems/disjunction/disj-5.tptp +[disj-6]: https://github.com/jonaprieto/prop-pack/blob/master/problems/disjunction/disj-6.tptp +[disj-7]: https://github.com/jonaprieto/prop-pack/blob/master/problems/disjunction/disj-7.tptp +[disj-8]: https://github.com/jonaprieto/prop-pack/blob/master/problems/disjunction/disj-8.tptp +[disj-9]: https://github.com/jonaprieto/prop-pack/blob/master/problems/disjunction/disj-9.tptp +[disj-10]: https://github.com/jonaprieto/prop-pack/blob/master/problems/disjunction/disj-10.tptp +[disj-11]: https://github.com/jonaprieto/prop-pack/blob/master/problems/disjunction/disj-11.tptp +[disj-12]: https://github.com/jonaprieto/prop-pack/blob/master/problems/disjunction/disj-12.tptp +[disj-13]: https://github.com/jonaprieto/prop-pack/blob/master/problems/disjunction/disj-13.tptp +[disj-14]: https://github.com/jonaprieto/prop-pack/blob/master/problems/disjunction/disj-14.tptp +[disj-15]: https://github.com/jonaprieto/prop-pack/blob/master/problems/disjunction/disj-15.tptp #### Biconditional @@ -154,19 +152,19 @@ Many problems (almost everyone) have been taken from: 12. [ p ⇒ (q ⇔ r) ⊢ (p ⋀ q) ⇔ (p ⋀ r) ][bicond-12] 13. [ ⊢ (p ⋀ (q ∨ r)) ⇔ ((p ∨ q) ⋀ (p ∨ r)) ][bicond-13] -[bicond-1]: https://github.com/jonaprieto/ndpack/blob/master/problems/biconditional/bicond-1.tptp -[bicond-2]: https://github.com/jonaprieto/ndpack/blob/master/problems/biconditional/bicond-2.tptp -[bicond-3]: https://github.com/jonaprieto/ndpack/blob/master/problems/biconditional/bicond-3.tptp -[bicond-4]: https://github.com/jonaprieto/ndpack/blob/master/problems/biconditional/bicond-4.tptp -[bicond-5]: https://github.com/jonaprieto/ndpack/blob/master/problems/biconditional/bicond-5.tptp -[bicond-6]: https://github.com/jonaprieto/ndpack/blob/master/problems/biconditional/bicond-6.tptp -[bicond-7]: https://github.com/jonaprieto/ndpack/blob/master/problems/biconditional/bicond-7.tptp -[bicond-8]: https://github.com/jonaprieto/ndpack/blob/master/problems/biconditional/bicond-8.tptp -[bicond-9]: https://github.com/jonaprieto/ndpack/blob/master/problems/biconditional/bicond-9.tptp -[bicond-10]: https://github.com/jonaprieto/ndpack/blob/master/problems/biconditional/bicond-10.tptp -[bicond-11]: https://github.com/jonaprieto/ndpack/blob/master/problems/biconditional/bicond-11.tptp -[bicond-12]: https://github.com/jonaprieto/ndpack/blob/master/problems/biconditional/bicond-12.tptp -[bicond-13]: https://github.com/jonaprieto/ndpack/blob/master/problems/biconditional/bicond-13.tptp +[bicond-1]: https://github.com/jonaprieto/prop-pack/blob/master/problems/biconditional/bicond-1.tptp +[bicond-2]: https://github.com/jonaprieto/prop-pack/blob/master/problems/biconditional/bicond-2.tptp +[bicond-3]: https://github.com/jonaprieto/prop-pack/blob/master/problems/biconditional/bicond-3.tptp +[bicond-4]: https://github.com/jonaprieto/prop-pack/blob/master/problems/biconditional/bicond-4.tptp +[bicond-5]: https://github.com/jonaprieto/prop-pack/blob/master/problems/biconditional/bicond-5.tptp +[bicond-6]: https://github.com/jonaprieto/prop-pack/blob/master/problems/biconditional/bicond-6.tptp +[bicond-7]: https://github.com/jonaprieto/prop-pack/blob/master/problems/biconditional/bicond-7.tptp +[bicond-8]: https://github.com/jonaprieto/prop-pack/blob/master/problems/biconditional/bicond-8.tptp +[bicond-9]: https://github.com/jonaprieto/prop-pack/blob/master/problems/biconditional/bicond-9.tptp +[bicond-10]: https://github.com/jonaprieto/prop-pack/blob/master/problems/biconditional/bicond-10.tptp +[bicond-11]: https://github.com/jonaprieto/prop-pack/blob/master/problems/biconditional/bicond-11.tptp +[bicond-12]: https://github.com/jonaprieto/prop-pack/blob/master/problems/biconditional/bicond-12.tptp +[bicond-13]: https://github.com/jonaprieto/prop-pack/blob/master/problems/biconditional/bicond-13.tptp #### Negation @@ -215,46 +213,102 @@ Many problems (almost everyone) have been taken from: 31. [ p ⊢ ¬ (¬ p) ][neg-31] 32. [ ¬ (¬ p) ∧ ¬ (¬ q) ⊢ p ∧ q ][neg-32] +[neg-1]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-1.tptp +[neg-2]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-2.tptp +[neg-3]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-3.tptp +[neg-4]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-4.tptp +[neg-5]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-5.tptp +[neg-6]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-6.tptp +[neg-7]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-7.tptp +[neg-8]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-8.tptp +[neg-9]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-9.tptp +[neg-10]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-10.tptp +[neg-11]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-11.tptp +[neg-12]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-12.tptp +[neg-13]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-13.tptp +[neg-14]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-14.tptp +[neg-15]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-15.tptp +[neg-16]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-16.tptp +[neg-17]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-17.tptp +[neg-18]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-18.tptp +[neg-19]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-19.tptp +[neg-20]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-20.tptp +[neg-21]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-21.tptp +[neg-22]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-22.tptp +[neg-23]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-23.tptp +[neg-24]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-24.tptp +[neg-25]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-25.tptp +[neg-26]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-26.tptp +[neg-27]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-27.tptp +[neg-28]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-28.tptp +[neg-29]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-29.tptp +[neg-30]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-30.tptp +[neg-31]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-31.tptp +[neg-32]: https://github.com/jonaprieto/prop-pack/blob/master/problems/negation/neg-32.tptp + +#### Additional Propositional Problems + +From Metis sources (some could be repeated from the lists above): + + 1. [ ⊢ (p ⇒ q) ⇔ (¬ q ⇒ ¬ p) ][prop-1] + 2. [ ⊢ (¬ (¬ p)) ⇔ p ][prop-2] + 3. [ ⊢ ¬ (p ⇒ q) ⇒ (q ⇒ p) ][prop-3] + 4. [ ⊢ (¬ p ⇒ q) ⇔ (¬ q ⇒ p) ][prop-4] + 5. [ ⊢ ((p ∨ q) ⇒ (p ∨ r)) ⇒ (p ∨ (q ⇒ r)) ][prop-5] + 6. [ ⊢ p ∨ ¬ p ][prop-6] + 7. [ ⊢ p ∨ ¬ (¬ (¬ p)) ][prop-7] + 8. [ ⊢ ((p ⇒ q) ⇒ p) ⇒ p ][prop-8] + 9. [ ⊢ ((p ∨ q) ⋀ (¬ p ∨ q) ⋀ (p ∨ ¬ q)) ⇒ (¬ (¬ q ∨ ¬ q)) ][prop-9] + 10. [ ⊢ ((q ⇒ r) ⋀ (r ⇒ (p ⋀ q)) ⋀ (p ⇒ (q ⋀ r))) ⇒ (p ⇔ q) ][prop-10] + 11. [ ⊢ p ⇔ p ][prop-11] + 12. [ ⊢ ((p ⇔ q) ⇔ r) ⇔ (p ⇔ (q ⇔ r)) ][prop-12] + 13. [ ⊢ (p ∨ (q ⋀ r)) ⇔ ((p ∨ q) ⋀ (p ∨ r)) ][prop-13] + 14. [ ⊢ (p ⇔ q) ⇔ ((q ∨ ¬ p) ⋀ (¬ q ∨ p)) ][prop-14] + 15. [ ⊢ (p ⇒ q) ⇔ (¬ p ∨ q) ][prop-15] + 16. [ ⊢ (p ⇒ q) ∨ (q ⇒ p) ][prop-16] + 17. [ ⊢ ((p ⋀ (q ⇒ r)) ⇒ s) ⇔ ((¬ p ∨ q ∨ s) ⋀ (¬ p ∨ ¬ r ∨ s)) ][prop-17] + 18. [ ⊢ (((a ∨ ¬ k) ⇒ g) ⋀ (g ⇒ q) ⋀ ¬ q) ⇒ k ][prop-18] + 19. [ ⊢ ((p ⇒ r) ⋀ (¬ p ⇒ ¬ q) ⋀ (p ∨ q)) ⇒ (p ⋀ r) ][prop-19] + 20. [ ⊢ (¬ (¬ (p ⇔ q) ⇔ r)) ⇔ ¬ (p ⇔ ¬ (q ⇔ r)) ][prop-20] + 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)) ⇒ $false ][prop-21] + 22. [ ⊢ (lit ⇒ clause) ⇒ ((lit ∨ clause) ⇔ clause) ][prop-22] + 23. [ ⊢ (¬ (p ⇔ q)) ⇒ ((p ⇒ ¬ q) ⋀ (q ⇒ ¬ p)) ][prop-23] + +[prop-1]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-1.tptp +[prop-2]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-2.tptp +[prop-3]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-3.tptp +[prop-4]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-4.tptp +[prop-5]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-5.tptp +[prop-6]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-6.tptp +[prop-7]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-7.tptp +[prop-8]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-8.tptp +[prop-9]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-9.tptp +[prop-10]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-10.tptp +[prop-11]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-11.tptp +[prop-12]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-12.tptp +[prop-13]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-13.tptp +[prop-14]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-14.tptp +[prop-15]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-15.tptp +[prop-16]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-16.tptp +[prop-17]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-17.tptp +[prop-18]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-18.tptp +[prop-19]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-19.tptp +[prop-20]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-20.tptp +[prop-21]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-21.tptp +[prop-22]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-22.tptp +[prop-23]: https://github.com/jonaprieto/prop-pack/blob/master/problems/prop-pack/prop-23.tptp + +### References + +Many problems have been taken from: + + - Carr Alastair, (2017). *[The Natural Deduction Pack][nd]*. + + +[nd]: https://github.com/Alastair-Carr/Natural-Deduction-Pack + -[neg-1]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-1.tptp -[neg-2]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-2.tptp -[neg-3]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-3.tptp -[neg-4]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-4.tptp -[neg-5]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-5.tptp -[neg-6]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-6.tptp -[neg-7]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-7.tptp -[neg-8]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-8.tptp -[neg-9]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-9.tptp -[neg-10]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-10.tptp -[neg-11]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-11.tptp -[neg-12]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-12.tptp -[neg-13]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-13.tptp -[neg-14]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-14.tptp -[neg-15]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-15.tptp -[neg-16]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-16.tptp -[neg-17]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-17.tptp -[neg-18]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-18.tptp -[neg-19]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-19.tptp -[neg-20]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-20.tptp -[neg-21]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-21.tptp -[neg-22]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-22.tptp -[neg-23]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-23.tptp -[neg-24]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-24.tptp -[neg-25]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-25.tptp -[neg-26]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-26.tptp -[neg-27]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-27.tptp -[neg-28]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-28.tptp -[neg-29]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-29.tptp -[neg-30]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-30.tptp -[neg-31]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-31.tptp -[neg-32]: https://github.com/jonaprieto/ndpack/blob/master/problems/negation/neg-32.tptp - - -### PDF Documents - -We provide two latex files: - - - The problems in `tptp` file format are in the `tptp.tex` file and, - - Their solutions using [Metis][metis] Prover `tstp` file format are in the `tstp.tex` file. [metis]: http://github.com/gilith/metis diff --git a/problems/prop-metis/prop-01.tptp b/problems/prop-metis/prop-01.tptp new file mode 100644 index 0000000..44e173d --- /dev/null +++ b/problems/prop-metis/prop-01.tptp @@ -0,0 +1,2 @@ +% ----------------------------------------------------------------------------- +fof(PROP_1, conjecture, (p => q) <=> (~ q => ~ p)). diff --git a/problems/prop-metis/prop-02.tptp b/problems/prop-metis/prop-02.tptp new file mode 100644 index 0000000..bf062f3 --- /dev/null +++ b/problems/prop-metis/prop-02.tptp @@ -0,0 +1,2 @@ +% ----------------------------------------------------------------------------- +fof(PROP_2, conjecture, (~ (~ p)) <=> p). \ No newline at end of file diff --git a/problems/prop-metis/prop-03.tptp b/problems/prop-metis/prop-03.tptp new file mode 100644 index 0000000..87d34f3 --- /dev/null +++ b/problems/prop-metis/prop-03.tptp @@ -0,0 +1,2 @@ +% ----------------------------------------------------------------------------- +fof(PROP_3, conjecture, ~ (p => q) => (q => p)). diff --git a/problems/prop-metis/prop-04.tptp b/problems/prop-metis/prop-04.tptp new file mode 100644 index 0000000..398637e --- /dev/null +++ b/problems/prop-metis/prop-04.tptp @@ -0,0 +1,2 @@ +% ----------------------------------------------------------------------------- +fof(PROP_4, conjecture, (~ p => q) <=> (~ q => p)). diff --git a/problems/prop-metis/prop-05.tptp b/problems/prop-metis/prop-05.tptp new file mode 100644 index 0000000..4a4d263 --- /dev/null +++ b/problems/prop-metis/prop-05.tptp @@ -0,0 +1,2 @@ +% ----------------------------------------------------------------------------- +fof(PROP_5, conjecture, ((p | q) => (p | r)) => (p | (q => r))). diff --git a/problems/prop-metis/prop-06.tptp b/problems/prop-metis/prop-06.tptp new file mode 100644 index 0000000..31c439b --- /dev/null +++ b/problems/prop-metis/prop-06.tptp @@ -0,0 +1,2 @@ +% ----------------------------------------------------------------------------- +fof(PROP_6, conjecture, p | ~ p). diff --git a/problems/prop-metis/prop-07.tptp b/problems/prop-metis/prop-07.tptp new file mode 100644 index 0000000..f81d968 --- /dev/null +++ b/problems/prop-metis/prop-07.tptp @@ -0,0 +1,2 @@ +% ----------------------------------------------------------------------------- +fof(PROP_7, conjecture, p | ~ (~ (~ p)) ). diff --git a/problems/prop-metis/prop-08.tptp b/problems/prop-metis/prop-08.tptp new file mode 100644 index 0000000..bd77d98 --- /dev/null +++ b/problems/prop-metis/prop-08.tptp @@ -0,0 +1,2 @@ +% ----------------------------------------------------------------------------- +fof(PROP_8, conjecture, ((p => q) => p) => p). diff --git a/problems/prop-metis/prop-09.tptp b/problems/prop-metis/prop-09.tptp new file mode 100644 index 0000000..2578be4 --- /dev/null +++ b/problems/prop-metis/prop-09.tptp @@ -0,0 +1,3 @@ +% ----------------------------------------------------------------------------- +fof(PROP_9, conjecture, + ((p | q) & (~ p | q) & (p | ~ q)) => (~ (~ q | ~ q))). diff --git a/problems/prop-metis/prop-10.tptp b/problems/prop-metis/prop-10.tptp new file mode 100644 index 0000000..d5074e9 --- /dev/null +++ b/problems/prop-metis/prop-10.tptp @@ -0,0 +1,3 @@ +% ----------------------------------------------------------------------------- +fof(PROP_10, conjecture, + ((q => r) & (r => (p & q)) & (p => (q & r))) => (p <=> q)). diff --git a/problems/prop-metis/prop-11.tptp b/problems/prop-metis/prop-11.tptp new file mode 100644 index 0000000..6fd6b8e --- /dev/null +++ b/problems/prop-metis/prop-11.tptp @@ -0,0 +1,2 @@ +% ----------------------------------------------------------------------------- +fof(PROP_11, conjecture, p <=> p). diff --git a/problems/prop-metis/prop-12.tptp b/problems/prop-metis/prop-12.tptp new file mode 100644 index 0000000..bbd071e --- /dev/null +++ b/problems/prop-metis/prop-12.tptp @@ -0,0 +1,3 @@ +% ----------------------------------------------------------------------------- +fof(PROP_12, conjecture, + ((p <=> q) <=> r) <=> (p <=> (q <=> r))). diff --git a/problems/prop-metis/prop-13.tptp b/problems/prop-metis/prop-13.tptp new file mode 100644 index 0000000..f8f75de --- /dev/null +++ b/problems/prop-metis/prop-13.tptp @@ -0,0 +1,2 @@ +% ----------------------------------------------------------------------------- +fof(PROP_13, conjecture, (p | (q & r)) <=> ((p | q) & (p | r))). diff --git a/problems/prop-metis/prop-14.tptp b/problems/prop-metis/prop-14.tptp new file mode 100644 index 0000000..b46c743 --- /dev/null +++ b/problems/prop-metis/prop-14.tptp @@ -0,0 +1,2 @@ +% ----------------------------------------------------------------------------- +fof(PROP_14, conjecture, (p <=> q) <=> ((q | ~ p) & (~ q | p))). diff --git a/problems/prop-metis/prop-15.tptp b/problems/prop-metis/prop-15.tptp new file mode 100644 index 0000000..f3e1daa --- /dev/null +++ b/problems/prop-metis/prop-15.tptp @@ -0,0 +1,2 @@ +% ----------------------------------------------------------------------------- +fof(PROP_15, conjecture, (p => q) <=> (~ p | q)). diff --git a/problems/prop-metis/prop-16.tptp b/problems/prop-metis/prop-16.tptp new file mode 100644 index 0000000..cde5989 --- /dev/null +++ b/problems/prop-metis/prop-16.tptp @@ -0,0 +1,2 @@ +% ----------------------------------------------------------------------------- +fof(PROP_16, conjecture, (p => q) | (q => p)). diff --git a/problems/prop-metis/prop-17.tptp b/problems/prop-metis/prop-17.tptp new file mode 100644 index 0000000..db36677 --- /dev/null +++ b/problems/prop-metis/prop-17.tptp @@ -0,0 +1,3 @@ +% ----------------------------------------------------------------------------- +fof(PROP_17, conjecture, + ((p & (q => r)) => s) <=> ((~ p | q | s) & (~ p | ~ r | s))). diff --git a/problems/prop-metis/prop-18.tptp b/problems/prop-metis/prop-18.tptp new file mode 100644 index 0000000..817e77f --- /dev/null +++ b/problems/prop-metis/prop-18.tptp @@ -0,0 +1,2 @@ +% ----------------------------------------------------------------------------- +fof(MATHS4_EXAMPLE, conjecture, (((a | ~ k) => g) & (g => q) & ~ q) => k). diff --git a/problems/prop-metis/prop-19.tptp b/problems/prop-metis/prop-19.tptp new file mode 100644 index 0000000..4fe032f --- /dev/null +++ b/problems/prop-metis/prop-19.tptp @@ -0,0 +1,3 @@ +% ----------------------------------------------------------------------------- +fof(LOGICPROOF_1996, conjecture, + ((p => r) & (~ p => ~ q) & (p | q)) => (p & r)). diff --git a/problems/prop-metis/prop-20.tptp b/problems/prop-metis/prop-20.tptp new file mode 100644 index 0000000..d289dbf --- /dev/null +++ b/problems/prop-metis/prop-20.tptp @@ -0,0 +1,3 @@ +% ----------------------------------------------------------------------------- +fof(XOR_ASSOC, conjecture, + (~ (~ (p <=> q) <=> r)) <=> ~ (p <=> ~ (q <=> r))). diff --git a/problems/prop-metis/prop-21.tptp b/problems/prop-metis/prop-21.tptp new file mode 100644 index 0000000..b97e62c --- /dev/null +++ b/problems/prop-metis/prop-21.tptp @@ -0,0 +1,5 @@ +% ----------------------------------------------------------------------------- +fof(ALL_3_CLAUSES, conjecture, + ((p | q | r) & (p | q | ~ r) & (p | ~ q | r) & (p | ~ q | ~ r) & + (~ p | q | r) & (~ p | q | ~ r) & (~ p | ~ q | r) & + (~ p | ~ q | ~ r)) => $false ). diff --git a/problems/prop-metis/prop-22.tptp b/problems/prop-metis/prop-22.tptp new file mode 100644 index 0000000..9e08044 --- /dev/null +++ b/problems/prop-metis/prop-22.tptp @@ -0,0 +1,3 @@ +% ----------------------------------------------------------------------------- +fof(CLAUSE_SIMP, conjecture, + (lit => clause) => ((lit | clause) <=> clause)). diff --git a/problems/prop-metis/prop-23.tptp b/problems/prop-metis/prop-23.tptp new file mode 100644 index 0000000..11c1451 --- /dev/null +++ b/problems/prop-metis/prop-23.tptp @@ -0,0 +1,3 @@ +% ----------------------------------------------------------------------------- +fof(SPLIT_NOT_IFF, conjecture, + (~ (p <=> q)) => ((p => ~ q) & (q => ~ p))). diff --git a/tptp.tex b/tptp.tex index 25b306a..e663633 100644 --- a/tptp.tex +++ b/tptp.tex @@ -98,7 +98,12 @@ \tableofcontents \section{\tptp Format} -The \tptp format is a precise and accurate language to describe without ambiguities problems written in a logic. It attempts to be a standard for all Automatic Theorems Provers (ATP). The syntax of the TPTP format is based on the Prolog language and endeavors to be processed with a similar parser for such a language\footnote{\tptp v6.4.0~\url{http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html}}.\par +The \tptp format is a precise and accurate language to describe without +ambiguities problems written in a logic. It attempts to be a standard for +all Automatic Theorems Provers (ATP). The syntax of the TPTP format is based +on the Prolog language and endeavors to be processed with a similar parser for +such a language +\footnote{\tptp v6.4.0~\url{http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html}}. The following is an example taken from the \tptp Problems repository\footnote{\url{http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems}}. @@ -108,7 +113,9 @@ \section{\tptp Format} cnf(an_2, axiom, (is_a_theorem(or(not(or(X,Y)) , or(Y,X))) )). \end{lstlisting} -We present a subset of \tptp that use for first-order logic the keyword \ttext{fof} and the keyword \ttext{cnf} to use the clause normal form. Their grammars are as follows. +We present a subset of \tptp that use for first-order logic the keyword +\ttext{fof} and the keyword \ttext{cnf} to use the clause normal form. +Their grammars are as follows. \label{syntax:fof} \begin{grammar} @@ -256,10 +263,38 @@ \subsection{Negation} \problemtptp[neg-31.tptp]{problems/negation/neg-31.tptp}{2} \problemtptp[neg-32.tptp]{problems/negation/neg-32.tptp}{2} + +\subsection{Additional Propositional Problems} + +\problemtptp[prop-01.tptp]{problems/prop-metis/prop-01.tptp}{2} +\problemtptp[prop-02.tptp]{problems/prop-metis/prop-02.tptp}{2} +\problemtptp[prop-03.tptp]{problems/prop-metis/prop-03.tptp}{2} +\problemtptp[prop-04.tptp]{problems/prop-metis/prop-04.tptp}{2} +\problemtptp[prop-05.tptp]{problems/prop-metis/prop-05.tptp}{2} +\problemtptp[prop-06.tptp]{problems/prop-metis/prop-06.tptp}{2} +\problemtptp[prop-07.tptp]{problems/prop-metis/prop-07.tptp}{2} +\problemtptp[prop-08.tptp]{problems/prop-metis/prop-08.tptp}{2} +\problemtptp[prop-09.tptp]{problems/prop-metis/prop-09.tptp}{2} +\problemtptp[prop-10.tptp]{problems/prop-metis/prop-10.tptp}{2} +\problemtptp[prop-11.tptp]{problems/prop-metis/prop-11.tptp}{2} +\problemtptp[prop-12.tptp]{problems/prop-metis/prop-12.tptp}{2} +\problemtptp[prop-13.tptp]{problems/prop-metis/prop-13.tptp}{2} +\problemtptp[prop-14.tptp]{problems/prop-metis/prop-14.tptp}{2} +\problemtptp[prop-15.tptp]{problems/prop-metis/prop-15.tptp}{2} +\problemtptp[prop-16.tptp]{problems/prop-metis/prop-16.tptp}{2} +\problemtptp[prop-17.tptp]{problems/prop-metis/prop-17.tptp}{2} +\problemtptp[prop-18.tptp]{problems/prop-metis/prop-18.tptp}{2} +\problemtptp[prop-19.tptp]{problems/prop-metis/prop-19.tptp}{2} +\problemtptp[prop-20.tptp]{problems/prop-metis/prop-20.tptp}{2} +\problemtptp[prop-21.tptp]{problems/prop-metis/prop-21.tptp}{2} +\problemtptp[prop-22.tptp]{problems/prop-metis/prop-22.tptp}{2} +\problemtptp[prop-23.tptp]{problems/prop-metis/prop-23.tptp}{2} + \section{References} \begin{thebibliography}{9} \bibitem{alastair2017} -Car Alastair (2017). \textit{The Natural Deduction Pack}. Revisited edition, Feb. 2017. +Car Alastair (2017). \textit{The Natural Deduction Pack}. +Revisited edition, Feb. 2017. \end{thebibliography} \end{document} diff --git a/tstp.tex b/tstp.tex index a17f744..05b77c2 100644 --- a/tstp.tex +++ b/tstp.tex @@ -99,7 +99,7 @@ \tableofcontents \section{TSTP Proofs} -Metis ATP (2.3 - release 20170315) found these solutions. +Metis Prover (2.3 - release 20170315) found these solutions. \subsection{Basic} \solutiontstp[basic-1.tptp]{problems/basic/basic-1.tstp} \solutiontstp[basic-2.tptp]{problems/basic/basic-2.tstp} @@ -204,4 +204,33 @@ \subsection{Negation} \solutiontstp[neg-31.tptp]{problems/negation/neg-31.tstp} \solutiontstp[neg-32.tptp]{problems/negation/neg-32.tstp} +\subsection{Additional Propositional Problems} +The following problems were extracted from a list of problems in +the repository of source code of Metis +\footnote{\url{https://github.com/gilith/metis/blob/f0b1a17cd57eb098077e963ab092477aee9fb340/src/problems.sml}}. + +\solutiontstp[prop-01.tstp]{problems/prop-metis/prop-01.tstp} +\solutiontstp[prop-02.tstp]{problems/prop-metis/prop-02.tstp} +\solutiontstp[prop-03.tstp]{problems/prop-metis/prop-03.tstp} +\solutiontstp[prop-04.tstp]{problems/prop-metis/prop-04.tstp} +\solutiontstp[prop-05.tstp]{problems/prop-metis/prop-05.tstp} +\solutiontstp[prop-06.tstp]{problems/prop-metis/prop-06.tstp} +\solutiontstp[prop-07.tstp]{problems/prop-metis/prop-07.tstp} +\solutiontstp[prop-08.tstp]{problems/prop-metis/prop-08.tstp} +\solutiontstp[prop-09.tstp]{problems/prop-metis/prop-09.tstp} +\solutiontstp[prop-10.tstp]{problems/prop-metis/prop-10.tstp} +\solutiontstp[prop-11.tstp]{problems/prop-metis/prop-11.tstp} +\solutiontstp[prop-12.tstp]{problems/prop-metis/prop-12.tstp} +\solutiontstp[prop-13.tstp]{problems/prop-metis/prop-13.tstp} +\solutiontstp[prop-14.tstp]{problems/prop-metis/prop-14.tstp} +\solutiontstp[prop-15.tstp]{problems/prop-metis/prop-15.tstp} +\solutiontstp[prop-16.tstp]{problems/prop-metis/prop-16.tstp} +\solutiontstp[prop-17.tstp]{problems/prop-metis/prop-17.tstp} +\solutiontstp[prop-18.tstp]{problems/prop-metis/prop-18.tstp} +\solutiontstp[prop-19.tstp]{problems/prop-metis/prop-19.tstp} +\solutiontstp[prop-20.tstp]{problems/prop-metis/prop-20.tstp} +\solutiontstp[prop-21.tstp]{problems/prop-metis/prop-21.tstp} +\solutiontstp[prop-22.tstp]{problems/prop-metis/prop-22.tstp} +\solutiontstp[prop-23.tstp]{problems/prop-metis/prop-23.tstp} + \end{document}