sivawashere
sivawashere
/ NaturalDeduction.hs
Created
December 6, 2015 05:49
Partially implements a natural deduction system in Haskell
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE TypeOperators #-} | |
| module NaturalDeduction where | |
| data (⊥) -- no inhabitants | |
| type (¬)p = p -> (⊥) | |
| type (∧) = (,) | |
| type (∨) = Either | |
| type (→) = (->) | |
| modusTollens :: (p → q) ∧ (¬)q → (¬)p |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE RecordWildCards #-} | |
| import Data.Ratio | |
| import Linear.Matrix | |
| import Linear.V3 | |
| import Linear.Epsilon | |
| import Control.Monad.Fix | |
| type State = V3 Double | |
| data System = System { |