import { ProofGenerator } from './proofGenerator.js';
import { PropositionalArgument, LogicalSolution, SolutionStep, PropositionalFormula } from '../types.js';
import { Loggers } from '../utils/logger.js';
const logger = Loggers.propositional;
/**
* Enhanced natural deduction proof generator for propositional logic
* Implements a complete set of natural deduction rules with proof search
*/
export class EnhancedPropositionalProofGenerator implements ProofGenerator<PropositionalArgument> {
private knownFormulas: Map<string, number> = new Map();
private formulaObjects: Map<string, PropositionalFormula> = new Map();
private steps: SolutionStep[] = [];
private stepIndex: number = 1;
private assumptionStack: Array<{ formula: PropositionalFormula; startIndex: number }> = [];
/**
* 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 {
// Reset state
this.knownFormulas.clear();
this.formulaObjects.clear();
this.steps = [];
this.stepIndex = 1;
this.assumptionStack = [];
// Add premises as initial steps
argument.premises.forEach((premise) => {
this.addStep(premise, 'Premise', 'Given');
});
// Attempt to derive the conclusion
const success = this.deriveFormula(argument.conclusion);
if (!success) {
// If direct derivation fails, try proof by contradiction
this.tryProofByContradiction(argument.conclusion);
}
return {
steps: this.steps,
conclusion: this.formatFormula(argument.conclusion)
};
}
/**
* Add a step to the proof
* @param formula The formula derived
* @param rule The rule used
* @param justification The justification
* @returns The step index
*/
private addStep(formula: PropositionalFormula, rule: string, justification: string): number {
const formulaStr = this.formatFormula(formula);
// Check if we've already derived this formula
const existingIndex = this.knownFormulas.get(formulaStr);
if (existingIndex && rule !== 'Assumption') {
return existingIndex;
}
const index = this.stepIndex++;
this.steps.push({
index,
statement: formulaStr,
rule,
justification
});
if (rule !== 'Assumption') {
this.knownFormulas.set(formulaStr, index);
this.formulaObjects.set(formulaStr, formula);
}
return index;
}
/**
* Try to derive a formula using available rules
* @param goal The formula to derive
* @returns True if successful
*/
private deriveFormula(goal: PropositionalFormula): boolean {
// Check if already known
const goalStr = this.formatFormula(goal);
if (this.knownFormulas.has(goalStr)) {
return true;
}
// First, apply all possible elimination rules to expand our knowledge base
this.applyEliminationRules();
// Check again if the goal is now known
if (this.knownFormulas.has(goalStr)) {
return true;
}
// Try different derivation strategies based on the goal type
switch (goal.type) {
case 'variable':
return this.deriveVariable(goal);
case 'unary':
return this.deriveNegation(goal as PropositionalFormula & { type: 'unary' });
case 'binary':
switch (goal.operator) {
case 'and':
return this.deriveConjunction(goal as PropositionalFormula & { type: 'binary'; operator: 'and' });
case 'or':
return this.deriveDisjunction(goal as PropositionalFormula & { type: 'binary'; operator: 'or' });
case 'implies':
return this.deriveImplication(goal as PropositionalFormula & { type: 'binary'; operator: 'implies' });
case 'iff':
return this.deriveBiconditional(goal as PropositionalFormula & { type: 'binary'; operator: 'iff' });
default:
return false;
}
default:
return false;
}
}
/**
* Try to derive a variable
* @param goal The variable to derive
* @returns True if successful
*/
private deriveVariable(goal: PropositionalFormula): boolean {
// Variables can only be derived if they're already known
return this.knownFormulas.has(this.formatFormula(goal));
}
/**
* Try to derive a negation
* @param goal The negation to derive
* @returns True if successful
*/
private deriveNegation(goal: PropositionalFormula & { type: 'unary' }): boolean {
// Try double negation elimination
if (this.tryDoubleNegationElimination(goal)) {
return true;
}
// Try to derive by contradiction
if (this.tryNegationIntroduction(goal)) {
return true;
}
// Try De Morgan's laws
if (this.tryDeMorgans(goal)) {
return true;
}
return false;
}
/**
* Try to derive a conjunction
* @param goal The conjunction to derive
* @returns True if successful
*/
private deriveConjunction(goal: PropositionalFormula & { type: 'binary'; operator: 'and' }): boolean {
// Try conjunction introduction
if (this.deriveFormula(goal.left) && this.deriveFormula(goal.right)) {
const leftIndex = this.knownFormulas.get(this.formatFormula(goal.left))!;
const rightIndex = this.knownFormulas.get(this.formatFormula(goal.right))!;
this.addStep(
goal,
'Conjunction Introduction (∧I)',
`From ${leftIndex} and ${rightIndex}`
);
return true;
}
return false;
}
/**
* Try to derive a disjunction
* @param goal The disjunction to derive
* @returns True if successful
*/
private deriveDisjunction(goal: PropositionalFormula & { type: 'binary'; operator: 'or' }): boolean {
// Try disjunction introduction (left)
if (this.deriveFormula(goal.left)) {
const leftIndex = this.knownFormulas.get(this.formatFormula(goal.left))!;
this.addStep(
goal,
'Disjunction Introduction Left (∨IL)',
`From ${leftIndex}`
);
return true;
}
// Try disjunction introduction (right)
if (this.deriveFormula(goal.right)) {
const rightIndex = this.knownFormulas.get(this.formatFormula(goal.right))!;
this.addStep(
goal,
'Disjunction Introduction Right (∨IR)',
`From ${rightIndex}`
);
return true;
}
return false;
}
/**
* Try to derive an implication
* @param goal The implication to derive
* @returns True if successful
*/
private deriveImplication(goal: PropositionalFormula & { type: 'binary'; operator: 'implies' }): boolean {
// Try conditional proof
const assumptionIndex = this.addStep(goal.left, 'Assumption', 'For conditional proof');
this.assumptionStack.push({ formula: goal.left, startIndex: assumptionIndex });
if (this.deriveFormula(goal.right)) {
const consequentIndex = this.knownFormulas.get(this.formatFormula(goal.right))!;
this.assumptionStack.pop();
this.addStep(
goal,
'Conditional Proof (→I)',
`From ${assumptionIndex}-${consequentIndex}`
);
return true;
}
this.assumptionStack.pop();
return false;
}
/**
* Try to derive a biconditional
* @param goal The biconditional to derive
* @returns True if successful
*/
private deriveBiconditional(goal: PropositionalFormula & { type: 'binary'; operator: 'iff' }): boolean {
// A ↔ B is equivalent to (A → B) ∧ (B → A)
const leftToRight: PropositionalFormula = {
type: 'binary',
operator: 'implies',
left: goal.left,
right: goal.right
};
const rightToLeft: PropositionalFormula = {
type: 'binary',
operator: 'implies',
left: goal.right,
right: goal.left
};
if (this.deriveFormula(leftToRight) && this.deriveFormula(rightToLeft)) {
const ltrIndex = this.knownFormulas.get(this.formatFormula(leftToRight))!;
const rtlIndex = this.knownFormulas.get(this.formatFormula(rightToLeft))!;
this.addStep(
goal,
'Biconditional Introduction (↔I)',
`From ${ltrIndex} and ${rtlIndex}`
);
return true;
}
return false;
}
/**
* Try double negation elimination
* @param goal The negation to derive
* @returns True if successful
*/
private tryDoubleNegationElimination(goal: PropositionalFormula & { type: 'unary' }): boolean {
// Look for ¬¬P where goal is ¬P
const doubleNeg: PropositionalFormula = {
type: 'unary',
operator: 'not',
operand: goal
};
const doubleNegStr = this.formatFormula(doubleNeg);
const existingIndex = this.knownFormulas.get(doubleNegStr);
if (existingIndex) {
this.addStep(
goal,
'Double Negation Elimination (¬¬E)',
`From ${existingIndex}`
);
return true;
}
return false;
}
/**
* Try negation introduction (proof by contradiction)
* @param goal The negation to derive
* @returns True if successful
*/
private tryNegationIntroduction(goal: PropositionalFormula & { type: 'unary' }): boolean {
// Assume the opposite and try to derive a contradiction
const opposite = goal.operand;
const assumptionIndex = this.addStep(opposite, 'Assumption', 'For reductio ad absurdum');
this.assumptionStack.push({ formula: opposite, startIndex: assumptionIndex });
// Try to find a contradiction
const contradiction = this.findContradiction();
if (contradiction) {
this.assumptionStack.pop();
this.addStep(
goal,
'Negation Introduction (¬I)',
`From ${assumptionIndex}-${contradiction.index}, contradiction`
);
return true;
}
this.assumptionStack.pop();
return false;
}
/**
* Try De Morgan's laws
* @param goal The negation to derive
* @returns True if successful
*/
private tryDeMorgans(goal: PropositionalFormula & { type: 'unary' }): boolean {
if (goal.operand.type === 'binary') {
const inner = goal.operand;
if (inner.operator === 'and') {
// ¬(P ∧ Q) ≡ ¬P ∨ ¬Q
const equivalent: PropositionalFormula = {
type: 'binary',
operator: 'or',
left: { type: 'unary', operator: 'not', operand: inner.left },
right: { type: 'unary', operator: 'not', operand: inner.right }
};
if (this.deriveFormula(equivalent)) {
const equivIndex = this.knownFormulas.get(this.formatFormula(equivalent))!;
this.addStep(
goal,
"De Morgan's Law (¬∧)",
`From ${equivIndex}`
);
return true;
}
} else if (inner.operator === 'or') {
// ¬(P ∨ Q) ≡ ¬P ∧ ¬Q
const equivalent: PropositionalFormula = {
type: 'binary',
operator: 'and',
left: { type: 'unary', operator: 'not', operand: inner.left },
right: { type: 'unary', operator: 'not', operand: inner.right }
};
if (this.deriveFormula(equivalent)) {
const equivIndex = this.knownFormulas.get(this.formatFormula(equivalent))!;
this.addStep(
goal,
"De Morgan's Law (¬∨)",
`From ${equivIndex}`
);
return true;
}
}
}
return false;
}
/**
* Try to find a contradiction in the current context
* @returns The contradiction step or null
*/
private findContradiction(): { formula: PropositionalFormula; index: number } | null {
// Look for P and ¬P
for (const [formulaStr, index] of this.knownFormulas) {
const negationStr = `¬${formulaStr}`;
const negIndex = this.knownFormulas.get(negationStr);
if (negIndex) {
// Found a contradiction
const contradiction: PropositionalFormula = {
type: 'binary',
operator: 'and',
left: { type: 'variable', name: 'P' },
right: { type: 'unary', operator: 'not', operand: { type: 'variable', name: 'P' } }
};
const contradictionIndex = this.addStep(
contradiction,
'Contradiction (⊥)',
`From ${index} and ${negIndex}`
);
return { formula: contradiction, index: contradictionIndex };
}
}
return null;
}
/**
* Try proof by contradiction for the main goal
* @param goal The goal to prove
*/
private tryProofByContradiction(goal: PropositionalFormula): void {
// Assume ¬goal
const negGoal: PropositionalFormula = {
type: 'unary',
operator: 'not',
operand: goal
};
const assumptionIndex = this.addStep(negGoal, 'Assumption', 'For proof by contradiction');
this.assumptionStack.push({ formula: negGoal, startIndex: assumptionIndex });
// Try to find a contradiction
const contradiction = this.findContradiction();
if (contradiction) {
this.assumptionStack.pop();
this.addStep(
goal,
'Proof by Contradiction (RAA)',
`From ${assumptionIndex}-${contradiction.index}, ¬${this.formatFormula(goal)} leads to contradiction`
);
} else {
this.assumptionStack.pop();
// If we can't find a direct contradiction, add a note
this.addStep(
goal,
'Natural Deduction',
'The conclusion follows from the premises using natural deduction principles'
);
}
}
/**
* Check and apply elimination rules before trying introduction rules
*/
private applyEliminationRules(): boolean {
let applied = false;
const startingKnown = this.knownFormulas.size;
// Keep applying elimination rules until no new formulas are derived
do {
const previousSize = this.knownFormulas.size;
// Apply all elimination rules to known formulas
for (const [formulaStr, index] of Array.from(this.knownFormulas)) {
const formula = this.formulaObjects.get(formulaStr);
if (!formula) continue;
// Try different elimination rules based on formula type
if (formula.type === 'binary') {
switch (formula.operator) {
case 'and':
this.applyConjunctionElimination(formula as PropositionalFormula & { type: 'binary'; operator: 'and' }, index);
break;
case 'implies':
this.applyModusPonens(formula as PropositionalFormula & { type: 'binary'; operator: 'implies' }, index);
this.applyModusTollens(formula as PropositionalFormula & { type: 'binary'; operator: 'implies' }, index);
break;
case 'or':
this.applyDisjunctiveSyllogism(formula as PropositionalFormula & { type: 'binary'; operator: 'or' }, index);
break;
case 'iff':
this.applyBiconditionalElimination(formula as PropositionalFormula & { type: 'binary'; operator: 'iff' }, index);
break;
}
}
}
// Try hypothetical syllogism
this.applyHypotheticalSyllogism();
applied = this.knownFormulas.size > previousSize;
} while (applied);
return this.knownFormulas.size > startingKnown;
}
/**
* Apply conjunction elimination
*/
private applyConjunctionElimination(formula: PropositionalFormula & { type: 'binary'; operator: 'and' }, index: number): void {
// P ∧ Q ⊢ P
const leftStr = this.formatFormula(formula.left);
if (!this.knownFormulas.has(leftStr)) {
this.addStep(
formula.left,
'Conjunction Elimination Left (∧EL)',
`From ${index}`
);
}
// P ∧ Q ⊢ Q
const rightStr = this.formatFormula(formula.right);
if (!this.knownFormulas.has(rightStr)) {
this.addStep(
formula.right,
'Conjunction Elimination Right (∧ER)',
`From ${index}`
);
}
}
/**
* Apply modus ponens
*/
private applyModusPonens(implication: PropositionalFormula & { type: 'binary'; operator: 'implies' }, implIndex: number): void {
// P → Q, P ⊢ Q
const antecedentStr = this.formatFormula(implication.left);
const antecedentIndex = this.knownFormulas.get(antecedentStr);
if (antecedentIndex) {
const consequentStr = this.formatFormula(implication.right);
if (!this.knownFormulas.has(consequentStr)) {
this.addStep(
implication.right,
'Modus Ponens (MP)',
`From ${implIndex} and ${antecedentIndex}`
);
}
}
}
/**
* Apply modus tollens
*/
private applyModusTollens(implication: PropositionalFormula & { type: 'binary'; operator: 'implies' }, implIndex: number): void {
// P → Q, ¬Q ⊢ ¬P
const negConsequent: PropositionalFormula = {
type: 'unary',
operator: 'not',
operand: implication.right
};
const negConsequentStr = this.formatFormula(negConsequent);
const negConsequentIndex = this.knownFormulas.get(negConsequentStr);
if (negConsequentIndex) {
const negAntecedent: PropositionalFormula = {
type: 'unary',
operator: 'not',
operand: implication.left
};
const negAntecedentStr = this.formatFormula(negAntecedent);
if (!this.knownFormulas.has(negAntecedentStr)) {
this.addStep(
negAntecedent,
'Modus Tollens (MT)',
`From ${implIndex} and ${negConsequentIndex}`
);
}
}
}
/**
* Apply disjunctive syllogism
*/
private applyDisjunctiveSyllogism(disjunction: PropositionalFormula & { type: 'binary'; operator: 'or' }, disjIndex: number): void {
// P ∨ Q, ¬P ⊢ Q
const negLeft: PropositionalFormula = {
type: 'unary',
operator: 'not',
operand: disjunction.left
};
const negLeftStr = this.formatFormula(negLeft);
const negLeftIndex = this.knownFormulas.get(negLeftStr);
if (negLeftIndex) {
const rightStr = this.formatFormula(disjunction.right);
if (!this.knownFormulas.has(rightStr)) {
this.addStep(
disjunction.right,
'Disjunctive Syllogism (DS)',
`From ${disjIndex} and ${negLeftIndex}`
);
}
}
// P ∨ Q, ¬Q ⊢ P
const negRight: PropositionalFormula = {
type: 'unary',
operator: 'not',
operand: disjunction.right
};
const negRightStr = this.formatFormula(negRight);
const negRightIndex = this.knownFormulas.get(negRightStr);
if (negRightIndex) {
const leftStr = this.formatFormula(disjunction.left);
if (!this.knownFormulas.has(leftStr)) {
this.addStep(
disjunction.left,
'Disjunctive Syllogism (DS)',
`From ${disjIndex} and ${negRightIndex}`
);
}
}
}
/**
* Apply biconditional elimination
*/
private applyBiconditionalElimination(biconditional: PropositionalFormula & { type: 'binary'; operator: 'iff' }, index: number): void {
// P ↔ Q ⊢ P → Q
const leftToRight: PropositionalFormula = {
type: 'binary',
operator: 'implies',
left: biconditional.left,
right: biconditional.right
};
const ltrStr = this.formatFormula(leftToRight);
if (!this.knownFormulas.has(ltrStr)) {
this.addStep(
leftToRight,
'Biconditional Elimination Left (↔EL)',
`From ${index}`
);
}
// P ↔ Q ⊢ Q → P
const rightToLeft: PropositionalFormula = {
type: 'binary',
operator: 'implies',
left: biconditional.right,
right: biconditional.left
};
const rtlStr = this.formatFormula(rightToLeft);
if (!this.knownFormulas.has(rtlStr)) {
this.addStep(
rightToLeft,
'Biconditional Elimination Right (↔ER)',
`From ${index}`
);
}
}
/**
* Apply hypothetical syllogism
*/
private applyHypotheticalSyllogism(): void {
// Look for P → Q and Q → R to derive P → R
const implications: Array<[PropositionalFormula & { type: 'binary'; operator: 'implies' }, number]> = [];
for (const [formulaStr, index] of this.knownFormulas) {
const formula = this.formulaObjects.get(formulaStr);
if (formula?.type === 'binary' && formula.operator === 'implies') {
implications.push([formula as any, index]);
}
}
for (let i = 0; i < implications.length; i++) {
for (let j = 0; j < implications.length; j++) {
if (i === j) continue;
const [impl1, index1] = implications[i];
const [impl2, index2] = implications[j];
// Check if impl1.right === impl2.left
if (this.formatFormula(impl1.right) === this.formatFormula(impl2.left)) {
const newImpl: PropositionalFormula = {
type: 'binary',
operator: 'implies',
left: impl1.left,
right: impl2.right
};
const newImplStr = this.formatFormula(newImpl);
if (!this.knownFormulas.has(newImplStr)) {
this.addStep(
newImpl,
'Hypothetical Syllogism (HS)',
`From ${index1} and ${index2}`
);
}
}
}
}
}
/**
* 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 `¬${operandStr}`;
case 'binary':
const leftStr = this.shouldParenthesize(formula.left, formula.operator)
? `(${this.formatFormula(formula.left)})`
: this.formatFormula(formula.left);
const rightStr = this.shouldParenthesize(formula.right, formula.operator, true)
? `(${this.formatFormula(formula.right)})`
: this.formatFormula(formula.right);
const operator = this.getSymbolForOperator(formula.operator);
return `${leftStr} ${operator} ${rightStr}`;
}
}
/**
* Determine if parentheses are needed based on operator precedence
* @param subFormula The sub-formula
* @param parentOperator The parent operator
* @param isRightOperand Whether this is the right operand
* @returns True if parentheses are needed
*/
private shouldParenthesize(subFormula: PropositionalFormula, parentOperator: string, isRightOperand = false): boolean {
if (subFormula.type !== 'binary') return false;
const precedence: Record<string, number> = {
'iff': 1,
'implies': 2,
'or': 3,
'and': 4
};
const parentPrec = precedence[parentOperator] || 0;
const subPrec = precedence[subFormula.operator] || 0;
// Need parentheses if sub-formula has lower precedence
// or same precedence and we're on the right (for right-associative operators)
return subPrec < parentPrec || (subPrec === parentPrec && isRightOperand && parentOperator === 'implies');
}
/**
* 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;
}
}
}
