diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1fcec1ae..eb47f7fd 100755
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -33,6 +33,41 @@
   This works by extracting lower/upper bounds from inequality assumptions
   and using them during comparison operations.
 
+- **Type Inference from Assumptions**: When assumptions are made, symbol types
+  are now correctly inferred. Inequality assumptions (`>`, `<`, `>=`, `<=`) set
+  the symbol's type to `real`, and equality assumptions infer the type from the
+  value (e.g., equal to an integer means type `integer`).
+
+  ```javascript
+  ce.assume(ce.box(['Greater', 'x', 4]));
+  ce.box('x').type.toString();  // → 'real' (was: 'unknown')
+
+  ce.assume(ce.box(['Equal', 'one', 1]));
+  ce.box('one').type.toString();  // → 'integer' (was: 'unknown')
+  ```
+
+- **Tautology and Contradiction Detection**: `ce.assume()` now returns
+  `'tautology'` for redundant assumptions that are already implied by existing
+  assumptions, and `'contradiction'` for assumptions that conflict with
+  existing ones.
+
+  ```javascript
+  ce.assume(ce.box(['Greater', 'x', 4]));
+
+  // Redundant assumption (x > 4 implies x > 0)
+  ce.assume(ce.box(['Greater', 'x', 0]));  // → 'tautology' (was: 'ok')
+
+  // Conflicting assumption (x > 4 contradicts x < 0)
+  ce.assume(ce.box(['Less', 'x', 0]));     // → 'contradiction'
+
+  // Same assumption repeated
+  ce.assume(ce.box(['Equal', 'one', 1]));
+  ce.assume(ce.box(['Equal', 'one', 1]));  // → 'tautology'
+
+  // Conflicting equality
+  ce.assume(ce.box(['Less', 'one', 0]));   // → 'contradiction'
+  ```
+
 ### Bug Fixes
 
 - **forget() Now Clears Assumed Values**: Fixed an issue where `ce.forget()` did not
diff --git a/requirements/DONE.md b/requirements/DONE.md
index 276f95ab..e8969a0b 100644
--- a/requirements/DONE.md
+++ b/requirements/DONE.md
@@ -1184,3 +1184,102 @@ ce.box('y').evaluate().json;  // → 'y' (was: 10)
 
 **Tests added:**
 - `test/compute-engine/bug-fixes.test.ts` - Test for scoped assumption cleanup
