import { LogicManager } from './logicManager.js';
import { LogicalSystem, LogicResult } from './types.js';
import { Loggers } from './utils/logger.js';
const logger = Loggers.server;
export interface TranslationResult {
sourceSystem: LogicalSystem;
targetSystem: LogicalSystem;
sourceInput: string;
translatedOutput: string;
successful: boolean;
notes?: string;
limitations?: string[];
}
export class LogicTranslator {
private logicManager: LogicManager;
constructor(logicManager: LogicManager) {
this.logicManager = logicManager;
}
/**
* Translate a logical statement from one system to another
* @param input The input statement
* @param sourceSystem Source logical system
* @param targetSystem Target logical system
* @returns Translation result
*/
async translate(
input: string,
sourceSystem: LogicalSystem,
targetSystem: LogicalSystem
): Promise<TranslationResult> {
logger.info(`Translating from ${sourceSystem} to ${targetSystem}`);
const limitations: string[] = [];
let translatedOutput = '';
let successful = false;
let notes = '';
try {
// First, formalize in the source system
const formalized = await this.logicManager.process(
sourceSystem,
'formalize',
input,
'natural'
);
if (formalized.status !== 'success') {
return {
sourceSystem,
targetSystem,
sourceInput: input,
translatedOutput: '',
successful: false,
notes: `Failed to formalize in source system: ${formalized.message}`
};
}
const formalizedForm = formalized.details?.formalizedInput || input;
// Perform translation based on system pairs
const translation = this.performTranslation(
formalizedForm,
sourceSystem,
targetSystem,
limitations
);
translatedOutput = translation.output;
successful = translation.successful;
notes = translation.notes || '';
} catch (error) {
return {
sourceSystem,
targetSystem,
sourceInput: input,
translatedOutput: '',
successful: false,
notes: error instanceof Error ? error.message : 'Translation error'
};
}
return {
sourceSystem,
targetSystem,
sourceInput: input,
translatedOutput,
successful,
notes,
limitations: limitations.length > 0 ? limitations : undefined
};
}
/**
* Perform the actual translation between systems
*/
private performTranslation(
input: string,
source: LogicalSystem,
target: LogicalSystem,
limitations: string[]
): { output: string; successful: boolean; notes?: string } {
// Handle same-system "translation"
if (source === target) {
return {
output: input,
successful: true,
notes: 'No translation needed (same system)'
};
}
// Propositional → Modal
if (source === 'propositional' && target === 'modal') {
return {
output: input, // Propositional formulas are valid modal formulas
successful: true,
notes: 'Propositional formulas are embedded in modal logic (system K)'
};
}
// Propositional → Predicate
if (source === 'propositional' && target === 'predicate') {
limitations.push('Variables become 0-ary predicates');
return {
output: input.replace(/\b([A-Z])\b/g, '$1()'),
successful: true,
notes: 'Variables converted to 0-ary predicates'
};
}
// Syllogistic → Predicate
if (source === 'syllogistic' && target === 'predicate') {
return this.translateSyllogisticToPredicate(input, limitations);
}
// Modal → Propositional (remove modalities)
if (source === 'modal' && target === 'propositional') {
limitations.push('Modal operators (□, ◇) are stripped, losing modal meaning');
const stripped = input.replace(/[□◇]/g, '').replace(/\[\]/g, '').replace(/<>/g, '');
return {
output: stripped,
successful: true,
notes: 'Modal operators removed - this loses the modal semantics!'
};
}
// Predicate → Propositional (ground instances)
if (source === 'predicate' && target === 'propositional') {
limitations.push('Quantifiers removed, only propositional structure retained');
const grounded = input.replace(/∀|∃/g, '').replace(/\(.*?\)/g, '');
return {
output: grounded,
successful: true,
notes: 'Quantifiers removed - this is a lossy translation'
};
}
// Temporal → Modal (via LTL → S4)
if (source === 'temporal' && target === 'modal') {
limitations.push('Temporal operators map to modal operators with temporal interpretation');
let output = input;
output = output.replace(/\bG\b/g, '□'); // Globally → Necessity
output = output.replace(/\bF\b/g, '◇'); // Eventually → Possibility
return {
output,
successful: true,
notes: 'G→□, F→◇ (temporal modalities as S4 operators)'
};
}
// Fuzzy → Propositional (threshold)
if (source === 'fuzzy' && target === 'propositional') {
limitations.push('Fuzzy degrees of truth binarized at 0.5 threshold');
return {
output: input,
successful: true,
notes: 'Fuzzy degrees converted to binary truth (>0.5 = true)'
};
}
// Default: unsupported translation
return {
output: '',
successful: false,
notes: `Direct translation from ${source} to ${target} is not supported. Consider translating through an intermediate system.`
};
}
/**
* Translate syllogistic form to predicate logic
*/
private translateSyllogisticToPredicate(
input: string,
limitations: string[]
): { output: string; successful: boolean; notes: string } {
limitations.push('Syllogistic forms become quantified statements');
// Parse common syllogistic patterns
const patterns = [
{
pattern: /All (\w+) are (\w+)/i,
replacement: (m: string, s: string, p: string) => `∀x(${s}(x) → ${p}(x))`
},
{
pattern: /No (\w+) are (\w+)/i,
replacement: (m: string, s: string, p: string) => `∀x(${s}(x) → ¬${p}(x))`
},
{
pattern: /Some (\w+) are (\w+)/i,
replacement: (m: string, s: string, p: string) => `∃x(${s}(x) ∧ ${p}(x))`
},
{
pattern: /Some (\w+) are not (\w+)/i,
replacement: (m: string, s: string, p: string) => `∃x(${s}(x) ∧ ¬${p}(x))`
}
];
let output = input;
let matched = false;
for (const {pattern, replacement} of patterns) {
if (pattern.test(output)) {
output = output.replace(pattern, replacement as any);
matched = true;
}
}
return {
output,
successful: matched,
notes: matched
? 'Syllogistic form translated to first-order logic'
: 'Could not parse syllogistic form'
};
}
/**
* Get supported translation pairs
*/
getSupportedTranslations(): Array<{ from: LogicalSystem; to: LogicalSystem; lossy: boolean }> {
return [
{ from: 'propositional', to: 'modal', lossy: false },
{ from: 'propositional', to: 'predicate', lossy: false },
{ from: 'syllogistic', to: 'predicate', lossy: false },
{ from: 'modal', to: 'propositional', lossy: true },
{ from: 'predicate', to: 'propositional', lossy: true },
{ from: 'temporal', to: 'modal', lossy: false },
{ from: 'fuzzy', to: 'propositional', lossy: true }
];
}
}
