import {
LogicalSystem,
Operation,
InputFormat,
LogicResult,
PropositionalFormula,
PropositionalArgument
} from '../types.js';
// Import parsers and visualization support
import { PropositionalParser } from '../parsers/propositionalParser.js';
import { EnhancedPropositionalParser } from '../parsers/enhancedPropositionalParser.js';
import { PropositionalVisualizer } from './visualization/propositional/propositionalVisualizer.js';
// Import proof generation support
import { PropositionalProofGenerator } from '../proof/propositionalProof.js';
import { EnhancedPropositionalProofGenerator } from '../proof/enhancedPropositionalProof.js';
// Import NLP preprocessor
import { NaturalLanguageProcessor } from '../preprocessors/naturalLanguageProcessor.js';
// Import validators
import { PropositionalValidator } from '../propositionalValidator.js';
import { PropositionalValidator as FormulaEvaluator } from '../validators/propositionalValidator.js';
// Import logger
import { Loggers } from '../utils/logger.js';
const logger = Loggers.propositional;
/**
* Propositional Logic System
* Handles truth-functional reasoning with logical operators
*/
export class PropositionalLogic {
private parser: PropositionalParser;
private enhancedParser: EnhancedPropositionalParser;
private visualizer: PropositionalVisualizer;
private proofGenerator: PropositionalProofGenerator;
private enhancedProofGenerator: EnhancedPropositionalProofGenerator;
private nlpProcessor: NaturalLanguageProcessor;
private variableMap: Map<string, string> = new Map();
constructor() {
this.parser = new PropositionalParser();
this.enhancedParser = new EnhancedPropositionalParser();
this.visualizer = new PropositionalVisualizer();
this.proofGenerator = new PropositionalProofGenerator();
this.enhancedProofGenerator = new EnhancedPropositionalProofGenerator();
this.nlpProcessor = new NaturalLanguageProcessor();
}
/**
* Main entry point for propositional logic operations
* @param operation The operation to perform
* @param input Input text or structured data
* @param format Input format
* @returns Operation result
*/
process(
operation: Operation,
input: string | PropositionalFormula | PropositionalArgument,
format: InputFormat = 'natural'
): LogicResult {
try {
// Reset state
this.variableMap = new Map<string, string>();
// Parse the input if it's a string
const parsedInput = typeof input === 'string'
? this.parseInput(input, format)
: input;
// Perform the requested operation
switch (operation) {
case 'validate':
return this.analyzeValidity(parsedInput);
case 'formalize':
return this.formatProposition(parsedInput);
case 'visualize':
return this.generateVisualization(parsedInput);
case 'solve':
return this.generateProof(parsedInput);
default:
throw new Error(`Unsupported operation: ${operation}`);
}
} catch (error) {
// Return an error result
return {
status: 'error',
message: error instanceof Error ? error.message : 'Unknown error',
details: {
system: 'propositional'
}
};
}
}
/**
* Parse input text into structured propositional logic
* @param input Input text
* @param format Input format
* @returns Parsed propositional formula or argument
*/
private parseInput(
input: string,
format: InputFormat
): PropositionalFormula | PropositionalArgument {
logger.debug('Parsing input', { input, format });
// Preprocess natural language if needed
let processedInput = input;
if (format === 'natural') {
// IMPORTANT: Check if this is an argument BEFORE preprocessing
// The enhanced parser removes periods which breaks argument detection
const looksLikeArgument = this.looksLikeArgument(input);
logger.debug('Argument detection check', { looksLikeArgument, input });
if (looksLikeArgument) {
// Use standard parser for arguments (it handles period-separated premises)
logger.debug('Using standard parser for argument');
return this.parser.parse(input);
}
// Use the NLP processor to preprocess the input
const nlpResult = this.nlpProcessor.preprocess(input);
processedInput = nlpResult.processedInput;
try {
// Use the enhanced parser for natural language input
const parseResult = this.enhancedParser.parse(processedInput);
this.variableMap = parseResult.variableMap;
return parseResult.formula;
} catch (error) {
// Fall back to standard parser if enhanced parser fails
logger.warn("Enhanced parser failed, falling back to standard parser", {
error: error instanceof Error ? error.message : String(error),
input: processedInput
});
return this.parser.parse(input); // Use original input, not processed
}
} else {
// Use the standard parser for symbolic/formal input
logger.debug('Using standard parser for symbolic input');
try {
const result = this.parser.parse(processedInput);
logger.debug('Parse successful', {
isArgument: 'premises' in result,
resultType: 'premises' in result ? 'argument' : 'formula'
});
return result;
} catch (error) {
logger.error('Standard parser failed', {
error: error instanceof Error ? error.message : String(error),
input: processedInput
});
throw error;
}
}
}
/**
* Check if input looks like an argument (before preprocessing)
* @param input Input string
* @returns True if it looks like an argument
*/
private looksLikeArgument(input: string): boolean {
const normalized = input.toLowerCase();
return normalized.includes('therefore') ||
normalized.includes('thus') ||
normalized.includes('hence') ||
normalized.includes('∴') ||
(normalized.includes(',') && normalized.split(',').length > 2) ||
(normalized.includes('.') && normalized.split('.').filter(s => s.trim()).length >= 3);
}
/**
* Analyze validity of a propositional formula or argument
* @param input The formula or argument to analyze
* @returns Analysis result
*/
private analyzeValidity(
input: PropositionalFormula | PropositionalArgument
): LogicResult {
// Check if the input is an argument or a formula
const isArgument = 'premises' in input;
if (isArgument) {
// Use the validator for arguments
const argument = input as PropositionalArgument;
const validator = new PropositionalValidator();
const result = validator.validateArgument(argument);
// Add variable mapping to the explanation if available
let explanation = result.explanation;
if (this.variableMap.size > 0) {
explanation += "\n\nVariable mapping:\n";
for (const [statement, variable] of this.variableMap.entries()) {
explanation += `• ${statement}: ${variable}\n`;
}
}
return {
status: 'success',
message: result.isValid ? 'The argument is valid.' : 'The argument is invalid.',
details: {
system: 'propositional',
analysis: {
...result,
explanation
}
}
};
} else {
// For standalone formulas, provide basic tautology/contradiction analysis
const formula = input as PropositionalFormula;
// Check tautology/contradiction by testing all truth value combinations
const variables = this.extractVariables(formula);
const { isTautology, isContradiction } = this.checkTautologyContradiction(formula, variables);
// Build explanation with variable mapping if available
let explanation = isTautology
? 'This formula is a tautology (always true).'
: isContradiction
? 'This formula is a contradiction (always false).'
: 'This formula is contingent (neither tautology nor contradiction).';
if (this.variableMap.size > 0) {
explanation += "\n\nVariable mapping:\n";
for (const [statement, variable] of this.variableMap.entries()) {
explanation += `• ${statement}: ${variable}\n`;
}
}
const analysis = {
isValid: isTautology,
fallacies: [] as any[],
explanation
};
return {
status: 'success',
message: analysis.explanation,
details: {
system: 'propositional',
analysis
}
};
}
}
/**
* Format a propositional formula or argument
* @param input The formula or argument to format
* @returns Formatting result
*/
private formatProposition(
input: PropositionalFormula | PropositionalArgument
): LogicResult {
// Convert to formal logic notation
const formatted = this.formatToLogicalNotation(input);
// Include variable mapping if available
let formattedWithMapping = formatted;
if (this.variableMap.size > 0) {
formattedWithMapping += "\n\nVariable mapping:\n";
for (const [statement, variable] of this.variableMap.entries()) {
formattedWithMapping += `• ${statement}: ${variable}\n`;
}
}
return {
status: 'success',
message: 'Input formatted successfully.',
details: {
system: 'propositional',
formalizedInput: formattedWithMapping
}
};
}
/**
* Convert propositional input to logical notation
* @param input Input formula or argument
* @returns Formatted logical notation
*/
private formatToLogicalNotation(input: PropositionalFormula | PropositionalArgument): string {
// Check if input is an argument or formula
if ('premises' in input) {
const argument = input as PropositionalArgument;
const premiseStrings = argument.premises.map(
(premise, index) => `Premise ${index + 1}: ${this.formulaToString(premise)}`
);
return [
...premiseStrings,
`Conclusion: ${this.formulaToString(argument.conclusion)}`
].join('\n');
} else {
// Format single formula
return this.formulaToString(input as PropositionalFormula);
}
}
/**
* Convert a formula to string representation
* @param formula Formula to convert
* @returns String representation
*/
private formulaToString(formula: PropositionalFormula): string {
switch (formula.type) {
case 'variable':
return formula.name;
case 'unary':
return `¬${this.formulaToString(formula.operand)}`;
case 'binary':
const left = this.formulaToString(formula.left);
const right = this.formulaToString(formula.right);
const operator = this.getOperatorSymbol(formula.operator);
return `(${left} ${operator} ${right})`;
default:
return 'unknown formula';
}
}
/**
* Get symbol for logical operator
* @param operator Operator name
* @returns Operator symbol
*/
private getOperatorSymbol(operator: string): string {
switch (operator) {
case 'and': return '∧';
case 'or': return '∨';
case 'implies': return '→';
case 'iff': return '↔';
case 'xor': return '⊕';
default: return operator;
}
}
/**
* Generate a visualization for a propositional formula or argument
* @param input The formula or argument to visualize
* @returns Visualization result
*/
private generateVisualization(
input: PropositionalFormula | PropositionalArgument
): LogicResult {
// Use the visualizer to generate different types of visualizations
const visualization = this.visualizer.visualize(input, 'circuit', 'svg');
// Add variable mapping if available
let fullVisualization = visualization;
if (this.variableMap.size > 0) {
fullVisualization += "\n\nVariable mapping:\n";
for (const [statement, variable] of this.variableMap.entries()) {
fullVisualization += `• ${statement}: ${variable}\n`;
}
}
// Return the result
return {
status: 'success',
message: 'Visualization generated successfully.',
details: {
system: 'propositional',
visualization: fullVisualization
}
};
}
/**
* Generate a proof for a propositional formula or argument
* @param input The formula or argument to prove
* @returns Proof result
*/
private generateProof(
input: PropositionalFormula | PropositionalArgument
): LogicResult {
// Check if input is an argument (has premises and conclusion)
if ('premises' in input) {
// Use the enhanced proof generator for arguments
const argument = input as PropositionalArgument;
const solution = this.enhancedProofGenerator.generateProof(argument);
// Add variable mapping to the solution if available
if (this.variableMap.size > 0) {
let mappingExplanation = "Variable mapping:\n";
for (const [statement, variable] of this.variableMap.entries()) {
mappingExplanation += `• ${statement}: ${variable}\n`;
}
// Add mapping as an initial step
solution.steps.unshift({
index: 0,
statement: mappingExplanation,
rule: 'Variable Assignment',
justification: 'Natural language translated to logical variables'
});
}
return {
status: 'success',
message: 'Proof generated successfully.',
details: {
system: 'propositional',
solution
}
};
} else {
// For standalone formulas, provide basic analysis
return {
status: 'success',
message: 'Formula analyzed (proof requires premises and conclusion).',
details: {
system: 'propositional',
solution: {
steps: [
{
index: 1,
statement: 'Formula provided without premises.',
rule: 'Analysis',
justification: 'A full proof requires both premises and a conclusion.'
}
],
conclusion: 'Please provide premises and a conclusion to generate a proof.'
}
}
};
}
}
/**
* Extract all variables from a formula
* @param formula Formula to extract variables from
* @returns Set of variable names
*/
private extractVariables(formula: PropositionalFormula): Set<string> {
const variables = new Set<string>();
const traverse = (f: PropositionalFormula) => {
if (f.type === 'variable') {
variables.add(f.name);
} else if (f.type === 'unary') {
traverse(f.operand);
} else if (f.type === 'binary') {
traverse(f.left);
traverse(f.right);
}
};
traverse(formula);
return variables;
}
/**
* Check if a formula is a tautology or contradiction
* @param formula Formula to check
* @param variables Set of variables in the formula
* @returns Object indicating if formula is tautology or contradiction
*/
private checkTautologyContradiction(
formula: PropositionalFormula,
variables: Set<string>
): { isTautology: boolean; isContradiction: boolean } {
const varArray = Array.from(variables);
const numVars = varArray.length;
// If no variables, evaluate once
if (numVars === 0) {
const evaluator = new FormulaEvaluator();
const value = evaluator.evaluate(formula, {});
return {
isTautology: value,
isContradiction: !value
};
}
// Test all 2^n combinations of truth values
const numCombinations = Math.pow(2, numVars);
let allTrue = true;
let allFalse = true;
const evaluator = new FormulaEvaluator();
for (let i = 0; i < numCombinations; i++) {
const valuation: { [atom: string]: boolean } = {};
// Generate truth value assignment for this combination
for (let j = 0; j < numVars; j++) {
const bitValue = (i >> j) & 1;
valuation[varArray[j]] = bitValue === 1;
}
// Evaluate formula with this valuation
const result = evaluator.evaluate(formula, valuation);
if (!result) allTrue = false;
if (result) allFalse = false;
// Early exit if we know it's contingent
if (!allTrue && !allFalse) break;
}
return {
isTautology: allTrue,
isContradiction: allFalse
};
}
}