+
+---
+
+### 21. Type Inference from Assumptions ✅
+
+**IMPLEMENTED:** When assumptions are made, symbol types are now correctly inferred
+based on the assumption.
+
+**Problem:** When `ce.assume(['Greater', 'x', 4])` was called, the symbol's type
+remained 'unknown'. Similarly, when `ce.assume(['Equal', 'one', 1])` was called,
+the symbol's type was 'finite_integer' instead of 'integer'.
+
+**Solution:** Modified the assumption processing to update symbol types:
+
+1. **For equality assumptions**: Added `inferTypeFromValue()` function that promotes
+   specific types to more general ones (e.g., `finite_integer` → `integer`,
+   `finite_real_number` → `real`). This is used when updating the type of a symbol
+   with an inferred type.
+
+2. **For inequality assumptions**: Updated `assumeInequality()` to set the symbol's
+   type to 'real' even when the symbol was already auto-declared with an inferred type.
+
+**Type promotion rules:**
+- `finite_integer`, `integer` → `integer`
+- `rational` → `real`
+- `finite_real_number`, `real` → `real`
+- `complex`, `imaginary` → `number`
+
+**Examples that now work:**
+```typescript
+ce.assume(ce.box(['Greater', 'x', 4]));
+ce.box('x').type.toString();  // → 'real' (was: 'unknown')
+
+ce.assume(ce.box(['Equal', 'one', 1]));
+ce.box('one').type.toString();  // → 'integer' (was: 'finite_integer' or 'unknown')
+
+ce.assume(ce.box(['Greater', 't', 0]));
+ce.box('t').type.toString();  // → 'real'
+
+ce.assume(ce.box(['Equal', 'p', 11]));
+ce.box('p').type.toString();  // → 'integer'
+```
+
+**Files modified:**
+- `src/compute-engine/assume.ts` - Added `inferTypeFromValue()`, updated type inference
+
+**Tests enabled:**
+- `test/compute-engine/assumptions.test.ts` - Enabled "TYPE INFERENCE FROM ASSUMPTIONS"
+  describe block (6 tests)
+
+---
+
+### 20. Tautology and Contradiction Detection ✅
+
+**IMPLEMENTED:** `ce.assume()` now returns `'tautology'` for redundant assumptions
+that are already implied by existing assumptions, and `'contradiction'` for
+assumptions that conflict with existing ones.
+
+**Problem:** When a user made an assumption like `x > 0` after already assuming
+`x > 4`, the function would return `'ok'` even though the new assumption was
+redundant (implied by the existing one). Similarly, assuming `x < 0` when `x > 4`
+exists would silently accept a contradictory assumption.
+
+**Solution:** Added bounds checking logic in `assumeInequality()` that:
+
+1. Extracts the symbol from the inequality being assumed
+2. Retrieves existing bounds for that symbol from current assumptions
+3. Compares the new inequality against existing bounds to detect:
+   - **Tautologies**: When the new inequality is implied by existing bounds
+   - **Contradictions**: When the new inequality conflicts with existing bounds
+
+The implementation correctly handles all combinations:
+- `Greater`/`GreaterEqual` vs existing lower bounds → tautology detection
+- `Greater`/`GreaterEqual` vs existing upper bounds → contradiction detection
+- `Less`/`LessEqual` vs existing upper bounds → tautology detection
+- `Less`/`LessEqual` vs existing lower bounds → contradiction detection
+
+It also handles canonical form normalization - the compute engine canonicalizes
+`Greater(x, k)` to `Less(k, x)`, so the code determines the "effective" relationship
+based on both the operator and which operand contains the symbol.
+
+**Examples that now work:**
+```typescript
+ce.assume(ce.box(['Equal', 'one', 1]));
+ce.assume(ce.box(['Equal', 'one', 1]));   // → 'tautology' (same assumption repeated)
+ce.assume(ce.box(['Less', 'one', 0]));    // → 'contradiction' (one=1 is not < 0)
+ce.assume(ce.box(['Greater', 'one', 0])); // → 'tautology' (one=1 > 0)
+
+ce.assume(ce.box(['Greater', 'x', 4]));
+ce.assume(ce.box(['Greater', 'x', 0]));   // → 'tautology' (x > 4 implies x > 0)
+ce.assume(ce.box(['Less', 'x', 0]));      // → 'contradiction' (x > 4 contradicts x < 0)
+```
+
+**Files modified:**
+- `src/compute-engine/assume.ts` - Added bounds checking logic in `assumeInequality()`
+
+**Tests enabled:**
+- `test/compute-engine/assumptions.test.ts` - Enabled "TAUTOLOGY AND CONTRADICTION
+  DETECTION" describe block (4 tests)
diff --git a/requirements/TODO.md b/requirements/TODO.md
index 12eca548..1eb890e1 100644
--- a/requirements/TODO.md
+++ b/requirements/TODO.md
@@ -778,92 +778,15 @@ See `requirements/DONE.md` for implementation details.
 
 ---
 
-### 20. Tautology and Contradiction Detection
+### ~~20. Tautology and Contradiction Detection~~ ✅ COMPLETED
 
-**Problem:** `ce.assume()` should detect when an assumption is redundant
-(tautology) or conflicts with existing assumptions (contradiction), but
-currently it always returns `"ok"`.
-
-**Current behavior:**
-
-```typescript
-ce.assume(ce.box(['Equal', 'one', 1]));
-ce.assume(ce.box(['Equal', 'one', 1]));  // Returns: "ok" (should be "tautology")
-ce.assume(ce.box(['Less', 'one', 0]));   // Returns: "ok" (should be "contradiction")
-```
-
-**Expected behavior:**
-
-```typescript
-ce.assume(ce.box(['Equal', 'one', 1]));
-ce.assume(ce.box(['Equal', 'one', 1]));   // Should return: "tautology"
-ce.assume(ce.box(['Less', 'one', 0]));    // Should return: "contradiction"
-ce.assume(ce.box(['Greater', 'one', 0])); // Should return: "tautology" (one=1 > 0)
-
-ce.assume(ce.box(['Greater', 'x', 4]));
-ce.assume(ce.box(['Greater', 'x', 0]));   // Should return: "tautology" (implied by x > 4)
-ce.assume(ce.box(['Less', 'x', 0]));      // Should return: "contradiction"
-```
-
-**Implementation notes:**
-
-- Tautology detection: Check if the new assumption is already implied by
-  existing assumptions
-- Contradiction detection: Check if the new assumption conflicts with existing
-  assumptions
-- Requires transitive reasoning for inequalities
-- The return type of `assume()` already includes `"tautology"` and
-  `"contradiction"` as options
-
-**Files to investigate:**
-
-- `src/compute-engine/assume.ts` - `assume()` function and `AssumeResult` type
-
-**Tests:** `test/compute-engine/assumptions.test.ts` - "TAUTOLOGY AND
-CONTRADICTION DETECTION"
+See `requirements/DONE.md` for implementation details.
 
 ---
 
