import { ProofGenerator } from './proofGenerator.js';
import { PredicateArgument, LogicalSolution, SolutionStep, PredicateFormula } from '../types.js';
import { substitute, canInstantiate, formulaEquals, formatFormula as formatFormulaUtil } from '../utils/substitution.js';
/**
* Generates formal proofs for predicate logic arguments
*/
export class PredicateProofGenerator implements ProofGenerator<PredicateArgument> {
/**
* Generate a formal proof for a predicate logic argument
* @param argument The predicate logic argument
* @returns A logical solution with proof steps
*/
generateProof(argument: PredicateArgument): 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 construct proof using inference rules
const proofSteps = this.attemptProof(argument.premises, argument.conclusion);
// Add proof steps
let stepIndex = argument.premises.length + 1;
proofSteps.forEach(proofStep => {
steps.push({
index: stepIndex++,
statement: proofStep.statement,
rule: proofStep.rule,
justification: proofStep.justification
});
});
return {
steps,
conclusion: this.formatFormula(argument.conclusion)
};
}
/**
* Format a predicate formula for display
* @param formula The formula to format
* @returns Formatted string
*/
private formatFormula(formula: PredicateFormula): string {
return formatFormulaUtil(formula);
}
/**
* Attempt to generate a proof using inference rules
* @param premises The premises
* @param conclusion The conclusion
* @returns Proof steps
*/
private attemptProof(premises: PredicateFormula[], conclusion: PredicateFormula): Array<{
statement: string;
rule: string;
justification: string;
}> {
const steps: Array<{
statement: string;
rule: string;
justification: string;
}> = [];
// Collect all derived formulas (starts with premises)
const derived: PredicateFormula[] = [...premises];
// Try universal instantiation
if (this.tryUniversalInstantiation(premises, conclusion, steps, derived)) {
return steps;
}
// Try existential generalization
if (this.tryExistentialGeneralization(premises, conclusion, steps)) {
return steps;
}
// Try modus ponens with universal instantiation
if (this.tryModusPonensWithUI(premises, conclusion, steps, derived)) {
return steps;
}
// Try simple quantifier elimination/introduction
if (this.tryQuantifierElimination(premises, conclusion, steps)) {
return steps;
}
// Try direct match (conclusion is already a premise)
if (this.tryDirectMatch(premises, conclusion, steps)) {
return steps;
}
// If no pattern matches, indicate proof not found
steps.push({
statement: this.formatFormula(conclusion),
rule: 'Proof Not Found',
justification: 'No inference rule pattern matched this argument'
});
return steps;
}
/**
* Try direct match: conclusion is exactly a premise
* @param premises The premises
* @param conclusion The conclusion
* @param steps Array to add steps to
* @returns True if pattern was applied
*/
private tryDirectMatch(
premises: PredicateFormula[],
conclusion: PredicateFormula,
steps: Array<{ statement: string; rule: string; justification: string; }>
): boolean {
for (let i = 0; i < premises.length; i++) {
if (formulaEquals(premises[i], conclusion)) {
steps.push({
statement: this.formatFormula(conclusion),
rule: 'Direct Match',
justification: `Conclusion is premise ${i + 1}`
});
return true;
}
}
return false;
}
/**
* Try universal instantiation: ∀x φ(x) ⊢ φ(t)
* @param premises The premises
* @param conclusion The conclusion
* @param steps Array to add steps to
* @param derived Array of derived formulas to update
* @returns True if pattern was applied
*/
private tryUniversalInstantiation(
premises: PredicateFormula[],
conclusion: PredicateFormula,
steps: Array<{ statement: string; rule: string; justification: string; }>,
derived: PredicateFormula[]
): boolean {
for (let i = 0; i < premises.length; i++) {
const premise = premises[i];
if (premise.type === 'quantified' && premise.quantifier === 'forall') {
// Check if conclusion can be obtained by instantiating the universal
if (canInstantiate(premise.formula, conclusion, premise.variable)) {
steps.push({
statement: this.formatFormula(conclusion),
rule: 'Universal Instantiation (UI)',
justification: `From premise ${i + 1}: ${this.formatFormula(premise)}`
});
derived.push(conclusion);
return true;
}
}
}
return false;
}
/**
* Try existential generalization: φ(t) ⊢ ∃x φ(x)
* @param premises The premises
* @param conclusion The conclusion
* @param steps Array to add steps to
* @returns True if pattern was applied
*/
private tryExistentialGeneralization(
premises: PredicateFormula[],
conclusion: PredicateFormula,
steps: Array<{ statement: string; rule: string; justification: string; }>
): boolean {
if (conclusion.type === 'quantified' && conclusion.quantifier === 'exists') {
for (let i = 0; i < premises.length; i++) {
const premise = premises[i];
// Check if premise is an instance of the existential conclusion
if (canInstantiate(conclusion.formula, premise, conclusion.variable)) {
steps.push({
statement: this.formatFormula(conclusion),
rule: 'Existential Generalization (EG)',
justification: `From premise ${i + 1}: ${this.formatFormula(premise)}`
});
return true;
}
}
}
return false;
}
/**
* Try modus ponens with universal instantiation:
* ∀x (P(x) → Q(x)), P(a) ⊢ Q(a)
* @param premises The premises
* @param conclusion The conclusion
* @param steps Array to add steps to
* @param derived Array of derived formulas
* @returns True if pattern was applied
*/
private tryModusPonensWithUI(
premises: PredicateFormula[],
conclusion: PredicateFormula,
steps: Array<{ statement: string; rule: string; justification: string; }>,
derived: PredicateFormula[]
): boolean {
// Look for universal implication and its antecedent
for (let i = 0; i < premises.length; i++) {
const premise = premises[i];
// Check if premise is ∀x (P(x) → Q(x))
if (
premise.type === 'quantified' &&
premise.quantifier === 'forall' &&
premise.formula.type === 'binary' &&
premise.formula.operator === 'implies'
) {
const implication = premise.formula;
const variable = premise.variable;
// Try to find an instantiation of the antecedent in premises
for (let j = 0; j < premises.length; j++) {
if (i === j) continue;
const otherPremise = premises[j];
// Check if otherPremise matches P(t) for some term t
if (canInstantiate(implication.left, otherPremise, variable)) {
// Instantiate the consequent Q(t)
try {
// Find what term to substitute
const instantiatedConsequent = this.instantiateForMatch(
implication.right,
implication.left,
otherPremise,
variable
);
// Check if this matches our conclusion
if (formulaEquals(instantiatedConsequent, conclusion)) {
// Add intermediate steps
const instantiatedImplication = this.instantiateForMatch(
premise.formula,
implication.left,
otherPremise,
variable
);
steps.push({
statement: this.formatFormula(instantiatedImplication),
rule: 'Universal Instantiation (UI)',
justification: `From premise ${i + 1}: ${this.formatFormula(premise)}`
});
steps.push({
statement: this.formatFormula(conclusion),
rule: 'Modus Ponens (MP)',
justification: `From premise ${j + 1} and instantiated implication`
});
derived.push(conclusion);
return true;
}
} catch {
// Substitution failed, try next
continue;
}
}
}
}
}
return false;
}
/**
* Instantiate a formula based on matching another formula
* @param formula The formula to instantiate
* @param template The template to match against
* @param instance The instance that template should match
* @param variable The variable to substitute
* @returns The instantiated formula
*/
private instantiateForMatch(
formula: PredicateFormula,
template: PredicateFormula,
instance: PredicateFormula,
variable: string
): PredicateFormula {
// Find what term to substitute for variable
const term = this.findSubstitutionTerm(template, instance, variable);
if (term === null) {
throw new Error('Cannot find substitution term');
}
// Apply substitution
return substitute(formula, variable, term);
}
/**
* Find the term to substitute for a variable
* @param template The template formula
* @param instance The instance formula
* @param variable The variable to find substitution for
* @returns The term to substitute, or null if not found
*/
private findSubstitutionTerm(
template: PredicateFormula,
instance: PredicateFormula,
variable: string
): PredicateFormula | null {
// Base case: if template is the variable, return instance
if (template.type === 'variable' && template.name === variable) {
return instance;
}
// If types don't match, no substitution
if (template.type !== instance.type) {
return null;
}
// Recursively search based on type
switch (template.type) {
case 'predicate':
if (
instance.type === 'predicate' &&
template.name === instance.name &&
template.args.length === instance.args.length
) {
for (let i = 0; i < template.args.length; i++) {
const term = this.findSubstitutionTerm(template.args[i], instance.args[i], variable);
if (term !== null) {
return term;
}
}
}
return null;
case 'function':
if (
instance.type === 'function' &&
template.name === instance.name &&
template.args.length === instance.args.length
) {
for (let i = 0; i < template.args.length; i++) {
const term = this.findSubstitutionTerm(template.args[i], instance.args[i], variable);
if (term !== null) {
return term;
}
}
}
return null;
case 'binary':
if (instance.type === 'binary' && template.operator === instance.operator) {
const leftTerm = this.findSubstitutionTerm(template.left, instance.left, variable);
if (leftTerm !== null) {
return leftTerm;
}
return this.findSubstitutionTerm(template.right, instance.right, variable);
}
return null;
case 'unary':
if (instance.type === 'unary' && template.operator === instance.operator) {
return this.findSubstitutionTerm(template.operand, instance.operand, variable);
}
return null;
default:
return null;
}
}
/**
* Try quantifier elimination and introduction patterns
* @param premises The premises
* @param conclusion The conclusion
* @param steps Array to add steps to
* @returns True if pattern was applied
*/
private tryQuantifierElimination(
premises: PredicateFormula[],
conclusion: PredicateFormula,
steps: Array<{ statement: string; rule: string; justification: string; }>
): boolean {
// Look for simple quantifier patterns
for (let i = 0; i < premises.length; i++) {
const premise = premises[i];
// Universal to Existential: ∀x P(x) → ∃x P(x)
if (
premise.type === 'quantified' &&
premise.quantifier === 'forall' &&
conclusion.type === 'quantified' &&
conclusion.quantifier === 'exists'
) {
if (formulaEquals(premise.formula, conclusion.formula)) {
steps.push({
statement: this.formatFormula(conclusion),
rule: 'Existential Introduction',
justification: `From premise ${i + 1}: if true for all, then exists`
});
return true;
}
}
}
return false;
}
}
