Problems added from the sources of Metis.

jonaprieto · Aug 8, 2017 · c79d48a · c79d48a
1 parent 775d2a6
commit c79d48a
Show file tree

Hide file tree

Showing 27 changed files with 312 additions and 110 deletions.
diff --git 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
diff --git a/problems/prop-metis/prop-01.tptp 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
@@ -0,0 +1,2 @@
+% -----------------------------------------------------------------------------
+fof(PROP_2, conjecture, (~ (~ p)) <=> p).
diff --git a/problems/prop-metis/prop-03.tptp 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -0,0 +1,3 @@
+% -----------------------------------------------------------------------------
+fof(SPLIT_NOT_IFF, conjecture,
+    (~ (p <=> q)) => ((p => ~ q) & (q => ~ p))).
diff --git 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
@@ -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}