The last update to computation framework represented variable types by using the intuitionistic logic domain. I would like to implement the other part of Curry-Howard correspondence, 'proof as a program'. That is, implement an equivalence between a proof in propositional logic and the lambda domain.
As far as I can see, Axiom and FriCAS do not yet implement propositional logic but OpenAxiom does. I realise the forks are gradually drifting apart but, as a user, I would find life a little easier if these differences were minimised (I find it hard enough to understand one version of panAxiom, I don't think I can work on all 3). So, I guess what I am asking is: would it make sense for me to try to implement the OpenAxiom PropositionalLogic category and PropositionalFormula domain in FriCAS? If I did this, would the PropositionalFormula domain have some equivalence to the Lambda domain in computation framework? If so, would it make sense to include both these domains? OpenAxiom PropositionalLogic uses Kernel domain as its representation and I have some have some issues trying to understand this, as discussed here: http://groups.google.com/group/fricas-devel/browse_thread/thread/f39862f4a243239b?hl=en# (especially as PropositionalLogic and Kernel have minimal documentation) I think what is required is for this proposed propositional logic domain to implement the formation, introduction, elimination and computation rules for 'and', 'or' and 'implication'. the introduction rule for implication would then correspond to the creation of a lambda function and the elimination rule for implication would then correspond to the application of this function. I'm not quite sure how alpha and beta reduction would be implemented in propositional logic? Martin -- 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.
