import { PropositionalFormula } from '../../../types.js';
/**
* Truth table evaluation logic
* Handles formula evaluation under different variable assignments
*/
export class TruthTableEvaluator {
/**
* Evaluate a single formula under a specific assignment
* @param formula The formula to evaluate
* @param assignment Variable assignment
* @returns Boolean result of evaluation
*/
evaluateFormula(
formula: PropositionalFormula,
assignment: Map<string, boolean>
): boolean {
switch (formula.type) {
case 'variable':
return assignment.get(formula.name) || false;
case 'unary':
return !this.evaluateFormula(formula.operand, assignment);
case 'binary':
const left = this.evaluateFormula(formula.left, assignment);
const right = this.evaluateFormula(formula.right, assignment);
switch (formula.operator) {
case 'and':
case '∧':
return left && right;
case 'or':
case '∨':
return left || right;
case 'implies':
case '→':
return !left || right;
case 'iff':
case '↔':
return left === right;
case 'xor':
case '⊕':
return left !== right;
default:
return false;
}
}
}
/**
* Evaluate all formulas for all possible assignments
* @param formulas Propositional formulas
* @param assignments Variable assignments
* @returns 2D array of boolean results [assignmentIndex][formulaIndex]
*/
evaluateFormulas(
formulas: PropositionalFormula[],
assignments: Map<string, boolean>[]
): boolean[][] {
return assignments.map(assignment => {
return formulas.map(formula => this.evaluateFormula(formula, assignment));
});
}
/**
* Check if an argument row represents a counterexample
* @param rowResults Results for a single row
* @returns Whether this row is a counterexample
*/
isCounterexample(rowResults: boolean[]): boolean {
// A counterexample has all premises true but conclusion false
const allPremisesTrue = rowResults.slice(0, -1).every(result => result);
const conclusionFalse = !rowResults[rowResults.length - 1];
return allPremisesTrue && conclusionFalse;
}
/**
* Check if an argument is valid based on all evaluations
* @param results All evaluation results
* @returns Whether the argument is valid
*/
isArgumentValid(results: boolean[][]): boolean {
// An argument is valid if there are no counterexamples
return !results.some(rowResults => this.isCounterexample(rowResults));
}
}
