import { BaseLogicSystem } from './base.js';
import { ModalParser } from '../parsers/modalParser.js';
import { ModalValidator } from '../validators/modalValidator.js';
import { ModalProofGenerator } from '../proof/modalProofGenerator.js';
import { ModalFormula, ModalArgument, ModalSystem, LogicResult, SolutionStep } from '../types.js';
import { Loggers } from '../utils/logger.js';
const logger = Loggers.modal;
export class ModalLogic extends BaseLogicSystem {
private parser: ModalParser;
private validator: ModalValidator;
private proofGenerator: ModalProofGenerator;
private defaultSystem: ModalSystem = 'K';
constructor() {
super();
this.parser = new ModalParser();
this.validator = new ModalValidator();
this.proofGenerator = new ModalProofGenerator();
}
protected getSystemName(): 'modal' {
return 'modal';
}
validate(input: string, format: 'natural' | 'symbolic' | 'mixed' = 'mixed'): LogicResult {
try {
// Try to parse as an argument first
if (this.looksLikeArgument(input)) {
const argument = this.parser.parseArgument(input, format, this.defaultSystem);
const isValid = this.validator.isArgumentValid(argument);
let counterexample: string | undefined;
if (!isValid) {
const countermodel = this.validator.getLastCountermodel();
if (countermodel) {
counterexample = this.formatCountermodel(countermodel);
} else {
counterexample = 'A counterexample exists in some Kripke frame';
}
}
return {
status: 'success',
message: isValid ? 'The argument is valid.' : 'The argument is invalid.',
details: {
system: 'modal',
analysis: {
isValid,
explanation: this.generateArgumentExplanation(argument, isValid),
fallacies: [],
counterexample
}
}
};
} else {
// Parse as a single formula
const formula = this.parser.parse(input, format);
const isValid = this.validator.isValid(formula, this.defaultSystem);
const explanation = isValid
? `The formula ${this.parser.formatFormula(formula)} is valid in modal system ${this.defaultSystem}.`
: `The formula ${this.parser.formatFormula(formula)} is not valid in modal system ${this.defaultSystem}.`;
let counterexample: string | undefined;
if (!isValid) {
const countermodel = this.validator.getLastCountermodel();
if (countermodel) {
counterexample = this.formatCountermodel(countermodel);
}
}
return {
status: 'success',
message: explanation,
details: {
system: 'modal',
analysis: {
isValid,
explanation,
fallacies: [],
counterexample
}
}
};
}
} catch (error) {
return {
status: 'error',
message: `Error validating modal logic: ${error instanceof Error ? error.message : 'Unknown error'}`,
details: {
system: 'modal'
}
};
}
}
formalize(input: string, format: 'natural' | 'symbolic' | 'mixed' = 'natural'): LogicResult {
try {
const formula = this.parser.parse(input, format);
const formalized = this.parser.formatFormula(formula);
return {
status: 'success',
message: 'Input formalized successfully.',
details: {
system: 'modal',
formalizedInput: formalized,
}
};
} catch (error) {
return {
status: 'error',
message: `Error formalizing: ${error instanceof Error ? error.message : 'Unknown error'}`,
details: {
system: 'modal'
}
};
}
}
visualize(input: string, format: 'natural' | 'symbolic' | 'mixed' = 'mixed'): LogicResult {
try {
const formula = this.parser.parse(input, format);
return {
status: 'success',
message: 'Visualization generated successfully.',
details: {
system: 'modal',
visualization: this.generateKripkeModelVisualization(formula)
}
};
} catch (error) {
return {
status: 'error',
message: `Error visualizing: ${error instanceof Error ? error.message : 'Unknown error'}`,
details: {
system: 'modal'
}
};
}
}
solve(input: string, format: 'natural' | 'symbolic' | 'mixed' = 'mixed'): LogicResult {
try {
const argument = this.parser.parseArgument(input, format, this.defaultSystem);
const isValid = this.validator.isArgumentValid(argument);
// Use new proof generator
const proofSteps = this.proofGenerator.generateProof(argument, isValid);
let conclusion = isValid
? `The argument is valid in modal system ${argument.system}.`
: `The argument is invalid in modal system ${argument.system}.`;
// Add countermodel reference if invalid
if (!isValid) {
conclusion += ' See countermodel in validation result.';
}
return {
status: 'success',
message: 'Proof attempt completed.',
details: {
system: 'modal',
solution: {
steps: proofSteps,
conclusion
}
}
};
} catch (error) {
return {
status: 'error',
message: `Error solving: ${error instanceof Error ? error.message : 'Unknown error'}`,
details: {
system: 'modal'
}
};
}
}
setModalSystem(system: ModalSystem): void {
this.defaultSystem = system;
logger.debug(`Modal system set to ${system}`);
}
private looksLikeArgument(input: string): boolean {
return /\b(therefore|thus|hence|so|∴)\b/i.test(input);
}
private generateArgumentExplanation(argument: ModalArgument, isValid: boolean): string {
const premises = argument.premises.map((p: ModalFormula) => this.parser.formatFormula(p)).join(', ');
const conclusion = this.parser.formatFormula(argument.conclusion);
if (isValid) {
return `The argument "${premises} ∴ ${conclusion}" is valid in modal system ${argument.system}. ` +
`In all Kripke models satisfying the ${argument.system} constraints, ` +
`whenever all premises are true at a world, the conclusion is also true at that world.`;
} else {
return `The argument "${premises} ∴ ${conclusion}" is invalid in modal system ${argument.system}. ` +
`There exists a Kripke model satisfying the ${argument.system} constraints ` +
`with a world where all premises are true but the conclusion is false.`;
}
}
private generateFormalizationExplanation(original: string, formalized: string): string {
const explanations: string[] = [];
if (formalized.includes('□')) {
explanations.push('□ represents necessity ("it is necessary that")');
}
if (formalized.includes('◇')) {
explanations.push('◇ represents possibility ("it is possible that")');
}
return `Formalized "${original}" as "${formalized}". ${explanations.join('. ')}.`;
}
private generateKripkeModelVisualization(formula: ModalFormula): string {
// Generate a simple text-based Kripke model visualization
return `
Kripke Model Visualization for: ${this.parser.formatFormula(formula)}
Example Frame (System ${this.defaultSystem}):
Worlds: {w0, w1, w2}
Accessibility:
w0 → w1
w1 → w2
${this.defaultSystem !== 'K' ? 'w0 → w0 (reflexive)' : ''}
${this.defaultSystem === 'S4' || this.defaultSystem === 'S5' ? 'w0 → w2 (transitive)' : ''}
${this.defaultSystem === 'S5' ? 'w1 → w0 (symmetric)' : ''}
Valuation would depend on the specific formula.
`;
}
/**
* Format a countermodel for display
*/
private formatCountermodel(countermodel: any): string {
const { frame, failingWorld, explanation, premiseEvaluations, conclusionEvaluation } = countermodel;
let output = `\nCountermodel Found:\n`;
output += `================\n\n`;
// Show worlds
output += `Worlds: {${frame.worlds.join(', ')}}\n\n`;
// Show accessibility relation
output += `Accessibility Relation (R):\n`;
if (frame.accessibility.length === 0) {
output += ` (empty)\n`;
} else {
frame.accessibility.forEach(([from, to]: [string, string]) => {
output += ` ${from} → ${to}\n`;
});
}
output += `\n`;
// Show valuation at each world
output += `Valuations:\n`;
for (const world of frame.worlds) {
const val = frame.valuation[world] || {};
const props = Object.entries(val)
.map(([prop, truth]) => `${prop}=${truth ? 'T' : 'F'}`)
.join(', ');
output += ` ${world}: {${props || 'empty'}}\n`;
}
output += `\n`;
// Show premise evaluations if available
if (Object.keys(premiseEvaluations).length > 0) {
output += `At world ${failingWorld}:\n`;
Object.entries(premiseEvaluations).forEach(([premise, val]) => {
output += ` ${premise}: ${val ? 'TRUE' : 'FALSE'}\n`;
});
output += ` Conclusion: ${conclusionEvaluation ? 'TRUE' : 'FALSE'}\n\n`;
}
output += `${explanation}\n`;
return output;
}
}
