OKlibrary  0.2.1.6
Formulas.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 9.2.2008 (Swansea) */
00002 /* Copyright 2008, 2009 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 
00021 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/PropositionalLogic/Formulas.mac")$
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/PropositionalLogic/tests/Formulas.mac")$
00023 
00024 /* ***********************************
00025    * Representation of formulas      *
00026    ***********************************
00027 */
00028 
00029 okltest_var_prpl(var_prpl);
00030 okltest_var_ft(var_ft);
00031 
00032 /* ******************************************
00033    * Basic transformations of formula trees *
00034    ******************************************
00035 */
00036 
00037 okltest_elimination_constants_ft(elimination_constants_ft);
00038 
00039 /* ***********************
00040    * Partial assignments *
00041    ***********************
00042 */
00043 
00044 okltest_apply_pa_prpl(apply_pa_prpl);
00045 
00046 /* ******************
00047    * Measures       *
00048    ******************
00049 */
00050 
00051 /* ******************
00052    * Translations   *
00053    ******************
00054 */
00055 
00056 
00057 
00058 /* ****************************
00059    * Tseitin translation      *
00060    ****************************
00061 */
00062 
00063 okltest_tseitin_trans_list_rel(tseitin_trans_list_rel);
00064 okltest_tseitin_trans_list(tseitin_trans_list);
00065 okltest_tseitin_trans_basic(tseitin_trans_basic);
00066