On 21/03/17 11:26, Ralf Hemmecke wrote:
On 03/21/2017 11:50 AM, Martin Baker wrote:
Yes, but Boolean can only return true or false, there is only confusion
in logics where variable/proposition names can also be returned.
Look at what I have done to help with the evaluation of the the
signature conditions.
https://github.com/hemmecke/fricas/blob/master-hemmecke/src/doc/api.spad#L160
I haven't implemented a general graph with /\ and \/, but rather my
elements are always in "normal form", saying that I don't have an
expression tree, but the elements are always stored as DNF's. There is a
top and bottom element, called 'true' and 'false', but my
DisjunctiveNormalForm does not work over Boolean, but over a general set
S. You can let S be Integer, (or Symbol) and you would have disjunctive
normal forms with variables.
Look a bit further down, I use DisjunctiveNormalForm(SExpression).
https://github.com/hemmecke/fricas/blob/master-hemmecke/src/doc/api.spad#L377
Shouldn't ILogic() be similar to DisjunctiveNormalForm(S).
In ILogic you have no such parameter S, but rather restrict to Symbol.
To me it looks a bit like you are just creating an SExpression where
only IMPLY, AND, OR, NOT, OTHER can appear as opType (and I cannot even
create "OTHER".
What do you think is the advantage to DisjunctiveNormalForm(Symbol)
(except that DisjunctiveNormalForm is currently only in my private branch)?
I guess this relates to another recent thread about how FriCAS domains
are usually represented in a simplified form? I appreciate that
principle but I'm not sure about the consequences in this case.
So in the same way that a polynomial might be stored as a sum of
products (I realise its more complicated than that in FriCAS) a lattice
might be stored as a join of meets.
Different logics would need different rules, for instance 'Law of
excluded middle' does not apply to ILogic, and so any use of 'not' has
to be treated with care.
A Boolean algebra is a full lattice but this does not apply to Heyting
algebras which may have say bottom but no top like BoundedJoinSemilattice
So I'm not sure these types of logics could be stored in a simplified
form like this?
The impotent thing for me is that I would like these structures to link
to the stuff I'm doing in algebraic topology, using ideas in: "Topology
Via Logic" Vickers 1989.
Im not sure if/how this could be done but I would like to avoid making
changes at this stage until I've a better idea about how this could be done.
Martin B
--
You received this message because you are subscribed to the Google Groups "FriCAS -
computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to fricas-devel+unsubscr...@googlegroups.com.
To post to this group, send email to fricas-devel@googlegroups.com.
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
