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 
00021 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Resolution/Proofs.mac")$
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Resolution/tests/Proofs.mac")$
00023 
00024 
00025 /* ******************
00026    * Basic concepts *
00027    ******************
00028 */
00029 
00030 okltest_resl_p(resl_p);
00031 okltest_resl_ref_p(resl_ref_p);
00032 okltest_reslrt_p(reslrt_p);
00033 
00034 /* ************************************
00035    * Extraction                       *
00036    ************************************
00037 */
00038 
00039 
00040 okltest_axioms_resl2cl(axioms_resl2cl);
00041 okltest_resolvents_resl2cl(resolvents_resl2cl);
00042 
00043 
00044 /* ************************************
00045    * Other properties                 *
00046    ************************************
00047 */
00048 
00049 okltest_irredundant_ref_resl(irredundant_ref_resl);
00050 
00051 /* ************************************
00052    * Modifying proofs                 *
00053    ************************************
00054 */
00055 
00056 okltest_rename_resl(rename_resl);
00057 
00058 
00059 /* ************************************
00060    * Generators                       *
00061    ************************************
00062 */
00063 
00064 okltest_php_ext_uni_resl(php_ext_uni_resl);
00065 okltest_ncl_php_ext_uni_resl(ncl_php_ext_uni_resl);
00066 okltest_php_ext_resl(php_ext_resl);
00067 
00068