OKlibrary  0.2.1.6
HittingProofSystem.mac
Go to the documentation of this file.
```00001 /* Oliver Kullmann, 21.2.2012 (Swansea) */
00002 /* Copyright 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
00024 kill(f)\$
00025
00026
00027 /* ****************************************
00028    * The notion of a "hitting refutation" *
00029    ****************************************
00030 */
00031
00032 okltest_hitref_csp(f) := (
00033   assert(f({},{}) = false),
00034   assert(f({{}},{}) = false),
00035   assert(f({},{{}}) = false),
00036   assert(f({{}},{{}}) = true),
00037   assert(f({{}},0) = false),
00038   assert(f({{1},{-1}},{{1},{-1}}) = true),
00039   assert(f({{1},{-1}},{{1,2},{-1,2},{1,-2},{-1,-2}}) = true),
00040   assert(f({{1,2},{-1},{-2}},{{-1},{1,2},{1,-2}}) = true),
00041   assert(f({{-1,2},{-2,3},{-3,1},{1,2,3},{-1,-2,-3}},{{-1,2},{-2,3},{-3,1},{1,2,3},{-1,-2,-3}}) = true),
00042
00043   true)\$
00044
00045
00046 /* ********************************************
00047    * Hitting refutations from splitting trees *
00048    ********************************************
00049 */
00050
00051 okltest_stcs2hitref0(f) := block([C],
00052   assert(f({{}},[false]) = {{}}),
00053   assert(f({{},C},[false]) = {{}}),
00054   assert(f({{1},{-1}},[1,[false],[false]]) = {{1},{-1}}),
00055   assert(f({{1},{-1},{2},{-2}},[1,[false],[false]]) = {{1},{-1}}),
00056   assert(f({{1},{-1},{2},{-2}},[2,[false],[false]]) = {{2},{-2}}),
00057   assert(f({{1},{1,2},{1,-2},{-1}},[2,[1,[false],[false]],[1,[false],[false]]]) = {{1},{-1}}),
00058   assert(f({{1,2},{-1},{-2}},[1,[2,[false],[false]],[false]]) = {{1,2},{-1},{1,-2}}),
00059   assert(f({{-1,2},{-2,3},{-3,1},{1,2,3},{-1,-2,-3}},[1,[3,[2,[false],[false]],[false]],[2,[false],[3,[false],[false]]]]) = {{-1,2},{-2,3},{-3,1},{1,2,3},{-1,-2,-3}}),
00060   true)\$
00061
00062 okltest_stcs2hitref1(f) := block([C],
00063   assert(f({{}},[false]) = {{}}),
00064   assert(f({{},C},[false]) = {{}}),
00065   assert(f({{1},{-1}},[1,[false],[false]]) = {{1},{-1}}),
00066   assert(f({{1},{-1},{2},{-2}},[1,[false],[false]]) = {{1},{-1}}),
00067   assert(f({{1},{-1},{2},{-2}},[2,[false],[false]]) = {{2},{-2}}),
00068   assert(f({{1},{1,2},{1,-2},{-1}},[2,[1,[false],[false]],[1,[false],[false]]]) = {{1,2},{1,-2},{-1}}),
00069   assert(f({{1,2},{-1},{-2}},[1,[2,[false],[false]],[false]]) = {{1,2},{-1},{1,-2}}),
00070   assert(f({{-1,2},{-2,3},{-3,1},{1,2,3},{-1,-2,-3}},[1,[3,[2,[false],[false]],[false]],[2,[false],[3,[false],[false]]]]) = {{-1,2},{-2,3},{-3,1},{1,2,3},{-1,-2,-3}}),
00071   true)\$
00072
00073
00074
```