|Functional Programming and Type Theory||ChungAng University, Fall 2003|
Homework in natural deduction for propositional logic
Deadline: Wednesday Dec 3, at 3 pm
Implement the natural deduction rules for constructive propositional logic in Haskell using the technique which was presented last week on the blackboard!
The main idea is that a proposition is implemented as a type and a proof as a program, proof rules are functions. So, you should implement the following type constructors:
And, Or, Implies, Neg, Falsity, Truthand functions for the introduction and elimination rules like:
Andintro, Orintro1, Orintro2, Implyintro, Negintro, Truthintro, andel, orel,etc.
Sorry! I think that Falsity is not possible to define in Haskell, neither is negation, but if you have an idea how to do it I would appreciate to see it. Otherwise you can skip that part of the exercise.
As an example, the implementation of
And A B = data Andintro A B end andelim :: (and A B) -> (A -> B -> C) -> C andelim = ...Maybe it is possible to use infix syntax for the logical connectives, then your formulae look nicer. Now you can prove (i.e. find a program for) the following propositions:
More examples can be found in the link to Sweden on top of this page.
Last modified: Fri Dec 5 16:17:27 KST 2003