OKlibrary  0.2.1.6
ResolutionReductions.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 24.5.2008 (Swansea) */
00002 /* Copyright 2008, 2013 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/Satisfiability/Lisp/Resolution/Basics.mac")$
00023 
00024 
00025 /* ****************************
00026    * 2-Subsumption resolution *
00027    ****************************
00028 */
00029 
00030 /* Checks whether a clause-set is reduced w.r.t. 2-subsumption resolution: */
00031 redtsrp(F) := block(
00032  [LF : listify(F), l : length(F), found : false],
00033  for i : 1 thru l-1 unless found do block([C : LF[i]],
00034   for j : i+1 thru l unless found do
00035    if two_subsumption_resolvable(C, LF[j]) then found : true),
00036  return(not found))$
00037 /* The variation where a list of length <= 1 is returned: */
00038 redtsrl(F) := block(
00039  [LF : listify(F), l : length(F), R : []],
00040  for i : 1 thru l-1 unless not emptyp(R) do block([C : LF[i]],
00041   for j : i+1 thru l unless not emptyp(R) do
00042    if two_subsumption_resolvable(C, LF[j]) then R : [{C,LF[j]}]),
00043  return(R))$
00044 /* Reduce F w.r.t. 2-subsumption resolution: */
00045 redtsr(F) := block([R : redtsrl(F)],
00046   while not emptyp(R) do (
00047     F : adjoin(resolvent_s(R[1]),setdifference(F,R[1])),
00048     R : redtsrl(F)),
00049   return(F))$
00050 
00051