/**
* Explanation Service
* Core service for generating step-by-step explanations for proofs
* Part of simplified Phase 4d Implementation
*/
import {
LogicalSystem,
LogicResult,
LogicalSolution,
SolutionStep
} from './types.js';
import {
EnhancedSolutionStep,
EnhancedLogicalSolution,
ExplanationOptions,
ProofContext,
ExplanationGenerator
} from './types-explanations.js';
import { SyllogisticExplanationGenerator } from './explanations/syllogisticExplanation.js';
import { PropositionalExplanationGenerator } from './explanations/propositionalExplanation.js';
import { PredicateExplanationGenerator } from './explanations/predicateExplanation.js';
import { MathematicalExplanationGenerator } from './explanations/mathematicalExplanation.js';
/**
* Manages explanation generators and provides a unified interface
* for generating explanations for different logical systems.
*/
export class ExplanationService {
private generators: Map<LogicalSystem, ExplanationGenerator>;
private defaultOptions: ExplanationOptions = {
detailLevel: 2,
includeEducationalNotes: true,
includeVisualizations: true,
includeAlternatives: false
};
/**
* Create a new explanation service with generators for all logical systems.
*/
constructor() {
this.generators = new Map();
this.initializeGenerators();
}
/**
* Initialize explanation generators for all logical systems.
*/
private initializeGenerators(): void {
this.generators.set('syllogistic', new SyllogisticExplanationGenerator());
this.generators.set('propositional', new PropositionalExplanationGenerator());
this.generators.set('predicate', new PredicateExplanationGenerator());
this.generators.set('mathematical', new MathematicalExplanationGenerator());
}
/**
* Set the default explanation options.
* @param options The new default options
*/
setDefaultOptions(options: Partial<ExplanationOptions>): void {
this.defaultOptions = {
...this.defaultOptions,
...options
};
}
/**
* Get the explanation generator for a logical system.
* @param system The logical system
* @returns The explanation generator
*/
private getGenerator(system: LogicalSystem): ExplanationGenerator {
const generator = this.generators.get(system);
if (!generator) {
throw new Error(`No explanation generator available for system: ${system}`);
}
return generator;
}
/**
* Create a proof context from a logic result.
* @param result The logic result
* @returns The proof context
*/
private createContext(result: LogicResult): ProofContext {
// Extract premises and conclusion from the result
// This is a simplified implementation - in reality, this would
// need to extract the actual premises and conclusion based on the system
const solution = result.details.solution;
return {
system: result.details.system,
originalInput: result.details.formalizedInput || '',
previousSteps: [],
premises: [], // Would extract from result based on system
conclusion: {} // Would extract from result based on system
};
}
/**
* Enhance a solution with detailed explanations.
* @param result The logic result containing the solution
* @param options Optional explanation options
* @returns Enhanced solution with detailed explanations
*/
enhanceSolution(result: LogicResult, options?: Partial<ExplanationOptions>): EnhancedLogicalSolution | null {
const solution = result.details.solution;
if (!solution) {
return null;
}
const system = result.details.system;
const generator = this.getGenerator(system);
const context = this.createContext(result);
const mergedOptions = { ...this.defaultOptions, ...options };
return generator.enhanceSolution(solution.steps, context, mergedOptions);
}
/**
* Explain a specific step in a solution.
* @param result The logic result containing the solution
* @param stepIndex The index of the step to explain (1-based)
* @param options Optional explanation options
* @returns Detailed explanation of the step
*/
explainStep(result: LogicResult, stepIndex: number, options?: Partial<ExplanationOptions>): EnhancedSolutionStep | null {
const solution = result.details.solution;
if (!solution || !solution.steps || stepIndex < 1 || stepIndex > solution.steps.length) {
return null;
}
const step = solution.steps[stepIndex - 1];
const system = result.details.system;
const generator = this.getGenerator(system);
const context = this.createContext(result);
const mergedOptions = { ...this.defaultOptions, ...options };
// Since we need a full enhanced solution to get a single step with dependencies etc.
const enhancedSolution = generator.enhanceSolution(solution.steps, context, mergedOptions);
return enhancedSolution.steps[stepIndex - 1];
}
/**
* Explain a logical rule.
* @param rule The logical rule to explain
* @param system The logical system context
* @returns Explanation of the rule
*/
explainRule(rule: string, system: LogicalSystem): string {
const generator = this.getGenerator(system);
if (!generator.generateEducationalNotes) {
return `No detailed explanation available for rule: ${rule} in system: ${system}`;
}
// Create a minimal context for rule explanation
const context: ProofContext = {
system,
originalInput: '',
previousSteps: [],
premises: [],
conclusion: {}
};
return generator.generateEducationalNotes(rule, context);
}
}
