818 |
818 |
819 text{*Problem 71, as found in TPTP (SYN007+1.005)*} |
819 text{*Problem 71, as found in TPTP (SYN007+1.005)*} |
820 lemma "p1 = (p2 = (p3 = (p4 = (p5 = (p1 = (p2 = (p3 = (p4 = p5))))))))" |
820 lemma "p1 = (p2 = (p3 = (p4 = (p5 = (p1 = (p2 = (p3 = (p4 = p5))))))))" |
821 by blast |
821 by blast |
822 |
822 |
|
823 |
|
824 subsection{*Examples of proof reconstruction*} |
|
825 |
823 text{*A manual resolution proof of problem 19.*} |
826 text{*A manual resolution proof of problem 19.*} |
824 lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))" |
827 lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))" |
825 proof (rule ccontr, skolemize, make_clauses) |
828 proof (rule ccontr, skolemize, make_clauses) |
826 fix x |
829 fix x |
827 assume P: "\<And>U. \<not> P U \<Longrightarrow> False" |
830 assume P: "\<And>U. \<not> P U \<Longrightarrow> False" |
828 and Q: "\<And>U. Q U \<Longrightarrow> False" |
831 and Q: "\<And>U. Q U \<Longrightarrow> False" |
829 and PQ: "\<lbrakk>P x; \<not> Q x\<rbrakk> \<Longrightarrow> False" |
832 and PQ: "\<lbrakk>P x; \<not> Q x\<rbrakk> \<Longrightarrow> False" |
830 have cl4: "\<And>U. \<not> Q x \<Longrightarrow> False" |
833 have cl4: "\<And>U. \<not> Q x \<Longrightarrow> False" |
831 by (rule P [binary 0 PQ 0]) |
834 by (meson P PQ) |
832 show "False" |
835 show "False" |
833 by (rule Q [binary 0 cl4 0]) |
836 by (meson Q cl4) |
834 qed |
837 qed |
835 |
838 |
|
839 |
|
840 text{*A lengthy proof of a significant theorem.*} |
|
841 |
|
842 lemmas subsetI_0 = subsetI[skolem, clausify 0] |
|
843 lemmas subsetI_1 = subsetI[skolem, clausify 1] |
|
844 |
|
845 lemma singleton_example_1: |
|
846 "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}" |
|
847 proof (rule ccontr, skolemize, make_clauses) |
|
848 fix S :: "'a set set" |
|
849 assume CL1: "\<And>Z. S \<subseteq> {Z} \<Longrightarrow> False" |
|
850 and CL2: "\<And>X Y. \<lbrakk>X \<in> S; Y \<in> S; \<not> X \<subseteq> Y\<rbrakk> \<Longrightarrow> False" |
|
851 have CL10: "!!U V. [|U \<in> S; V \<in> S; V \<subseteq> U; V \<noteq> U|] ==> False" |
|
852 by (iprover intro: equalityI CL2) |
|
853 have CL11: "!!U V. [|U \<in> S; V \<in> S; V \<noteq> U|] ==> False" |
|
854 by (iprover intro: CL10 CL2) |
|
855 have CL13: "!!U V. [|U \<in> S; ~ (S \<subseteq> V); U \<noteq> Set_XsubsetI_sko1_ S V|] ==> False" |
|
856 by (iprover intro: subsetI_0 CL11) |
|
857 have CL14: "!!U V. [|~ (S \<subseteq> U); ~(S \<subseteq> V); Set_XsubsetI_sko1_ S U \<noteq> Set_XsubsetI_sko1_ S V|] ==> False" |
|
858 by (iprover intro: subsetI_0 CL13) |
|
859 have CL29: "!!U V. [|~ (S \<subseteq> U); Set_XsubsetI_sko1_ S U \<noteq> Set_XsubsetI_sko1_ S {V}|] ==> False" |
|
860 by (iprover intro: CL1 CL14) |
|
861 have CL58: "!!U V. [| Set_XsubsetI_sko1_ S {U} \<noteq> Set_XsubsetI_sko1_ S {V}|] ==> False" |
|
862 by (iprover intro: CL1 CL29) |
|
863 have CL82: "!!U V. [| Set_XsubsetI_sko1_ S {U} \<in> {V}; ~ (S \<subseteq> {V})|] ==> False" |
|
864 by (iprover intro: subsetI_1 CL58 elim: ssubst) |
|
865 have CL85: "!!U V. [| Set_XsubsetI_sko1_ S {U} \<in> {V}|] ==> False" |
|
866 by (blast intro: CL1 CL82) |
|
867 show False |
|
868 by (iprover intro: insertI1 CL85) |
|
869 qed |
|
870 |
|
871 |
|
872 (*Based on this SPASS proof: |
|
873 |
|
874 Here is a proof with depth 6, length 15 : |
|
875 1[0:Inp] || -> c_in(U,c_insert(U,V,W),W)*. |
|
876 2[0:Inp] || -> c_lessequals(U,V,tc_set(W)) c_in(c_Main_OsubsetI__1(U,V,W),U,W)* |
|
877 . |
|
878 3[0:Inp] || c_in(c_Main_OsubsetI__1(U,V,W),V,W)* -> c_lessequals(U,V,tc_set(W)). |
|
879 |
|
880 4[0:Inp] || c_lessequals(U,V,tc_set(W))* c_lessequals(V,U,tc_set(W))* -> equal(U |
|
881 ,V). |
|
882 |
|
883 5[0:Inp] || c_lessequals(v_S,c_insert(U,c_emptyset,tc_set(t_a)),tc_set(tc_set(t_ |
|
884 a)))* -> . |
|
885 |
|
886 6[0:Inp] || c_in(U,v_S,tc_set(t_a)) c_in(V,v_S,tc_set(t_a)) -> c_lessequals(U,V, |
|
887 tc_set(t_a))*. |
|
888 10[0:Res:6.2,4.1] || c_in(U,v_S,tc_set(t_a)) c_in(V,v_S,tc_set(t_a)) c_lessequal |
|
889 s(V,U,tc_set(t_a))* -> equal(V,U). |
|
890 11[0:MRR:10.2,6.2] || c_in(U,v_S,tc_set(t_a))*+ c_in(V,v_S,tc_set(t_a))* -> equa |
|
891 l(V,U)*. |
|
892 13[0:Res:2.1,11.0] || c_in(U,v_S,tc_set(t_a))*+ -> c_lessequals(v_S,V,tc_set(tc_set(t_a)))* equal(U,c_Main_OsubsetI__1(v_S,V,tc_set(t_a)))*. |
|
893 |
|
894 14[0:Res:2.1,13.0] || -> c_lessequals(v_S,U,tc_set(tc_set(t_a)))* c_lessequals( |
|
895 v_S,V,tc_set(tc_set(t_a)))* equal(c_Main_OsubsetI__1(v_S,U,tc_set(t_a)),c_Main_OsubsetI__1(v_S,V,tc_set(t_a)))*. |
|
896 |
|
897 29[0:Res:14.1,5.0] || -> c_lessequals(v_S,U,tc_set(tc_set(t_a)))* equal(c_Main_ |
|
898 OsubsetI__1(v_S,U,tc_set(t_a)),c_Main_OsubsetI__1(v_S,c_insert(V,c_emptyset,tc_s |
|
899 et(t_a)),tc_set(t_a)))*. |
|
900 58[0:Res:29.0,5.0] || -> equal(c_Main_OsubsetI__1(v_S,c_insert(U,c_emptyset,tc_ |
|
901 set(t_a)),tc_set(t_a)),c_Main_OsubsetI__1(v_S,c_insert(V,c_emptyset,tc_set(t_a)) |
|
902 ,tc_set(t_a)))*. |
|
903 |
|
904 82[0:SpL:58.0,3.0] || c_in(c_Main_OsubsetI__1(v_S,c_insert(U,c_emptyset,tc_set(t_a)),tc_set(t_a)),c_insert(V,c_emptyset,tc_set(t_a)),tc_set(t_a))* -> c_lessequals(v_S,c_insert(V,c_emptyset,tc_set(t_a)),tc_set(tc_set(t_a))). |
|
905 |
|
906 85[0:MRR:82.1,5.0] || c_in(c_Main_OsubsetI__1(v_S,c_insert(U,c_emptyset,tc_set(t |
|
907 _a)),tc_set(t_a)),c_insert(V,c_emptyset,tc_set(t_a)),tc_set(t_a))* -> . |
|
908 |
|
909 86[0:UnC:85.0,1.0] || -> . |
|
910 Formulae used in the proof : |
|
911 *) |
|
912 |
836 end |
913 end |