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.