OKlibrary  0.2.1.6
Formulas.hpp File Reference

Plans on representations of propositional logic. More...

Go to the source code of this file.


Detailed Description

Plans on representations of propositional logic.

Todo:
Replacement of "makelist" by "create_list"
  • Supplying tests for all modified functions.
Todo:
Basic concepts
Todo:
Using Maxima expressions
  • There is a Maxima package on the topic (not in the current distribution).
  • As a second method for handling propositional logic, define appropriate new functions with appropriate properties, so that we can express propositional logic via Maxima terms.
  • Then exploit the built-in simplification methods.
  • It would be a "user-interface".
  • Simplifications would really be only the "straightforward" ones.
  • We cannot use the build-in "and, or, not", since they do not form expressions (and likely we would mess up the whole system).
  • And then perhaps we should also change their names in our tree- representation?
  • Proposed translations (trailing "o" for "operation"):
    1. "not" becomes "neo"
    2. "and" becomes "ano"
    3. "or" becomes "oro"
    4. "impl" becomes "imo"
    5. "equiv" becomes "eqo"
    6. "xor" becomes "xoo"
    7. "if-then-else" becomes "ifo"
    8. "nand" becomes "nao"
    9. "nor" becomes "noo"
    10. The Sheffer-op becomes "sho"
  • Or perhaps we should use longer (easier readable) names for our tree-representation? But then the translation becomes more tedious.
  • Attempting more readable operation-names (though less systematical):
    1. "not" becomes "nego"
    2. "and" becomes "ando"
    3. "or" becomes "oro"
    4. "impl" becomes "impo"
    5. "equiv" becomes "eqo"
    6. "xor" becomes "xoro"
    7. "if-then-else" becomes "ifo"
    8. "nand" becomes "nano"
    9. "nor" becomes "noro"
    10. The Sheffer-op becomes "sheo"
    I (OK) like these more.
  • Perhaps we should have all 16 binary operations.
    1. See ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/plans/BasicFunctions.hpp for the list.
    2. Likely we should very similar names?
  • In principle the following should do the job for the boolean basis:
    matchdeclare(logexpr,true);
    matchdeclare(logexpr2,true);
    kill(ando,oro,nego);
    declare(ando, commutative);
    declare(ando, nary);
    tellsimp(ando(true,logexpr),logexpr);
    tellsimp(ando(false,logexpr),false);
    tellsimp(ando(),true);
    tellsimp(ando(logexpr),logexpr);
    tellsimp(ando(logexpr,logexpr),logexpr);
    declare(oro, commutative);
    declare(oro, nary);
    matchdeclare(logexpr,true);
    tellsimp(oro(true,logexpr),true);
    tellsimp(oro(false,logexpr),logexpr);
    tellsimp(oro(),false);
    tellsimp(oro(logexpr),logexpr);
    tellsimp(oro(logexpr,logexpr),logexpr);
    tellsimp(ando(logexpr,oro(logexpr,logexpr2)),logexpr);
    tellsimp(oro(logexpr,ando(logexpr,logexpr2)),logexpr);
    tellsimp(oro(ando(logexpr,logexpr2),ando(logexpr,nego(logexpr2))),logexpr);
    tellsimp(ando(oro(logexpr,logexpr2),oro(logexpr,nego(logexpr2))),logexpr);
    tellsimp(nego(false), true);
    tellsimp(nego(true), false);
    tellsimp(nego(nego(logexpr)),logexpr);
    tellsimp(ando(logexpr,nego(logexpr)),false);
    tellsimp(oro(logexpr,nego(logexpr)),true);
    tellsimp(nego(ando(logexpr,logexpr2)),oro(nego(logexpr),nego(logexpr2)));
    tellsimp(nego(oro(logexpr,logexpr2)),ando(nego(logexpr),nego(logexpr2)));
       
    The last two rules could be separated (they establish NNF).
  • Are these rules together confluent? (Should be; perhaps we should install Maude, as a strong system for handling rewrite-rules.)
  • The constant-simplification apparently needs to be strengthened, so that constants in arbitrary nary-expressions (at arbitrary positions) are recognised.
  • The commutative-decl has no effect? ando(a,b) should be recognised as equal to ando(b,a) ?? It works alone, but not together with nary. So perhaps we have a bug here. Using "lassociative" instead of "nary" seems to render the whole thing useless??
  • See the neg-declarations in ComputerAlgebra/Satisfiability/Lisp/PropositionalLogic/Formulas.mac.
  • The Maxima-documentation on these issues seems completely obscure. Ask at the mailing-list.

Definition in file Formulas.hpp.