-### 21. Type Inference from Assumptions
-
-**Problem:** When assumptions are made, symbol types should be inferred. For
-example, `x > 4` implies `x` is real, and `one = 1` implies `one` is an integer.
+### ~~21. Type Inference from Assumptions~~ ✅ COMPLETED
 
-**Current behavior:**
-
-```typescript
-ce.assume(ce.box(['Greater', 'x', 4]));
-ce.box('x').type.toString()  // Returns: "unknown"
-
-ce.assume(ce.box(['Equal', 'one', 1]));
-ce.box('one').type.toString()  // Returns: "unknown"
-```
-
-**Expected behavior:**
-
-```typescript
-ce.assume(ce.box(['Greater', 'x', 4]));
-ce.box('x').type.toString()  // Should return: "real" (inequalities imply real numbers)
-
-ce.assume(ce.box(['Equal', 'one', 1]));
-ce.box('one').type.toString()  // Should return: "integer" (equal to integer literal)
-```
-
-**Implementation notes:**
-
-- Inequality assumptions (`>`, `<`, `>=`, `<=`) imply the symbol is `real`
-- Equality to an integer implies the symbol is `integer`
-- Equality to a rational implies the symbol is `rational`
-- This might be handled by updating the symbol's type when an assumption is made
-- Alternatively, the type getter could query assumptions
-
-**Files to investigate:**
-
-- `src/compute-engine/assume.ts` - Assumption processing
-- `src/compute-engine/boxed-expression/boxed-symbol.ts` - Symbol type resolution
-
-**Tests:** `test/compute-engine/assumptions.test.ts` - "TYPE INFERENCE FROM
-ASSUMPTIONS"
+See `requirements/DONE.md` for implementation details.
 
 ---
 
