From: Gabriel Dos Reis <gdr@cs...> - 2011-10-15 18:25:15
[ CC:ing open-axiom-help ]
Martin Baker <ax87438@...> writes:
| Its not clear to me how best to use your (undocumented) PropositionalFormula
| domain. Should I use it over Symbol so that the propositions are represented
| by symbols as below?
Martin, you keep asserting that PropositionalFormula is undocumented but
you do not say exactly what you believe is undocumented. The domain
PropositionalFormula implements a data structures for formulae in
propositional logic, as stated in the constructor's header:
++ Description: This domain implements propositional formula build
++ over a term domain, that itself belongs to PropositionalLogic
Each and every signature exported by that domain has a description.
Why are you saying it is undocumented?
The domain constructor accepts any argument that satisfies the category
SetCageory. It produces a domain that satisfies PropositionalLogic.
The argument is not restricted so symbols, just like you would expect
from propositional logic.
It would also help if you showed the result of your script when run with