import { ProofGenerator } from './proofGenerator.js';
import { PropositionalArgument, LogicalSolution, SolutionStep, PropositionalFormula } from '../types.js';
/**
* Generates natural deduction proofs for propositional logic arguments
*/
export class PropositionalProofGenerator implements ProofGenerator<PropositionalArgument> {
/**
* Generate a natural deduction proof for a propositional argument
* @param argument The propositional argument
* @returns A logical solution with proof steps
*/
generateProof(argument: PropositionalArgument): LogicalSolution {
const steps: SolutionStep[] = [];
// Add premises as initial steps
argument.premises.forEach((premise, index) => {
steps.push({
index: index + 1,
statement: this.formatFormula(premise),
rule: 'Premise',
justification: 'Given'
});
});
// Attempt to derive the conclusion using natural deduction rules
const derivationSteps = this.deriveConclusion(argument.premises, argument.conclusion);
// Add derivation steps
let stepIndex = argument.premises.length + 1;
derivationSteps.forEach(derivationStep => {
steps.push({
index: stepIndex++,
statement: derivationStep.statement,
rule: derivationStep.rule,
justification: derivationStep.justification
});
});
return {
steps,
conclusion: this.formatFormula(argument.conclusion)
};
}
/**
* Format a propositional formula for display
* @param formula The formula to format
* @returns Formatted string
*/
private formatFormula(formula: PropositionalFormula): string {
switch (formula.type) {
case 'variable':
return formula.name;
case 'unary':
const operandStr = formula.operand.type === 'binary'
? `(${this.formatFormula(formula.operand)})`
: this.formatFormula(formula.operand);
return `${formula.operator === 'not' ? '¬' : formula.operator}${operandStr}`;
case 'binary':
const leftStr = formula.left.type === 'binary'
? `(${this.formatFormula(formula.left)})`
: this.formatFormula(formula.left);
const rightStr = formula.right.type === 'binary'
? `(${this.formatFormula(formula.right)})`
: this.formatFormula(formula.right);
const operator = this.getSymbolForOperator(formula.operator);
return `${leftStr} ${operator} ${rightStr}`;
}
}
/**
* Get the symbol for a logical operator
* @param operator The operator
* @returns Symbol
*/
private getSymbolForOperator(operator: string): string {
switch (operator) {
case 'and': return '∧';
case 'or': return '∨';
case 'implies': return '→';
case 'iff': return '↔';
case 'xor': return '⊕';
default: return operator;
}
}
/**
* Attempt to derive the conclusion from premises using natural deduction
* @param premises The premises
* @param conclusion The conclusion to derive
* @returns Derivation steps
*/
private deriveConclusion(premises: PropositionalFormula[], conclusion: PropositionalFormula): Array<{
statement: string;
rule: string;
justification: string;
}> {
const steps: Array<{
statement: string;
rule: string;
justification: string;
}> = [];
// For simplicity, try to match the conclusion with known patterns
// This is a basic implementation - a full proof system would be much more complex
// Check if conclusion is already a premise
const premiseIndex = this.findMatchingPremise(conclusion, premises);
if (premiseIndex !== -1) {
steps.push({
statement: this.formatFormula(conclusion),
rule: 'Identity',
justification: `From premise ${premiseIndex + 1}`
});
return steps;
}
// Check for modus ponens pattern (P → Q, P ⊢ Q)
if (this.tryModusPonens(premises, conclusion, steps)) {
return steps;
}
// Check for hypothetical syllogism (P → Q, Q → R ⊢ P → R)
if (this.tryHypotheticalSyllogism(premises, conclusion, steps)) {
return steps;
}
// Check for conjunction introduction (P, Q ⊢ P ∧ Q)
if (this.tryConjunctionIntroduction(premises, conclusion, steps)) {
return steps;
}
// Check for disjunction introduction (P ⊢ P ∨ Q or Q ⊢ P ∨ Q)
if (this.tryDisjunctionIntroduction(premises, conclusion, steps)) {
return steps;
}
// If no pattern matches, provide a general derivation note
steps.push({
statement: this.formatFormula(conclusion),
rule: 'Natural Deduction',
justification: 'Derived using natural deduction principles'
});
return steps;
}
/**
* Find a premise that matches the given formula
* @param formula The formula to find
* @param premises The premises
* @returns Index of matching premise or -1
*/
private findMatchingPremise(formula: PropositionalFormula, premises: PropositionalFormula[]): number {
return premises.findIndex(premise =>
JSON.stringify(premise) === JSON.stringify(formula)
);
}
/**
* Try to apply modus ponens rule
* @param premises The premises
* @param conclusion The conclusion
* @param steps Array to add steps to
* @returns True if modus ponens was applied
*/
private tryModusPonens(
premises: PropositionalFormula[],
conclusion: PropositionalFormula,
steps: Array<{ statement: string; rule: string; justification: string; }>
): boolean {
// Look for P → Q and P among premises
for (let i = 0; i < premises.length; i++) {
const premise = premises[i];
if (premise.type === 'binary' && premise.operator === 'implies') {
const implication = premise;
// Check if consequent matches conclusion
if (JSON.stringify(implication.right) === JSON.stringify(conclusion)) {
// Look for antecedent in premises
const antecedentIndex = this.findMatchingPremise(implication.left, premises);
if (antecedentIndex !== -1) {
steps.push({
statement: this.formatFormula(conclusion),
rule: 'Modus Ponens',
justification: `From premises ${i + 1} and ${antecedentIndex + 1}`
});
return true;
}
}
}
}
return false;
}
/**
* Try to apply hypothetical syllogism
* @param premises The premises
* @param conclusion The conclusion
* @param steps Array to add steps to
* @returns True if hypothetical syllogism was applied
*/
private tryHypotheticalSyllogism(
premises: PropositionalFormula[],
conclusion: PropositionalFormula,
steps: Array<{ statement: string; rule: string; justification: string; }>
): boolean {
// Look for P → Q and Q → R where conclusion is P → R
if (conclusion.type === 'binary' && conclusion.operator === 'implies') {
const targetImplication = conclusion;
// Find matching implications in premises
for (let i = 0; i < premises.length; i++) {
for (let j = 0; j < premises.length; j++) {
if (i !== j &&
premises[i].type === 'binary' &&
(premises[i] as any).operator === 'implies' &&
premises[j].type === 'binary' &&
(premises[j] as any).operator === 'implies') {
const imp1 = premises[i] as { type: 'binary'; operator: 'implies'; left: PropositionalFormula; right: PropositionalFormula };
const imp2 = premises[j] as { type: 'binary'; operator: 'implies'; left: PropositionalFormula; right: PropositionalFormula };
// Check for P → Q and Q → R pattern
if (JSON.stringify(imp1.right) === JSON.stringify(imp2.left) &&
JSON.stringify(imp1.left) === JSON.stringify(targetImplication.left) &&
JSON.stringify(imp2.right) === JSON.stringify(targetImplication.right)) {
steps.push({
statement: this.formatFormula(conclusion),
rule: 'Hypothetical Syllogism',
justification: `From premises ${i + 1} and ${j + 1}`
});
return true;
}
}
}
}
}
return false;
}
/**
* Try to apply conjunction introduction
* @param premises The premises
* @param conclusion The conclusion
* @param steps Array to add steps to
* @returns True if conjunction introduction was applied
*/
private tryConjunctionIntroduction(
premises: PropositionalFormula[],
conclusion: PropositionalFormula,
steps: Array<{ statement: string; rule: string; justification: string; }>
): boolean {
if (conclusion.type === 'binary' && conclusion.operator === 'and') {
const leftIndex = this.findMatchingPremise(conclusion.left, premises);
const rightIndex = this.findMatchingPremise(conclusion.right, premises);
if (leftIndex !== -1 && rightIndex !== -1) {
steps.push({
statement: this.formatFormula(conclusion),
rule: 'Conjunction Introduction',
justification: `From premises ${leftIndex + 1} and ${rightIndex + 1}`
});
return true;
}
}
return false;
}
/**
* Try to apply disjunction introduction
* @param premises The premises
* @param conclusion The conclusion
* @param steps Array to add steps to
* @returns True if disjunction introduction was applied
*/
private tryDisjunctionIntroduction(
premises: PropositionalFormula[],
conclusion: PropositionalFormula,
steps: Array<{ statement: string; rule: string; justification: string; }>
): boolean {
if (conclusion.type === 'binary' && conclusion.operator === 'or') {
// Check if either disjunct is a premise
const leftIndex = this.findMatchingPremise(conclusion.left, premises);
const rightIndex = this.findMatchingPremise(conclusion.right, premises);
if (leftIndex !== -1) {
steps.push({
statement: this.formatFormula(conclusion),
rule: 'Disjunction Introduction (Left)',
justification: `From premise ${leftIndex + 1}`
});
return true;
}
if (rightIndex !== -1) {
steps.push({
statement: this.formatFormula(conclusion),
rule: 'Disjunction Introduction (Right)',
justification: `From premise ${rightIndex + 1}`
});
return true;
}
}
return false;
}
}
