added exludedMiddle function in ndRules.js with tests

src/utils/expAst.js

@@ -230,5 +230,6 @@ ast.astToLaTeX = astToLaTeX;
 ast.astsToLateX = astsToLateX;
 ast.astsToString = astsToString;
 ast.containExpNode = containExpNode;
+ast.toEqual = toEqual;
 
 module.exports = ast; // Export the AST module
\ No newline at end of file

src/utils/ndRules.js

@@ -175,8 +175,8 @@ function contradiction(input) {
 
 // input list of list of ast, return list of sequents
 function axiom(input) {
-    const givens = input[0]; // list type, given list of sequent
-    const conclusion = input[1][0]; //list type of sequent
+    const givens = input[0]; // list of expressions
+    const conclusion = input[1][0]; //expression
 
     if (ast.containExpNode(givens, conclusion)) {
         return [];
@@ -186,6 +186,29 @@ function axiom(input) {
 
 } 
 
+// input list of sequent, return list of sequents
+function exludedMiddle(input) {
+    const conclusion = input[1][0]; // expression, after the turnstile
+
+    if (conclusion.type == "and") {
+        const left = conclusion.left;
+        const right = conclusion.right;
+        if (right.type == "not") {
+            if (ast.toEqual(left, right.left)) {
+                return [];
+            } else {
+                throw new Error("Invalid application for Exluded Middle law");
+            }
+        } else {
+            throw new Error("Invalid statement type for Exluded Middle law: The statement in right hand side of And must be type 'Not' to apply the law of Exluded Middle.");
+        }
+    } else {
+        throw new Error("Invalid statement type for Exluded Middle law: The statement must be type 'And' to apply the law of Exluded Middle.");
+    }
+    
+
+} 
+
 module.exports = {
     negationIntroduction,
     negationElimination,
@@ -198,5 +221,6 @@ module.exports = {
     implyIntroduction,
     implyElimination,
     contradiction,
-    axiom
+    axiom,
+    exludedMiddle
 };

tests/unit/ndRules.test.js

@@ -10,7 +10,8 @@ const { negationIntroduction,
     implyIntroduction,
     implyElimination,
     contradiction,
-    axiom } = require('../../src/utils/ndRules');
+    axiom,
+    exludedMiddle} = require('../../src/utils/ndRules');
 const { parse } = require("../../src/utils/parser");
 
 
@@ -236,4 +237,14 @@ test('Axiom should throw an error for invalid application', () => {
     const input = parse("|- !A & B");
 
     expect(() => axiom(input)).toThrow("Invalid application for axiom rule: The list of formulas in left hand side of turnstile must contain the formula in right hand side of turnstile, to apply the imply introduction rule.");
+});
+
+//exludedMiddle
+test('exludedMiddle should return the correct premises', () => {
+
+    const input = parse("B, A |- A & !A");
+
+    const output = exludedMiddle(input);
+
+    expect(output).toEqual([parse("")]);
 });
\ No newline at end of file