OKlibrary  0.2.1.6
Proofs.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 23.9.2011 (Swansea) */
00002 /* Copyright 2011, 2012 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/TestSystem/Lisp/Asserts.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Trees/Lisp/Basics.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Pigeonhole.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac")$
00026 
00027 kill(f)$
00028 
00029 /* ************************************
00030    * Checking the defining properties *
00031    ************************************
00032 */
00033 
00034 okltest_resl_p(f) := block(
00035   assert(f(1) = false),
00036   assert(f([]) = true),
00037   assert(f([1]) = false),
00038   assert(f([{1},1]) = false),
00039   assert(f([{}]) = true),
00040   assert(f([{1}]) = true),
00041   assert(f([{1},{2},{-3}]) = true),
00042   assert(f([{-1},{1},[{},[1,2]]]) = true),
00043   assert(f([{-1},{-2},{1,2},[{1},[2,3]],[{},[1,4]]]) = true),
00044   assert(f([{-1},{1},[{},[1,3]]]) = false),
00045   assert(f([{-1},{1},[{},["s",3]]]) = false),
00046   assert(f([{-1},{1},[{},[-1,2]]]) = false),
00047   assert(f([{-1},{1},{1,2},{1,4},[{},[1,2]]]) = true),
00048   assert(f([{-1},{1},{1,2},{1,4},[{},[1,2]],{3}]) = true),
00049   assert(f([{-1},{1},{1,2},{1,4},[{},[1,2]],[{},[1,2]]]) = true),
00050   assert(f([{-1},{1},{1,2},{1,4},[{},[1,2]],[{},[3,4]]]) = false),
00051   true)$
00052 
00053 okltest_resl_ref_p(f) := block(
00054   assert(f(1) = false),
00055   assert(f([]) = false),
00056   assert(f([1]) = false),
00057   assert(f([{1},1]) = false),
00058   assert(f([{}]) = true),
00059   assert(f([{1}]) = false),
00060   assert(f([{1},{2},{-3}]) = false),
00061   assert(f([{-1},{1},[{},[1,2]]]) = true),
00062   assert(f([{-1},{-2},{1,2},[{1},[2,3]],[{},[1,4]]]) = true),
00063   assert(f([{-1},{1},[{},[1,3]]]) = false),
00064   assert(f([{-1},{1},[{},["s",3]]]) = false),
00065   assert(f([{-1},{1},[{},[-1,2]]]) = false),
00066   assert(f([{-1},{1},{1,2},{1,4},[{},[1,2]]]) = true),
00067   assert(f([{-1},{1},{1,2},{1,4},[{},[1,2]],{3}]) = true),
00068   assert(f([{-1},{1},{1,2},{1,4},[{},[1,2]],[{},[1,2]]]) = true),
00069   assert(f([{-1},{1},{1,2},{1,4},[{},[1,2]],[{},[3,4]]]) = false),
00070   true)$
00071 
00072 okltest_reslrt_p(f) := block(
00073   assert(f([{}]) = true),
00074   assert(f([{1}]) = true),
00075   assert(f([{-1}]) = true),
00076   assert(f([{2}]) = true),
00077   assert(f([[1]]) = false),
00078   assert(f([{},[{1}],[{-1}]]) = true),
00079   assert(f([{},[{1}],[{1}]]) = false),
00080   assert(f([{},[{}],[{}]]) = false),
00081   assert(f([{},[{1}],[{-1}],[{1}]]) = false),
00082   assert(f([{1},[{1,2}],[{-2}]]) = true),
00083   assert(f([{1},[{1,2},[{1,2,3}],[{1,2,-3}]],[{-2},[{1,-2}],[{-1,-2}]]]) = true),
00084   assert(f([{},[{1,2},[{1,2,3}],[{1,2,-3}]],[{-2},[{1,-2}],[{-1,-2}]]]) = false),
00085   assert(f([{1},[{1,2},[{1,2,3}],[{1,2,-3}]],[{-2}]]) = true),
00086   assert(f([{1},[{1,2},[{1,2,3}],[{1,2,-3}],[{1,2}]],[{-2}]]) = false),
00087   if oklib_test_level = 0 then return(true),
00088   for m : 1 thru 3 do
00089     assert(f(st2reslrt_cs(
00090           dll_simplest_st(
00091             weak_php_fcs(m+1,m),
00092             dll_heuristics_first_formal),weak_php_fcs(m+1,m)[2])) = true),
00093   true)$
00094 
00095 
00096 /* ************************************
00097    * Extraction                       *
00098    ************************************
00099 */
00100 
00101 
00102 okltest_axioms_resl2cl(f) := block(
00103   assert(f([]) = []),
00104   assert(f([{}]) = [{}]),
00105   assert(f([{1}]) = [{1}]),
00106   assert(f([{1},{2},{-3}]) = [{1},{2},{-3}]),
00107   assert(f([{-1},{1},[{},[1,2]]]) = [{-1},{1}]),
00108   assert(f([{-1},{-2},{1,2},[{1},[2,3]],[{},[1,4]]]) = [{-1},{-2},{1,2}]),
00109   assert(f([{-1},{1},{1,2},{1,4},[{},[1,2]]]) = [{-1},{1},{1,2},{1,4}]),
00110   assert(
00111     f([{-1},{1},{1,2},{1,4},[{},[1,2]],{3}]) = [{-1},{1},{1,2},{1,4},{3}]),
00112   assert(
00113     f([{-1},{1},{1,2},{1,4},[{},[1,2]],[{},[1,2]]]) = [{-1},{1},{1,2},{1,4}]),
00114   true)$
00115 
00116 okltest_resolvents_resl2cl(f) := block(
00117   assert(f([]) = []),
00118   assert(f([{}]) = []),
00119   assert(f([{1}]) = []),
00120   assert(f([{1},{2},{-3}]) = []),
00121   assert(f([{-1},{1},[{},[1,2]]]) = [{}]),
00122   assert(f([{-1},{-2},{1,2},[{1},[2,3]],[{},[1,4]]]) = [{1},{}]),
00123   assert(f([{-1},{1},{1,2},{1,4},[{},[1,2]]]) = [{}]),
00124   assert(f([{-1},{1},{1,2},{1,4},[{},[1,2]],{3}]) = [{}]),
00125   assert(f([{-1},{1},{1,2},{1,4},[{},[1,2]],{3}]) = [{}]),
00126   assert(f([{-1},{1},{1,2},{1,4},[{},[1,2]],[{},[1,2]]]) = [{},{}]),
00127   true)$
00128 
00129 okltest_irredundant_ref_resl(f) := block(
00130   assert(f([{}])),
00131   assert(f([{1},{-1},[{},[1,2]]])),
00132   assert(not(f([{1},{-1},{2},[{},[1,2]]]))),
00133   assert(not(f([{1,2},{-1,2},[{2},[1,2]],{1},{-1},[{},[4,5]]]))),
00134   true)$
00135 
00136 
00137 /* ************************************
00138    * Modifying proofs                 *
00139    ************************************
00140 */
00141 
00142 okltest_rename_resl(f) := block(
00143   assert(f([], sm2hm({})) = []),
00144   assert(f([], sm2hm({[1,2],[-1,-2]})) = []),
00145   assert(f([{1},{2}], sm2hm({[1,2],[-1,-2],[2,1],[-2,-1]})) = [{2},{1}]),
00146   assert(f([{1},{-2}], sm2hm({[1,2],[-1,-2],[2,1],[-2,-1]})) = [{2},{-1}]),
00147   assert(f([{1},{-2},{3}], sm2hm({[1,2],[-1,-2],[2,1],[-2,-1]})) = [{2},{-1},{3}]),
00148   assert(
00149     f([{1,-2},{1,2},[{1},[1,2]]], sm2hm({[1,3],[-1,-3],[2,4],[-2,-4]}))
00150       = [{3,-4},{3,4},[{3},[1,2]]]),
00151   true)$
00152 
00153 /* ************************************
00154    * Generators                       *
00155    ************************************
00156 */
00157 
00158 okltest_php_ext_uni_resl(f) := block(
00159   assert(f(0) = [{}]),
00160   assert(f(1) =
00161     [{-php_ext(1,1,1),-php_ext(1,2,1)},{php_ext(1,1,1)},{php_ext(1,2,1)},
00162      [{-php_ext(1,2,1)},[1,2]],[{},[3,4]]]),
00163   if oklib_test_level = 0 then return(true),
00164   assert(f(2) =
00165     [{-php_ext(1,1,1),php_ext(2,1,1),php_ext(2,1,2)},
00166      {-php_ext(1,1,1),php_ext(2,1,1),php_ext(2,3,1)},
00167      {php_ext(1,1,1),-php_ext(2,1,1)},
00168      {php_ext(1,1,1),-php_ext(2,1,2),-php_ext(2,3,1)},
00169      {-php_ext(1,2,1),php_ext(2,2,1),php_ext(2,2,2)},
00170      {-php_ext(1,2,1),php_ext(2,2,1),php_ext(2,3,1)},
00171      {php_ext(1,2,1),-php_ext(2,2,1)},
00172      {php_ext(1,2,1),-php_ext(2,2,2),-php_ext(2,3,1)},
00173      {-php_ext(2,1,1),-php_ext(2,2,1)},{-php_ext(2,1,1),-php_ext(2,3,1)},
00174      {php_ext(2,1,1),php_ext(2,1,2)},{-php_ext(2,1,2),-php_ext(2,2,2)},
00175      {-php_ext(2,1,2),-php_ext(2,3,2)},{-php_ext(2,2,1),-php_ext(2,3,1)},
00176      {php_ext(2,2,1),php_ext(2,2,2)},{-php_ext(2,2,2),-php_ext(2,3,2)},
00177      {php_ext(2,3,1),php_ext(2,3,2)},
00178      [{-php_ext(1,2,1),-php_ext(2,1,1),php_ext(2,2,1)},[6,10]],
00179      [{-php_ext(1,2,1),-php_ext(2,1,1)},[18,9]],
00180      [{-php_ext(1,1,1),php_ext(2,1,1),-php_ext(2,2,1)},[2,14]],
00181      [{-php_ext(1,1,1),-php_ext(2,2,1)},[20,9]],
00182      [{-php_ext(1,1,1),-php_ext(1,2,1),php_ext(2,1,2)},[1,19]],
00183      [{-php_ext(1,1,1),-php_ext(1,2,1),php_ext(2,2,2)},[5,21]],
00184      [{-php_ext(1,1,1),-php_ext(1,2,1),-php_ext(2,1,2)},[23,12]],
00185      [{-php_ext(1,1,1),-php_ext(1,2,1)},[24,22]],
00186      [{php_ext(1,1,1),php_ext(2,1,2)},[11,3]],
00187      [{php_ext(1,2,1),php_ext(2,2,2)},[15,7]],
00188      [{php_ext(1,1,1),-php_ext(2,1,2),php_ext(2,3,2)},[17,4]],
00189      [{php_ext(1,2,1),-php_ext(2,2,2),php_ext(2,3,2)},[17,8]],
00190      [{php_ext(1,1,1),-php_ext(2,1,2)},[28,13]],
00191      [{php_ext(1,2,1),-php_ext(2,2,2)},[29,16]],[{php_ext(1,1,1)},[30,26]],
00192      [{php_ext(1,2,1)},[31,27]],[{-php_ext(1,2,1)},[25,32]],[{},[33,34]]]),
00193   for i : 3 thru 5 do block([F],
00194     F : f(i),
00195     assert(resl_ref_p(F)),
00196     assert(irredundant_ref_resl(F))),
00197   true)$
00198 
00199 okltest_php_ext_resl(f) := block(
00200   assert(
00201     okltest_php_ext_uni_resl(
00202       buildq([f], lambda([n], rename_resl(f(n),sm2hm(var_php2ephp_sm(n))))))),
00203   true)$
00204 
00205 okltest_ncl_php_ext_uni_resl(f) := block(
00206   assert(f(0) = 1),
00207   assert(f(1) = 5),
00208   assert(f(2) = 35),
00209   assert(f(3) = 138),
00210   assert(f(4) = 385),
00211   true)$
00212