Waldek, Thanks, do you intend putting this into FriCAS? I looked in SVN trunk and boolean.spad.pamphlet has not changed recently, or have you put it somewhere else?
The comments below are very useful. I suspect it may also be useful to others who may work on the code so, if you do put this into FriCAS, it would be helpful if you could cut&paste these notes into the pamphlet file. Thanks again, Martin On Monday 31 Oct 2011 20:29:54 Waldek Hebisch wrote: > Martin Baker wrote: > > Gaby, > > > > 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? > > By definition propositional formula is build from atomic formulas > using logical connectives. Which kind of atomic formulas you > use depends on your needs. Symbols are good to represent variables, > but you may wish to use something more fancy like your typed > variables. But you may also represent formulas form differnet > theories, for example you may use comparisons between variables > as atomic formulas to handle orders. Or you may use equality > and inequality between polynomials to represent quantifier-free > part of ring theory. The point is that PropositionalFormula > domains imposes no interpretation on atomic formulas, it > only performs logical operations for which it needs to know > if two atomic formulas are equal or not. Of course, to take > advantage of more interesting atomic formulas you need to > add extra code, but the point is that it should be possible > reusing PropositionalFormula for what it can do. To get > the spirit Google for "SMT solvers" or Nelson-Oppen > (PropositionalFormula is a toy compared to serious SMT > solvers, but SMT solvers show that one can sucessfully > decuple propositional resoning for resonings specific > to given theory). > > > Also its written using Kernel, what is the advantage of this? > > Kernel-s are cached, so there is only one kernel with given > arguments. That makes testing equality faster. It > is easier to detect if formula changed (some simplifications > are applied as long as formula changes). Also, some > transformations if done naively would duplicate subformulas. > Due to recursion this can easily lead to exponential growth > of formula size. Caching of kernels means that some > subformulas are automatically shared, limiting possibility > of running out of memory and saving processing time. > > > Martin > > ------------------------------------------------ > > (ran in FriCAS using Waldeks translation) > > > > Type: PropositionalFormula(Symbol) > > > > (5) -> pq := p /\ q > > > > Internal Error > > The function /\ with signature hashcode is missing from domain > > > > PropositionalFormula(Symbol) > > ... > > > (8) -> dual(pq) > > Function: ?=? : (%,%) -> Boolean is missing from domain: > > PropositionalFormula(Polynomial(Integer)) > > > > Internal Error > > The function = with signature (Boolean)$$ is missing from domain > > > > PropositionalFormula(Polynomial (Integer)) > > ... > > > (8) -> simplify(conjunction(b := true()$PROP,pq)) > > Function: ?=? : (%,%) -> Boolean is missing from domain: > > PropositionalFormula(Symbol) > > > > Internal Error > > The function = with signature (Boolean)$$ is missing from domain > > > > PropositionalFormula(Symbol) > > Below is new version with this problem fixed. It uses changed > Product, so you need FriCAS from svn to compile it. -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To post to this group, send email to [email protected]. To unsubscribe from this group, send email to [email protected]. For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en.
