(* ---------------------------------------------------------------------------- * $Id: MLDEMO.md,v 1.5 1995/11/04 18:00:23 pesch Exp $ * ---------------------------------------------------------------------------- * Copyright (c) 1993 Universitaet Passau * ---------------------------------------------------------------------------- * This file is part of MAS. * ---------------------------------------------------------------------------- * $Log: MLDEMO.md,v $ * Revision 1.5 1995/11/04 18:00:23 pesch * Changed comments violating documentation rules. Should be rewritten. * * Revision 1.4 1994/11/28 21:04:10 dolzmann * New revision of the MASLOG system: New functions and bug fixes of old one. * * Revision 1.3 1993/12/17 17:15:35 dolzmann * Additional input procedures are added. * * Revision 1.2 1993/10/03 18:28:04 dolzmann * New version of procedure FORMKVD * * Revision 1.1 1993/07/13 14:44:07 dolzmann * The maslog-system and a simple example. * * ---------------------------------------------------------------------------- *) DEFINITION MODULE MLDEMO; (* Maslog Demonstration Definition Module. *) (****************************************************************************** * M A S L O G D E M O N S T R A T I O N * *-----------------------------------------------------------------------------* * Author: Andreas Dolzmann * * Language: Modula II (mtc or mocka are possible) * * System: Program for the computer algebra system MAS by Heinz Kredel. * * Project: MASLOG * * Remark: Library maslog is used. * * Abstract: This is a example for MASLOG. * ******************************************************************************) FROM MASSTOR IMPORT LIST; FROM MASLISPU IMPORT PROCF1, PROCP1;CONSTrcsid = "$Id: MLDEMO.md,v 1.5 1995/11/04 18:00:23 pesch Exp $";CONSTcopyright = "Copyright (c) 1993 Universitaet Passau";VAREQU, NEQ: LIST; (****************************************************************************** * I M P L E M E N T A T I O N O F T H E A T O M I C F O R M U L A S * ******************************************************************************)PROCEDURE MLDMKATOM(rel,left,right:LIST):LIST; (* maslog demonstration make atomic formula. rel is the relation symbol (either EQU or NEQ), left and right are beta integers or variables. The formula (left rel right) is returned. *) (****************************************************************************** * H I G H L E V E L P R O C E D U R E S * ******************************************************************************)PROCEDURE MLDTST(l: LIST):LIST; (* maslog demonstration test 1. l is a list; MLDTST returns 1 if l represents a formula otherwise 0. *)PROCEDURE MLDMKPOS(phi: LIST): LIST; (* maslog demonstration make positive. phi is a formula; a formula equivalent to phi, which is relative positive, is returned. Relative positive means that negations are only in front of atomic formulas. *)PROCEDURE MLDMKPOS1(phi, pref: LIST): LIST; (* maslog demonstration make positive 1. phi is a formula; pref is a symbol of the set \{ET, VEL, NON\}; a formula equivalent to phi, which is relative positive, is returned. Relative positive means that negations are only in front of atomic formulas. pref is a switch that controls the substitution of the operators IMP, REP, EQUIV, XOR.*)PROCEDURE MLDMKDNF(phi: LIST): LIST; (* maslog demonstration make disjunctive normal form. phi is a formula; MLMKDNF returns a formula in strict disjunctive normal form which is equivalent to phi. *)PROCEDURE MLDMKCNF(phi: LIST): LIST; (* maslog demonstration make disjunctive normal form. phi is a formula; MLDMKCNF returns a formula in strict conjunctive normal form which is equivalent to phi. *)PROCEDURE MLDMKPRENEX(phi, pref: LIST): LIST; (* maslog demonstration make prenex. phi is a formula; pref is an element of \{EXIST, FORALL\}; a formula psi in prenex normal form is returned. phi must be a relative positive formula without additional operation symbols like IMP, REP, etc. All bound variables in phi must have different specifications (i.e. different names or different types). The only transformation which is used to calculate psi is the interchange of a junctor with a quantifier. The formula psi has the minimal number of blocks of quantifiers under all prenex formulas which are built using only the interchange of a junctor with an quantifier. The argument pref is only respected, if there are two equivalent formulas with the same optimal number of blocks of quantifiers. In this case the formula is returned which has a "`pref"'-quantifier as the outermost operation symbol.*)PROCEDURE MLDSUBSTVAR(phi,old,new:LIST):LIST; (* maslog demonstration substitute variables. phi is a formula; old and new are variables; a formula in which the variable old is substituted by the variable new is returned. *)PROCEDURE MLDMKVD(phi: LIST):LIST; (* maslog demonstration make variables disjoint. formula is a formula, this procedure returns a formula in which all bound variables of the same sort have different names. Only the minimal number of renamings are done to make the names different.*)PROCEDURE MLDSMPL(phi: LIST): LIST; (* maslog demonstration simplify. phi is a formula; a formula phi1 equivalent to phi is returned. The formula phi1 is simplified, that means the constants VERUM and FALSUM are eliminated, and nested operators are eliminated. (In this case the procedure takes advantage of associativity of ET and VEL, and the idempotenz of NON. *)PROCEDURE MLDPREPQE(phi: LIST):LIST; (* maslog demonstration prepare quantifier elimination. phi is a prenex formu\-la; a formula psi equivalent to phi is returned. psi is built according to the following rules: If the innermost block of quantifiers is an exist-quantifier, then matrix(phi) is transformed in CNF and the innermost block of quantifiers is moved inside the conjunction. If the innermost quantifier is a forall-quantifier, then matrix(phi) is transformed in DNF and the innermost block of quantifiers is moved inside the disjunction.*)PROCEDURE MLDAPPLYAT(phi:LIST):LIST; (* maslog demonstration apply to atomic formulas. phi is a formula; the formula phi is returned and all atomic formulas are written in the outout stream. *)PROCEDURE MLDPPRT(phi: LIST); (* maslog demonstration pretty print. phi is a formula; this procedure writes the formula phi formated in the output stream. *)PROCEDURE MLDTEXW(phi: LIST); (* maslog demonstration tex write. phi is a formula; this procedure writes phi in tex style in the output stream. *)PROCEDURE MLDCONTVAR(phi,var:LIST):LIST; (* maslog demonstration contain variable. phi is a formula, var is a variable; 1 is returned, if phi contains var as an unbound variable, otherwise 0 is returned. *)PROCEDURE MLDCONTBDVAR(phi,var:LIST):LIST; (* maslog demonstration contains bound variable. phi is a formula, var is a variable; 1 is returned, if phi contains var as bound variable, otherwise 0 is returned. *)PROCEDURE MLDPREAD():LIST; (* maslog demonstration prefix read. A formula is read from the input stream. *)PROCEDURE MLDIREAD():LIST; (* maslog demonstration infix read. A formula is read from the input stream. *)ENDMLDEMO. (* -EOF- *)