1module tplp; 2% Theorem proving lisp prefix. Main module. Algorithms on first-order 3% formulas over a finite language. The terms are represented in lisp 4% prefix. 5 6revision('tplp, "$Id: tplp.red 4049 2017-05-16 06:38:49Z thomas-sturm $"); 7 8copyright('tplp, "(c) 2007-2017 T. Sturm"); 9 10% Redistribution and use in source and binary forms, with or without 11% modification, are permitted provided that the following conditions 12% are met: 13% 14% * Redistributions of source code must retain the relevant 15% copyright notice, this list of conditions and the following 16% disclaimer. 17% * Redistributions in binary form must reproduce the above 18% copyright notice, this list of conditions and the following 19% disclaimer in the documentation and/or other materials provided 20% with the distribution. 21% 22% THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 23% "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 24% LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR 25% A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT 26% OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 27% SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT 28% LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, 29% DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY 30% THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT 31% (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE 32% OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 33% 34 35% The following is from the old rlsched.red: 36%% rl_mkserv('skolemize,'(rl_simp),{function(lambda x; x)},'(nil),'rl_mk!*fof,t); 37 38create!-package('(tplp tplpkapur),nil); 39 40load!-package 'redlog; % for rl_texmacsp() 41loadtime load!-package 'cl; 42 43global '(tplp_fsyml!* tplp_rsyml!*); 44 45flag('(tplp),'rl_package); 46 47% Parameters 48put('tplp,'rl_params,'( 49 (rl_op!* . tplp_op))); 50 51% Services 52put('tplp,'rl_services,'( 53 (rl_kapur!* . tplp_kapur) 54 (rl_miniscope!* . tplp_miniscope) 55 (rl_skolemize!* . tplp_skolemize) 56 (rl_subfof!* . cl_subfof) 57 (rl_ex!* . cl_ex) 58 (rl_all!* . cl_all) 59 (rl_atnum!* . tplp_atnum) 60 (rl_qnum!* . cl_qnum) 61 (rl_atl!* . cl_atl) 62 (rl_atml!* . cl_atml) 63 (rl_terml!* . cl_terml) 64 (rl_termml!* . cl_termml) 65 (rl_cnf!* . tplp_cnf) 66 (rl_dnf!* . tplp_dnf) 67 (rl_pnf!* . cl_pnf) 68 (rl_nnf!* . cl_nnf) 69 (rl_nnfnot!* . cl_nnfnot) 70 (rl_bnfsimpl!* . cl_bnfsimpl) 71 (rl_sacat!* . cl_sacat) 72 (rl_sacatlp!* . cl_sacatlp) 73 (rl_negateat!* . tplp_negateat) 74 (rl_simpl!* . cl_simpl) 75 (rl_smupdknowl!* . cl_smupdknowl) 76 (rl_smrmknowl!* . cl_smrmknowl) 77 (rl_smcpknowl!* . cl_smcpknowl) 78 (rl_smmkatl!* . cl_smmkatl) 79 (rl_smsimpl!-impl!* . cl_smsimpl!-impl) 80 (rl_smsimpl!-equiv1!* . cl_smsimpl!-equiv1) 81 (rl_simplat1!* . tplp_simplat1) 82 (rl_ordatp!* . ordop) 83 (rl_varl!* . cl_varl) 84 (rl_fvarl!* . cl_fvarl) 85 (rl_bvarl!* . cl_bvarl) 86 (rl_subat!* . tplp_subat) 87 (rl_eqnrhskernels!* . tplp_eqnrhskernels) 88 (rl_subalchk!* . tplp_subalchk) 89 (rl_varlat!* . tplp_varlat) 90 (rl_matrix!* . cl_matrix))); 91 92% Admin 93put('tplp,'rl_enter,'tplp_enter); 94put('tplp,'rl_exit,'tplp_exit); 95put('tplp,'simpfnname,'tplp_simpfn); 96put('tplp,'rl_prepat,'tplp_prepat); 97put('tplp,'rl_resimpat,'tplp_resimpat); 98put('tplp,'rl_lengthat,'tplp_lengthat); 99put('tplp,'rl_prepterm,'tplp_prepterm); 100put('tplp,'rl_simpterm,'tplp_simpterm); 101 102algebraic infix equal; 103put('equal,'number!-of!-args,2); 104put('equal,'tplp_simpfn,'tplp_simpat); 105 106algebraic infix neq; 107put('neq,'number!-of!-args,2); 108put('neq,'tplp_simpfn,'tplp_simpat); 109put('neq,'rtypefn,'quotelog); 110newtok '((!< !>) neq); 111 112flag('(equal neq),'spaced); 113flag('(tplp_simpat),'full); 114 115procedure tplp_enter(argl); 116 % Theorem proving lisp prefix enter context. [argl] is a list 117 % containing lists representing language elements. Returns a pair 118 % $(f . l)$. If $f$ is nil then $l$ contains an error message, else 119 % $l$ is the new value of [rl_argl!*]. 120 begin scalar op; 121 if not eqn(length argl,2) then 122 return nil . "wrong number of arguments"; 123 tplp_fsyml!* := for each x in cdar argl collect << 124 op := cadr x; 125 if not idp op then 126 typerr(op,"function symbol"); 127 if eqn(caddr x,0) then << 128 lprim {op,"is being reserved"}; 129 flag ({op},'reserved) 130 >> else 131 tplp_mkalop cdr x; 132 cadr x . caddr x 133 >>; 134 tplp_rsyml!* := for each x in cdadr argl collect << 135 tplp_mkalop cdr x; 136 tplp_mkpredicate cdr x; 137 cadr x . caddr x 138 >>; 139 return t . argl 140 end; 141 142procedure tplp_exit(); 143 % Theorem proving lisp prefix exit context. 144 << 145 for each x in tplp_fsyml!* do 146 if eqn(cdr x,0) then 147 remflag({car x},'reserved) 148 else 149 tplp_unmkalop car x; 150 for each x in tplp_rsyml!* do << 151 tplp_unmkalop car x; 152 tplp_unmkpredicate car x 153 >>; 154 tplp_rsyml!* := nil; 155 tplp_fsyml!* := nil; 156 nil 157 >>; 158 159procedure tplp_mkalop(f); 160 % Theorem proving lisp prefix make algebraic operator. [f] is a 161 % dotted pair of the form $(op . arity)$. 162 (algebraic operator op) where op=car f; 163 164procedure tplp_unmkalop(f); 165 % Theorem proving lisp prefix unmake algebraic operator. [f] is an 166 % identifier. 167 algebraic clear f; 168 169procedure tplp_mkpredicate(r); 170 % Theorem proving lisp prefix make predicate. [r] is a 171 % dotted pair of the form $(op . arity)$. 172 put(car r,'tplp_simpfn,'tplp_simpat); 173 174procedure tplp_unmkpredicate(r); 175 % Theorem proving lisp prefix unmake predicate. [r] is an 176 % identifier. 177 remprop(r,'tplp_simpfn); 178 179procedure tplp_fsyml(); 180 % Theorem proving Lisp prefix get language. 181 tplp_fsyml!*; 182 183procedure tplp_rsyml(); 184 % Theorem proving Lisp prefix get language. 185 tplp_rsyml!*; 186 187procedure tplp_prepat(atf); 188 % Theorem proving Lisp prefix prep atomic formula. [atf] is an atomic 189 % formula. Returns [atf] in Lisp prefix form. 190 atf; 191 192procedure tplp_lengthat(atf); 193 % Theorem proving Lisp prefix length of atomic formula. [atf] is an 194 % atomic formula. Returns length of [atf]. 195 length cdr atf; 196 197procedure tplp_simpterm(term); 198 % Theorem proving Lisp prefix simplify term. [term] is a Lisp 199 % prefix term. Returns context-specific representation of [term], 200 % which is Lisp prefix here. Apart from syntax-checking, reval 201 % would work here. We have to take care of rebound atoms. 202 begin scalar w; integer arity; 203 if atom term then 204 return reval term; 205 w := atsoc(car term,tplp_fsyml()); 206 if null w then 207 rederr {car term,"not declared as function symbol"}; 208 arity := cdr w; 209 if not eqn(length cdr term,arity) then 210 rederr {car term, "requires", arity,"arguments"}; 211 return car term . for each arg in cdr term collect 212 tplp_simpterm arg 213 end; 214 215procedure tplp_resimpterm(term); 216 % Theorem proving Lisp prefix resimplify term. [term] is a term. 217 % Returns resimplified [term]. We try to be somewhat more efficient 218 % than reval. 219 if atom term then 220 reval term 221 else 222 car term . for each x in cdr term collect tplp_resimpterm x; 223 224procedure tplp_prepterm(term); 225 % Theorem proving Lisp prefix prep term. [term] is a term. Returns 226 % the Lisp prefix representaion of term. 227 term; 228 229procedure tplp_simpat(atf); 230 % Theorem proving Lisp prefix simplify atomic formula. [atf] is 231 % Lisp prefix. Returns an atomic formula. 232 begin scalar op; 233 op := car atf; 234 if not (op and atom op) then 235 typerr (op,"predicate symbol"); 236 return op . for each x in cdr atf collect tplp_simpterm x 237 end; 238 239procedure tplp_resimpat(atf); 240 % Theorem proving Lisp prefix simplify atomic formula. [atf] is an 241 % atomic formula. Returns atomic formula with resimplified terms. 242 car atf . for each x in cdr atf collect tplp_resimpterm x; 243 244procedure tplp_opp(op); 245 % Theorem proving Lisp prefix operator predicate. [op] is an atom. 246 % Returns non-[nil] if op is a relation. 247 atsoc(op,tplp_rsyml()); 248 249procedure tplp_op(at); 250 % Theorem proving Lisp prefix operator. [at] is an atomic formula. 251 % Returns the relation symbol of [at]. 252 car at; 253 254procedure tplp_arg2l(at); 255 % Theorem proving Lisp prefix argument binary operator left hand 256 % side. [at] is an atomic formula $R(lhs,rhs)$. Returns $lhs$. 257 cadr at; 258 259procedure tplp_arg2r(at); 260 % Theorem proving Lisp prefix argument binary operator right hand 261 % side. [at] is an atomic formula $R(lhs,rhs)$. Returns $rhs$. 262 caddr at; 263 264procedure tplp_argl(f); 265 % Theorem proving Lisp prefix argument list. [f] is a formula. 266 % Returns the list of arguments of [f]. 267 cdr f; 268 269procedure tplp_mk2(op,lhs,rhs); 270 % Theorem proving Lisp prefix make atomic formula for binary 271 % operator. [op] is ['equal] or ['neq], [lhs] and [rhs] are 272 % terms. Returns the atomic formula $[op]([lhs],[rhs])$. 273 {op,lhs,rhs}; 274 275procedure tplp_mkn(op,argl); 276 % Theorem proving Lisp prefix make atomic formula for n-ary operator. 277 % [op] is ['equal], ['neq] or a predicate symbol, [argl] is a list of 278 % terms. Returns the atomic formula $[op]([argl])$. 279 op . argl; 280 281procedure tplp_fop(term); 282 % Theorem proving Lisp prefix function operator. [term] is a term $(F 283 % args)$. Returns $F$. 284 car term; 285 286procedure tplp_fmkn(op,argl); 287 % Theorem proving Lisp prefix function make for n-ary operator. 288 % [op] is an identifier, [argl] is a list of terms. 289 op . argl; 290 291procedure tplp_fargl(term); 292 % Theorem proving Lisp prefix function's argument list. [term] is a 293 % term. Return the list of argument terms. 294 cdr term; 295 296procedure tplp_varlat(atf); 297 % Variable list atomic formula. [atf] is an atomic formula. Returns a 298 % list of identifiers. The set of variables ocurring in [atf]. 299 begin scalar l; 300 for each x in tplp_argl atf do 301 if idp x and null tplp_funcp x then 302 l := lto_insertq(x,l) 303 else if pairp x and tplp_funcp tplp_fop x then 304 l := union(l,tplp_varlterm x); 305 return l 306 end; 307 308procedure tplp_funcp(op); 309 % Theorem proving Lisp prefix function predicate. [op] is an identifier. 310 % Returns non-[nil] if op is a function. 311 atsoc(op,tplp_fsyml()); 312 313procedure tplp_varlterm(term); 314 % Variable list term. [term] is a term. Returns a 315 % list of identifiers. The set of variables ocurring in [term]. 316 begin scalar l; 317 if idp term then 318 return if null tplp_funcp term then {term}; 319 for each x in tplp_fargl term do 320 if idp x and null tplp_funcp x then 321 l := lto_insertq(x,l) 322 else if pairp x then 323 l := union(l,tplp_varlterm x); 324 return l 325 end; 326 327procedure tplp_subat(al,atf); 328 % Substitute in atomic formula. [al] is an 329 % alist, [atf] is an atomic formula. Returns an atomic formula. 330 tplp_mkn(tplp_op atf,for each x in tplp_argl atf collect tplp_subt(al,x)); 331 332procedure tplp_subt(al,u); 333 % Substitute in term. [al] is an alist, [u] is a term. Returns a term. 334 begin scalar w; 335 if idp u and (w := atsoc(u,al)) then 336 return tplp_clonestruct cdr w; 337 if atom u then 338 return u; 339 return tplp_fmkn(tplp_fop u,for each arg in tplp_fargl u collect 340 tplp_subt(al,arg)) 341 end; 342 343procedure tplp_clonestruct(s); 344 % Clone structure. [s] is any. Returns any, which is a clone of [s] in a 345 % constructive way. 346 if atom s then s else (tplp_clonestruct car s) . (tplp_clonestruct cdr s); 347 348procedure tplp_eqnrhskernels(x); 349 % Equation right hand side 350 % kernels. [x] is an equation. Returns a list of all kernels 351 % contained in the right hand side of [x]. 352 tplp_varlterm cdr x; 353 354procedure tplp_subalchk(al); 355 % Substitution alist check. 356 ; 357 358procedure tplp_atnum(f); 359 % Atomic formula number. [f] is a 360 % formula. Returns the number of atomic formulas in [f]. 361 begin scalar op; 362 op := rl_op f; 363 if rl_boolp op then 364 return for each subf in rl_argn f sum tplp_atnum subf; 365 if rl_quap op then 366 return tplp_atnum rl_mat f; 367 if rl_tvalp op then return 0; 368 % [f] is an atomic formula. 369 return 1 370 end; 371 372procedure tplp_negateat(atf); 373 % Negate atomic formula. [atf] is an atomic formula. Returns the negation 374 % of [atf]. 375 if tplp_op atf eq 'negp then tplp_argl atf else tplp_mkn('negp,atf); 376 377procedure tplp_cnf(f); 378 % Conjunctive normalform. [f] is a formula. Returns a formula. 379 tplp_removenegp cl_cnf f; 380 381procedure tplp_dnf(f); 382 % Disjunctive normalform. [f] is a formula. Returns a formula. 383 tplp_removenegp cl_dnf f; 384 385procedure tplp_removenegp(f); 386 % Remove help-predicate negp. [f] is a formula. Returns a formula where each 387 % negated predicate is replaced by 'not . p. 388 if rl_tvalp rl_op f then 389 f 390 else if rl_boolp rl_op f then 391 rl_mkn(rl_op f,for each x in rl_argn f collect tplp_removenegp x) 392 else if rl_quap rl_op f then 393 rl_mkq(rl_op f,rl_var f,tplp_removenegp rl_mat f) 394 else if tplp_op f eq 'negp then 395 rl_mk1('not,tplp_argl f) 396 else 397 f; 398 399procedure tplp_simplat1(at,sop); 400 % Simplify atomic formula. (no simplification) 401 at; 402 403procedure tplp_constp(term); 404 % Constant predicate. [term] is a term. Returns non-nil if [term] 405 % is a constant term. 406 (idp term and tplp_funcp term) or (pairp term and null tplp_fargl term); 407 408procedure tplp_cons2func(f); 409 % Constant to function. [f] is a formula. Returns a formula where 410 % every constant is represented as a 0-ary function. 411 if rl_tvalp f then 412 f 413 else if rl_boolp rl_op f then 414 rl_mkn(rl_op f,for each x in rl_argn f collect tplp_cons2func x) 415 else if rl_quap rl_op f then 416 rl_mkq(rl_op f,rl_var f,tplp_cons2func rl_mat f) 417 else if tplp_op f eq 'negp then 418 rl_mk1('not,tplp_mkn(tplp_op tplp_argl f,for each x in tplp_argl 419 tplp_argl f collect tplp_fcons2func x)) 420 else 421 tplp_mkn(tplp_op f,for each x in tplp_argl f collect tplp_fcons2func x); 422 423procedure tplp_fcons2func(term); 424 % Term Constant to function. [term] is a term. Returns a term where 425 % every constant is represented as a 0-ary function. 426 if idp term and tplp_funcp term then 427 tplp_fmkn(term,nil) 428 else if idp term then 429 term 430 else 431 tplp_fmkn(tplp_fop term,for each x in tplp_fargl term collect 432 tplp_fcons2func x); 433 434endmodule; % [tplp] 435 436end; % of file 437