import { ProofGenerator } from './proofGenerator.js';
import { SyllogisticArgument, LogicalSolution, SolutionStep } from '../types.js';
/**
* Generates formal proofs for syllogistic arguments
*/
export class SyllogisticProofGenerator implements ProofGenerator<SyllogisticArgument> {
/**
* Generate a step-by-step proof for a syllogistic argument
* @param argument The syllogistic argument
* @returns A logical solution with proof steps
*/
generateProof(argument: SyllogisticArgument): LogicalSolution {
const steps: SolutionStep[] = [];
// Step 1: Major premise
steps.push({
index: 1,
statement: this.formatStatement(argument.majorPremise),
rule: 'Major Premise',
justification: 'Given'
});
// Step 2: Minor premise
steps.push({
index: 2,
statement: this.formatStatement(argument.minorPremise),
rule: 'Minor Premise',
justification: 'Given'
});
// Step 3: Application of syllogistic rule
const figure = this.determineFigure(argument);
const mood = this.determineMood(argument);
const syllogisticForm = this.getSyllogisticForm(mood, figure);
steps.push({
index: 3,
statement: `Application of ${syllogisticForm}`,
rule: syllogisticForm,
justification: `Syllogistic form ${mood}-${figure}`
});
// Step 4: Conclusion
steps.push({
index: 4,
statement: this.formatStatement(argument.conclusion),
rule: 'Conclusion',
justification: `From steps 1, 2 by ${syllogisticForm}`
});
return {
steps,
conclusion: this.formatStatement(argument.conclusion)
};
}
/**
* Format a syllogistic statement for display
* @param statement The syllogistic statement
* @returns Formatted string
*/
private formatStatement(statement: any): string {
const { type, subject, predicate } = statement;
switch (type) {
case 'A':
return `All ${subject} are ${predicate}`;
case 'E':
return `No ${subject} are ${predicate}`;
case 'I':
return `Some ${subject} are ${predicate}`;
case 'O':
return `Some ${subject} are not ${predicate}`;
default:
return `${subject} ${type} ${predicate}`;
}
}
/**
* Determine the figure of a syllogism
* @param argument The syllogistic argument
* @returns Figure number (1-4)
*/
private determineFigure(argument: SyllogisticArgument): number {
const majorPremise = argument.majorPremise;
const minorPremise = argument.minorPremise;
// Find the middle term (appears in both premises but not in conclusion)
const middleTerm = this.findMiddleTerm(argument);
if (!middleTerm) return 1; // Default
// Determine positions
const majorPos = majorPremise.subject === middleTerm ? 'S' : 'P';
const minorPos = minorPremise.subject === middleTerm ? 'S' : 'P';
// Map to figure
if (majorPos === 'S' && minorPos === 'P') return 3;
if (majorPos === 'P' && minorPos === 'S') return 1;
if (majorPos === 'P' && minorPos === 'P') return 2;
if (majorPos === 'S' && minorPos === 'S') return 4;
return 1; // Default
}
/**
* Determine the mood of a syllogism
* @param argument The syllogistic argument
* @returns Mood string (e.g., "AAA")
*/
private determineMood(argument: SyllogisticArgument): string {
return argument.majorPremise.type +
argument.minorPremise.type +
argument.conclusion.type;
}
/**
* Get the traditional syllogistic form name
* @param mood The mood string
* @param figure The figure number
* @returns Traditional name (e.g., "Barbara", "Celarent")
*/
private getSyllogisticForm(mood: string, figure: number): string {
const forms: { [key: string]: string } = {
'AAA-1': 'Barbara',
'EAE-1': 'Celarent',
'AII-1': 'Darii',
'EIO-1': 'Ferio',
'AEE-2': 'Camestres',
'EAE-2': 'Cesare',
'AOO-2': 'Baroco',
'EIO-2': 'Festino',
'AAI-3': 'Darapti',
'IAI-3': 'Disamis',
'AII-3': 'Datisi',
'EAO-3': 'Felapton',
'EIO-3': 'Bocardo',
'OAO-3': 'Ferison',
'AAI-4': 'Bramantip',
'AEE-4': 'Camenes',
'IAI-4': 'Dimaris',
'EAO-4': 'Fesapo',
'EIO-4': 'Fresison'
};
const key = `${mood}-${figure}`;
return forms[key] || `Syllogism ${mood}-${figure}`;
}
/**
* Find the middle term in a syllogism
* @param argument The syllogistic argument
* @returns The middle term or null
*/
private findMiddleTerm(argument: SyllogisticArgument): string | null {
const majorTerms = [argument.majorPremise.subject, argument.majorPremise.predicate];
const minorTerms = [argument.minorPremise.subject, argument.minorPremise.predicate];
const conclusionTerms = [argument.conclusion.subject, argument.conclusion.predicate];
// Middle term is in both premises but not in conclusion
for (const term of majorTerms) {
if (minorTerms.includes(term) && !conclusionTerms.includes(term)) {
return term;
}
}
return null;
}
}
