import { PropositionalFormula, PropositionalArgument } from '../../../types.js';
import { EnhancedTruthTableVisualizer } from './enhancedTruthTable.js';
import { ParseTreeVisualizer } from './parseTreeVisualizer.js';
import { LogicCircuitVisualizer } from './logicCircuitVisualizer.js';
/**
* Main visualization class for propositional logic
* Provides a unified interface for different visualization options
*/
export class PropositionalVisualizer {
private truthTableVisualizer: EnhancedTruthTableVisualizer;
private parseTreeVisualizer: ParseTreeVisualizer;
private circuitVisualizer: LogicCircuitVisualizer;
constructor() {
this.truthTableVisualizer = new EnhancedTruthTableVisualizer();
this.parseTreeVisualizer = new ParseTreeVisualizer();
this.circuitVisualizer = new LogicCircuitVisualizer();
}
/**
* Generate a visualization for a propositional formula or argument
* @param input The formula or argument to visualize
* @param type Type of visualization to generate
* @param format Output format
* @returns Visualization in the requested format
*/
visualize(
input: PropositionalFormula | PropositionalArgument,
type: 'truthTable' | 'parseTree' | 'circuit' = 'truthTable',
format: 'html' | 'svg' | 'text' = 'html'
): string {
// Generate the requested visualization type
switch (type) {
case 'truthTable':
// Use the enhanced truth table visualizer
return this.truthTableVisualizer.generateTruthTable(input, format);
case 'parseTree':
if ('premises' in input) {
// For arguments, generate a combined parse tree
return this.generateCombinedParseTree(input, format);
} else {
// For single formulas, generate a standard parse tree
return this.parseTreeVisualizer.generateParseTree(input);
}
case 'circuit':
return this.circuitVisualizer.visualize(input, format);
default:
// Use the enhanced truth table visualizer as default
return this.truthTableVisualizer.generateTruthTable(input, format);
}
}
/**
* Generate a combined parse tree for a propositional argument
* @param argument The argument to visualize
* @param format Output format
* @returns Visualization in the requested format
*/
private generateCombinedParseTree(
argument: PropositionalArgument,
format: 'html' | 'svg' | 'text'
): string {
// Create individual parse trees for each formula
const premiseTrees = argument.premises.map(premise =>
this.parseTreeVisualizer.generateParseTree(premise)
);
const conclusionTree = this.parseTreeVisualizer.generateParseTree(argument.conclusion);
// Combine trees into a single HTML layout
if (format === 'html' || format === 'text') {
let html = '<div class="combined-parse-tree">\n';
// Add premise trees
html += '<div class="premises">\n';
argument.premises.forEach((premise, index) => {
html += `<div class="premise">\n`;
html += `<h3>Premise ${index + 1}: ${this.formatFormula(premise)}</h3>\n`;
html += premiseTrees[index];
html += '</div>\n';
});
html += '</div>\n';
// Add therefore symbol
html += '<div class="therefore">\n';
html += '<h2>∴ (Therefore)</h2>\n';
html += '</div>\n';
// Add conclusion tree
html += '<div class="conclusion">\n';
html += `<h3>Conclusion: ${this.formatFormula(argument.conclusion)}</h3>\n`;
html += conclusionTree;
html += '</div>\n';
// Add CSS styling
html += `
<style>
.combined-parse-tree {
font-family: Arial, sans-serif;
margin: 20px 0;
}
.premises {
display: flex;
flex-wrap: wrap;
justify-content: center;
gap: 20px;
margin-bottom: 20px;
}
.premise, .conclusion {
border: 1px solid #ddd;
border-radius: 10px;
padding: 10px;
background-color: #f9f9f9;
}
.premise h3, .conclusion h3 {
text-align: center;
margin: 0 0 10px 0;
}
.therefore {
text-align: center;
margin: 20px 0;
}
.therefore h2 {
font-size: 24px;
margin: 0;
}
.conclusion {
margin: 0 auto;
max-width: 80%;
}
</style>
`;
html += '</div>';
return html;
} else {
// For SVG format, just return the conclusion tree for now
// A fully combined SVG would require more complex layout calculations
return conclusionTree;
}
}
// Method removed: generateArgumentTruthTable - now using EnhancedTruthTableVisualizer directly
/**
* Format a propositional formula as a string
* @param formula The formula to format
* @returns Formatted string representation
*/
private formatFormula(formula: PropositionalFormula): string {
switch (formula.type) {
case 'variable':
return formula.name;
case 'unary':
const unaryOpSymbol = formula.operator === 'not' ? '¬' : formula.operator;
const operand = this.formatFormula(formula.operand);
// Add parentheses if the operand is not a variable or another negation
if (formula.operand.type === 'binary') {
return `${unaryOpSymbol}(${operand})`;
} else {
return `${unaryOpSymbol}${operand}`;
}
case 'binary':
const left = this.formatFormula(formula.left);
const right = this.formatFormula(formula.right);
// Convert operator to symbol if needed
let operatorSymbol: string;
switch (formula.operator) {
case 'and': operatorSymbol = '∧'; break;
case 'or': operatorSymbol = '∨'; break;
case 'implies': operatorSymbol = '→'; break;
case 'iff': operatorSymbol = '↔'; break;
case 'xor': operatorSymbol = '⊕'; break;
default: operatorSymbol = formula.operator;
}
// Add parentheses around left operand if needed
const leftStr = (formula.left.type === 'binary' &&
this.getOperatorPrecedence(formula.left.operator) <
this.getOperatorPrecedence(formula.operator))
? `(${left})`
: left;
// Add parentheses around right operand if needed
const rightStr = (formula.right.type === 'binary' &&
this.getOperatorPrecedence(formula.right.operator) <=
this.getOperatorPrecedence(formula.operator))
? `(${right})`
: right;
return `${leftStr} ${operatorSymbol} ${rightStr}`;
default:
return 'Unknown formula type';
}
}
/**
* Get the precedence level of an operator
* Higher numbers indicate higher precedence
* @param operator The operator
* @returns Precedence level (number)
*/
private getOperatorPrecedence(operator: string): number {
switch (operator) {
case 'not':
case '¬':
return 4;
case 'and':
case '∧':
return 3;
case 'or':
case '∨':
return 2;
case 'implies':
case '→':
return 1;
case 'iff':
case '↔':
case 'xor':
case '⊕':
return 0;
default:
return 0;
}
}
/**
* Check if a propositional formula is a tautology
* @param formula The formula to check
* @returns Whether the formula is a tautology
*/
isTautology(formula: PropositionalFormula): boolean {
// Extract all variables in the formula
const variables = this.extractVariables(formula);
// Generate all possible variable assignments
const assignments = this.generateAssignments(variables);
// Check if the formula evaluates to true for all assignments
return assignments.every(assignment => this.evaluateFormula(formula, assignment));
}
/**
* Check if a propositional formula is a contradiction
* @param formula The formula to check
* @returns Whether the formula is a contradiction
*/
isContradiction(formula: PropositionalFormula): boolean {
// Extract all variables in the formula
const variables = this.extractVariables(formula);
// Generate all possible variable assignments
const assignments = this.generateAssignments(variables);
// Check if the formula evaluates to false for all assignments
return assignments.every(assignment => !this.evaluateFormula(formula, assignment));
}
/**
* Check if a propositional formula is a contingency (neither tautology nor contradiction)
* @param formula The formula to check
* @returns Whether the formula is a contingency
*/
isContingency(formula: PropositionalFormula): boolean {
return !this.isTautology(formula) && !this.isContradiction(formula);
}
/**
* Check if a propositional argument is valid
* @param argument The argument to check
* @returns Whether the argument is valid
*/
isArgumentValid(argument: PropositionalArgument): boolean {
// Extract all variables in the argument
const variables = new Set<string>();
argument.premises.forEach(premise => {
this.extractVariables(premise).forEach(v => variables.add(v));
});
this.extractVariables(argument.conclusion).forEach(v => variables.add(v));
// Generate all possible variable assignments
const assignments = this.generateAssignments(Array.from(variables));
// Check if the argument is valid:
// For all assignments, if all premises are true, the conclusion must be true
return assignments.every(assignment => {
const allPremisesTrue = argument.premises.every(premise =>
this.evaluateFormula(premise, assignment)
);
if (!allPremisesTrue) {
// If not all premises are true, this doesn't invalidate the argument
return true;
}
// If all premises are true, the conclusion must also be true
return this.evaluateFormula(argument.conclusion, assignment);
});
}
/**
* Extract all unique variables from a formula
* @param formula Propositional formula
* @returns Array of unique variable names
*/
private extractVariables(formula: PropositionalFormula): string[] {
const variables = new Set<string>();
const extractVarsFromFormula = (f: PropositionalFormula): void => {
if (f.type === 'variable') {
variables.add(f.name);
} else if (f.type === 'unary') {
extractVarsFromFormula(f.operand);
} else if (f.type === 'binary') {
extractVarsFromFormula(f.left);
extractVarsFromFormula(f.right);
}
};
extractVarsFromFormula(formula);
// Sort alphabetically
return Array.from(variables).sort();
}
/**
* Generate all possible truth assignments for a set of variables
* @param variables Variable names
* @returns Array of assignments (each assignment is a map from variable name to boolean value)
*/
private generateAssignments(variables: string[]): Map<string, boolean>[] {
const assignments: Map<string, boolean>[] = [];
const numAssignments = Math.pow(2, variables.length);
for (let i = 0; i < numAssignments; i++) {
const assignment = new Map<string, boolean>();
for (let j = 0; j < variables.length; j++) {
// Convert i to binary and check if the jth bit is set
const bitValue = (i & (1 << (variables.length - j - 1))) !== 0;
assignment.set(variables[j], bitValue);
}
assignments.push(assignment);
}
return assignments;
}
/**
* Evaluate a formula under a specific assignment
* @param formula The formula to evaluate
* @param assignment Variable assignment
* @returns Boolean result of evaluation
*/
private 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;
}
}
}
/**
* Find a counterexample for an invalid argument
* @param argument The argument to analyze
* @returns Assignment that makes premises true but conclusion false, or null if no counterexample exists
*/
findCounterexample(argument: PropositionalArgument): Map<string, boolean> | null {
// Extract all variables in the argument
const variables = new Set<string>();
argument.premises.forEach(premise => {
this.extractVariables(premise).forEach(v => variables.add(v));
});
this.extractVariables(argument.conclusion).forEach(v => variables.add(v));
// Generate all possible variable assignments
const assignments = this.generateAssignments(Array.from(variables));
// Look for a counterexample
for (const assignment of assignments) {
const allPremisesTrue = argument.premises.every(premise =>
this.evaluateFormula(premise, assignment)
);
if (allPremisesTrue) {
const conclusionTrue = this.evaluateFormula(argument.conclusion, assignment);
if (!conclusionTrue) {
// Found a counterexample: all premises true but conclusion false
return assignment;
}
}
}
// No counterexample found (argument is valid)
return null;
}
/**
* Format an assignment as a readable string
* @param assignment Variable assignment
* @returns Formatted string representation
*/
formatAssignment(assignment: Map<string, boolean>): string {
const parts: string[] = [];
// Sort keys alphabetically for consistent output
const keys = Array.from(assignment.keys()).sort();
keys.forEach(key => {
const value = assignment.get(key);
parts.push(`${key} = ${value ? 'T' : 'F'}`);
});
return parts.join(', ');
}
// Method removed: generateBasicTruthTable - now using EnhancedTruthTableVisualizer directly
}
