1module cl; % Common logic. Generic functions on first order formulas. 2 3revision('cl, "$Id: cl.red 4052 2017-05-16 08:07:37Z thomas-sturm $"); 4 5copyright('cl, "(c) 1995-2009 A. Dolzmann, T. Sturm, 2010-2017 T. Sturm"); 6 7% Redistribution and use in source and binary forms, with or without 8% modification, are permitted provided that the following conditions 9% are met: 10% 11% * Redistributions of source code must retain the relevant 12% copyright notice, this list of conditions and the following 13% disclaimer. 14% * Redistributions in binary form must reproduce the above 15% copyright notice, this list of conditions and the following 16% disclaimer in the documentation and/or other materials provided 17% with the distribution. 18% 19% THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 20% "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 21% LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR 22% A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT 23% OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 24% SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT 25% LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, 26% DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY 27% THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT 28% (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE 29% OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 30% 31 32create!-package('(cl clsimpl clbnf clnf clqe cltab clmisc clresolv), nil); 33 34load!-package 'redlog; 35 36exports cl_atfp,cl_cxfp,cl_atflp,cl_ncflp,cl_dnfp,cl_cnfp,cl_bnfp,cl_simpl, 37 cl_sitheo,cl_ordp,cl_smcpknowl,cl_smrmknowl,cl_smupdknowl,cl_smmkatl, 38 cl_smsimpl!-impl,cl_smsimpl!-equiv1,cl_siaddatl,cl_susimkatl,cl_susicpknowl, 39 cl_susiupdknowl,cl_dnf,cl_cnf,cl_bnf!-cartprod,cl_bnfsimpl,cl_sacatlp, 40 cl_sacat,cl_expand!-extbool,cl_nnf,cl_nnfnot,cl_pnf,cl_rename!-vars,cl_fvarl, 41 cl_fvarl1,cl_bvarl,cl_bvarl1,cl_varl,cl_varl1,cl_apnf,cl_freevp,cl_tnf, 42 cl_gqe,cl_gqea,cl_qe,cl_qea,cl_qeipo,cl_qews,cl_trygauss,cl_specelim,cl_tab, 43 cl_atab,cl_itab,cl_gentheo,cl_apply2ats,cl_apply2ats1,cl_apply2ats2,cl_atnum, 44 cl_f2ml,cl_atml,cl_atml1,cl_atl,cl_atl1,cl_identifyonoff,cl_ifacml, 45 cl_ifacml1,cl_ifacl,cl_ifacl1,cl_ifacdegl,cl_matrix,cl_closure,cl_all,cl_ex,cl_flip, 46 cl_cflip,cl_subfof,cl_termml,cl_termml1,cl_terml,cl_terml1,cl_struct, 47 cl_ifstruct,cl_surep,cl_splt; 48 49fluid '(cl_identify!-atl!* cl_pal!* cl_lps!* cl_theo!* 50 !*rlidentify !*rlsichk !*rlsism !*rlsiexpla !*rlbnfsm !*rlverbose 51 !*rlsiidem !*rlsiso !*rlqepnf !*rlqedfs !*rlqeans !*rlqegsd !*rlqeheu 52 !*rlqegen !*rlbnfsac !*rltnft !*rlsipw !*rlsipo !*rlqevarsel 53 !*rlspgs !*rlsithok !*rlqefb !*rlqelocal !*rlresi !*rlqeprecise 54 !*rlqeaprecise !*rlqestdans !*slat); 55 56struct Formula; 57struct FormulaL asserted by listp; 58struct QfFormula; 59struct QfFormulaL asserted by listp; 60struct TruthValue asserted by rl_tvalp; 61struct Theory asserted by listp; 62struct TheoryFormulaPair asserted by pairp; 63struct KernelL asserted by listp; 64struct Quantifier asserted by idp; 65 66procedure cl_atfp(x); 67 % Common logic atomic formula predicate. [x] is a formula. Returns 68 % non-[nil] iff [x] is an atomic formula. 69 not rl_cxp rl_op x; 70 71procedure cl_cxfp(x); 72 % Common logic complex formula predicate. [x] is a formula. Returns 73 % non-[nil] iff [x] is a complex, i.e. non-atomic, formula. 74 rl_cxp rl_op x; 75 76procedure cl_atflp(fl); 77 % Common logic atomic formula list predicate. [fl] is a list of 78 % formulas. Returns [T] or [nil]. [T] is returned if and only if 79 % [fl] is a list of atomic formulas. 80 null fl or (cl_atfp car fl and cl_atflp cdr fl); 81 82procedure cl_ncflp(fl); 83 % Common logic non-complex formula list predicate. [fl] is a list 84 % of formulas. Returns [T] or [nil]. [T] is returned if and only if 85 % [fl] is a list of atomic formulas and truth values. 86 null fl or ((cl_atfp car fl or rl_tvalp car fl) and cl_ncflp cdr fl); 87 88procedure cl_dnfp(f); 89 % Common logic disjunctive normal form predicate. [f] is a formula. 90 % Returns [T] or [nil]. [T] is returned iff [f] is in disjunctive 91 % normal form. 92 (rl_tvalp f) or (cl_atfp f) or (rl_op f eq 'and and cl_ncflp rl_argn f) 93 or ((rl_op f eq 'or) and cl_dnfp1 rl_argn f); 94 95procedure cl_dnfp1(fl); 96 % Common logic disjunctive normal form predicate subroutine. [f] is 97 % a formula. Returns [T] or [nil]. 98 (null fl) or ((rl_tvalp car fl) or (cl_atfp car fl) or 99 ((rl_op car fl eq 'and) and (cl_ncflp rl_argn car fl))) and 100 (cl_dnfp1 cdr fl); 101 102procedure cl_cnfp(f); 103 % Common logic conjunctive normal form predicate. [f] is a formula. 104 % Returns [T] or [nil]. [T] is returned iff [f] is in conjunctive 105 % normal form. 106 (rl_tvalp f) or (cl_atfp f) or (rl_op f eq 'or and cl_ncflp rl_argn f) 107 or ((rl_op f eq 'and) and cl_cnfp1 rl_argn f); 108 109procedure cl_cnfp1(fl); 110 % Common logic conjunctive normal form predicate subroutine . [f] 111 % is a formula. Returns [T] or [nil]. [T] is returned iff [f] is in 112 % conjunctive normal form. 113 (null fl) or ((rl_tvalp car fl) or (cl_atfp car fl) or 114 ((rl_op car fl eq 'or) and (cl_ncflp rl_argn car fl))) and 115 (cl_cnfp1 cdr fl); 116 117procedure cl_bnfp(f); 118 % Common logic boolean normal form predicate. [f] is a formula. 119 % Returns [T] or [nil]. [T] is returned iff [f] is in disjunctive 120 % or conjunctive normal form. 121 (rl_tvalp f) or (cl_atfp f) or (cl_ncflp rl_argn f) 122 or ((rl_op f eq 'and) and cl_cnfp1 rl_argn f) or 123 ((rl_op f eq 'or) and cl_dnfp1 rl_argn f); 124 125endmodule; % [cl] 126 127end; % of file 128