1 files changed, 38 insertions, 0 deletions
diff --git a/Logic.dcl b/Logic.dcl
new file mode 100644
index 0000000..767990f
--- /dev/null
+++ b/Logic.dcl
@@ -0,0 +1,38 @@
+definition module Logic
+
+import StdEnv
+
+// Expressions
+:: Expr = B Bool                // A constant
+        | Atom AtomName         // An atomic expression
+        | App1 Op1 Expr         // Applying an Op1 on an expression
+        | App2 Expr Op2 Expr    // Applying an Op2 on two expressions
+
+// Operators with one argument
+:: Op1  = Not   // logical not
+
+// Operators with two arguments
+:: Op2  = And   // logical and; left-associative
+        | Or    // logical or; right-associative
+        | Impl  // material implication; right-associative
+        | Equiv // equivalence; right-associative
+
+// All Chars may be used, but typically only [a-zA-Z] are used
+:: AtomName :== Char
+
+isBool  :: Expr -> Bool
+isAtom  :: Expr -> Bool
+isApp1  :: Expr -> Bool
+isApp2  :: Expr -> Bool
+isApp   :: Expr -> Bool
+
+isNot   :: Expr -> Bool
+isAnd   :: Expr -> Bool
+isOr    :: Expr -> Bool
+isImpl  :: Expr -> Bool
+isEquiv :: Expr -> Bool
+
+instance toString Op1
+instance toString Op2
+instance toString Expr
+