diff --git a/src/compute-engine/assume.ts b/src/compute-engine/assume.ts
index 19c6ea87..06e89f97 100755
--- a/src/compute-engine/assume.ts
+++ b/src/compute-engine/assume.ts
@@ -19,6 +19,34 @@ import {
 import { MathJsonSymbol } from '../math-json';
 import { isInequalityOperator } from './latex-syntax/utils';
 
+/**
+ * Infer a promoted type from a value expression.
+ * This promotes specific types to more general ones suitable for symbols:
+ * - finite_integer -> integer
+ * - rational -> real
+ * - finite_real_number -> real
+ * - complex/imaginary -> number
+ */
+function inferTypeFromValue(ce: ComputeEngine, value: BoxedExpression): BoxedType {
+  if (value.type.matches('integer')) {
+    // finite_integer, integer, etc. -> integer
+    return ce.type('integer');
+  }
+  if (value.type.matches('rational')) {
+    // rational -> real
+    return ce.type('real');
+  }
+  if (value.type.matches('real')) {
+    // finite_real_number, real -> real
+    return ce.type('real');
+  }
+  if (value.type.matches('complex')) {
+    // complex, imaginary -> number
+    return ce.type('number');
+  }
+  return value.type;
+}
+
 /**
  * An assumption is a predicate that is added to the current context.
  *
@@ -239,8 +267,9 @@ function assumeEquality(proposition: BoxedExpression): AssumeResult {
     // Use _setCurrentContextValue so the value is scoped to the current context
     // and will be automatically removed when the scope is popped.
     ce._setCurrentContextValue(lhs, val);
-    // If the type was inferred, update it based on the value
-    if (def.value.inferredType) def.value.type = val.type;
+    // If the type was inferred, update it based on the value.
+    // Use inferTypeFromValue to promote specific types (e.g., finite_integer -> integer)
+    if (def.value.inferredType) def.value.type = inferTypeFromValue(ce, val);
     return 'ok';
   }
 
@@ -270,8 +299,9 @@ function assumeEquality(proposition: BoxedExpression): AssumeResult {
     // Use _setCurrentContextValue so the value is scoped to the current context
     // and will be automatically removed when the scope is popped.
     ce._setCurrentContextValue(lhs, val);
-    // If the type was inferred, update it based on the value
-    if (def.value.inferredType) def.value.type = val.type;
+    // If the type was inferred, update it based on the value.
+    // Use inferTypeFromValue to promote specific types (e.g., finite_integer -> integer)
+    if (def.value.inferredType) def.value.type = inferTypeFromValue(ce, val);
     return 'ok';
   }
 
@@ -364,10 +394,139 @@ function assumeInequality(proposition: BoxedExpression): AssumeResult {
   const unknowns = result.unknowns;
   if (unknowns.length === 0) return 'not-a-predicate';
 
-  // Case 3
+  // Check if the new inequality is implied by or contradicts existing bounds
+  // (for single-symbol inequalities)
+  if (unknowns.length === 1) {
+    const symbol = unknowns[0];
+    const bounds = getInequalityBoundsFromAssumptions(ce, symbol);
+
+    // The normalized form is Less(p, 0) or LessEqual(p, 0) where p = lhs - rhs
+    // For a simple symbol case like "x > k", this becomes Less(-x + k, 0) meaning k - x < 0, i.e., x > k
+    // For "x < k", this becomes Less(x - k, 0) meaning x - k < 0, i.e., x < k
+
+    // Check if this is a simple "symbol > value" or "symbol < value" case
+    const originalOp = proposition.operator;
+    const isSymbolOnLeft = proposition.op1.symbol === symbol;
+    const otherSide = isSymbolOnLeft ? proposition.op2 : proposition.op1;
+
+    // Only do bounds checking for simple comparisons like "x > k" where k is numeric
+    if (otherSide.numericValue !== null) {
+      const k = otherSide.numericValue;
+
+      if (typeof k === 'number' && isFinite(k)) {
+        // Determine the EFFECTIVE relationship based on operator and symbol position
+        // Less(a, b) means a < b:
+        //   - if a is symbol: symbol < b, effective is "less"
+        //   - if b is symbol: a < symbol, so symbol > a, effective is "greater"
+        // Greater(a, b) means a > b:
+        //   - if a is symbol: symbol > b, effective is "greater"
+        //   - if b is symbol: a > symbol, so symbol < a, effective is "less"
+        let effectiveOp: 'greater' | 'greaterEqual' | 'less' | 'lessEqual';
+        if (originalOp === 'Greater') {
+          effectiveOp = isSymbolOnLeft ? 'greater' : 'less';
+        } else if (originalOp === 'GreaterEqual') {
+          effectiveOp = isSymbolOnLeft ? 'greaterEqual' : 'lessEqual';
+        } else if (originalOp === 'Less') {
+          effectiveOp = isSymbolOnLeft ? 'less' : 'greater';
+        } else {
+          // LessEqual
+          effectiveOp = isSymbolOnLeft ? 'lessEqual' : 'greaterEqual';
+        }
+
+        // Check for tautologies and contradictions based on existing bounds
+        if (effectiveOp === 'greater' || effectiveOp === 'greaterEqual') {
+          // We're asserting symbol > k or symbol >= k
+          const isStrict = effectiveOp === 'greater';
+
+          if (bounds.lowerBound !== undefined) {
+            const lowerVal = bounds.lowerBound.numericValue;
+            if (typeof lowerVal === 'number' && isFinite(lowerVal)) {
+              // We already know symbol > lowerVal (or >=)
+              if (isStrict) {
+                // Assuming symbol > k: tautology if existing lower bound implies this
+                // If lowerVal > k, then symbol > lowerVal > k, so symbol > k (tautology)
+                // If lowerVal == k and bound is strict, then symbol > lowerVal = k (tautology)
+                if (lowerVal > k) return 'tautology';
+                if (bounds.lowerStrict && lowerVal >= k) return 'tautology';
+              } else {
+                // Assuming symbol >= k: tautology if lowerVal >= k (with strict bound) or lowerVal > k
+                if (lowerVal > k) return 'tautology';
+                if (bounds.lowerStrict && lowerVal >= k) return 'tautology';
+                if (!bounds.lowerStrict && lowerVal >= k) return 'tautology';
+              }
+            }
+          }
+
+          if (bounds.upperBound !== undefined) {
+            const upperVal = bounds.upperBound.numericValue;
+            if (typeof upperVal === 'number' && isFinite(upperVal)) {
+              // We know symbol < upperVal (or <=), now checking symbol > k
+              if (isStrict) {
+                // Contradiction if upperVal <= k
+                if (upperVal < k) return 'contradiction';
+                if (bounds.upperStrict && upperVal <= k) return 'contradiction';
+                if (!bounds.upperStrict && upperVal <= k) return 'contradiction';
+              } else {
+                // symbol >= k: contradiction if upperVal < k
+                if (upperVal < k) return 'contradiction';
+                if (bounds.upperStrict && upperVal <= k) return 'contradiction';
+              }
+            }
+          }
+        } else {
+          // effectiveOp is 'less' or 'lessEqual'
+          // We're asserting symbol < k or symbol <= k
+          const isStrict = effectiveOp === 'less';
+
+          if (bounds.upperBound !== undefined) {
+            const upperVal = bounds.upperBound.numericValue;
+            if (typeof upperVal === 'number' && isFinite(upperVal)) {
+              // We already know symbol < upperVal (or <=)
+              if (isStrict) {
+                // Assuming symbol < k: tautology if existing upper bound implies this
+                if (upperVal < k) return 'tautology';
+                if (bounds.upperStrict && upperVal <= k) return 'tautology';
+              } else {
+                // symbol <= k: tautology if upperVal <= k
+                if (upperVal < k) return 'tautology';
+                if (upperVal <= k) return 'tautology';
+              }
+            }
+          }
+
+          if (bounds.lowerBound !== undefined) {
+            const lowerVal = bounds.lowerBound.numericValue;
+            if (typeof lowerVal === 'number' && isFinite(lowerVal)) {
+              // We know symbol > lowerVal (or >=), now checking symbol < k
+              if (isStrict) {
+                // Contradiction if lowerVal >= k
+                if (lowerVal > k) return 'contradiction';
+                if (bounds.lowerStrict && lowerVal >= k) return 'contradiction';
+                if (!bounds.lowerStrict && lowerVal >= k) return 'contradiction';
+              } else {
+                // symbol <= k: contradiction if lowerVal > k
+                if (lowerVal > k) return 'contradiction';
+                if (bounds.lowerStrict && lowerVal > k) return 'contradiction';
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+
+  // Case 3: single unknown - ensure the symbol has type 'real'
+  // (inequalities imply the symbol is a real number)
   if (unknowns.length === 1) {
-    if (!ce.lookupDefinition(unknowns[0]))
-      ce.declare(unknowns[0], { type: 'real' });
+    const symbol = unknowns[0];
+    const def = ce.lookupDefinition(symbol);
+    if (!def) {
+      // Symbol not defined yet - declare with type 'real'
+      ce.declare(symbol, { type: 'real' });
+    } else if (isValueDef(def) && def.value.inferredType) {
+      // Symbol was auto-declared with inferred type - update to 'real'
+      def.value.type = ce.type('real');
+    }
   }
 
   // Case 3, 4
diff --git a/test/compute-engine/assumptions.test.ts b/test/compute-engine/assumptions.test.ts
index cf5746ad..978f56e4 100755
--- a/test/compute-engine/assumptions.test.ts
+++ b/test/compute-engine/assumptions.test.ts
@@ -75,9 +75,9 @@ describe('INEQUALITY EVALUATION USING ASSUMPTIONS', () => {
   });
 });
 
-// TODO #20: Tautology and Contradiction Detection
+// #20: Tautology and Contradiction Detection
 // ce.assume() should return 'tautology' for redundant assumptions and 'contradiction' for conflicting ones
-describe.skip('TAUTOLOGY AND CONTRADICTION DETECTION', () => {
+describe('TAUTOLOGY AND CONTRADICTION DETECTION', () => {
   test(`assuming one = 1 again should return tautology`, () => {
     expect(ce.assume(ce.box(['Equal', 'one', 1]))).toEqual('tautology');
   });
@@ -95,9 +95,9 @@ describe.skip('TAUTOLOGY AND CONTRADICTION DETECTION', () => {
   });
 });
 
-// TODO #21: Type Inference from Assumptions
+// #21: Type Inference from Assumptions - IMPLEMENTED
 // When assumptions are made, symbol types should be inferred
-describe.skip('TYPE INFERENCE FROM ASSUMPTIONS', () => {
+describe('TYPE INFERENCE FROM ASSUMPTIONS', () => {
   test(`x should have type real (x > 4 assumed)`, () => {
     expect(ce.box('x').type.toString()).toBe('real');
   });