OKlibrary  0.2.1.6
ResolutionReductions.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 24.5.2008 (Swansea) */
00002 /* Copyright 2008 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/Satisfiability/Lisp/Generators/Generators.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/ResolutionReductions.mac")$
00025 
00026 kill(f)$
00027 
00028 
00029 /* ****************************
00030    * 2-Subsumption resolution *
00031    ****************************
00032 */
00033 
00034 okltest_redtsrp(f) := block(
00035   assert(f({}) = true),
00036   assert(f({{}}) = true),
00037   assert(f({{1}}) = true),
00038   assert(f({{},{1}}) = true),
00039   for n : 1 thru 5 do block([F : full_fcs(n)[2]],
00040     assert(f(F) = false)
00041   ),
00042   true)$
00043 
00044 okltest_redtsr(f) := block(
00045   assert(f({}) = {}),
00046   assert(f({{}}) = {{}}),
00047   assert(f({{1}}) = {{1}}),
00048   assert(f({{},{1}}) ={{},{1}}),
00049   for n : 1 thru 4 do block([F : full_fcs(n)[2]],
00050     assert(redtsrp(f(F)))
00051   ),
00052   true)$
00053 
00054