import { PredicateArgument, LogicalAnalysis, PredicateFormula } from '../types.js';
import { PredicateProofGenerator } from '../proof/predicateProof.js';
/**
* Validator for predicate logic arguments
*/
export class PredicateValidator {
private proofGenerator: PredicateProofGenerator;
constructor() {
this.proofGenerator = new PredicateProofGenerator();
}
/**
* Validate a predicate logic argument
* @param argument The argument to validate
* @returns Analysis with validity and explanation
*/
validate(argument: PredicateArgument): LogicalAnalysis {
try {
// Generate a proof
const solution = this.proofGenerator.generateProof(argument);
// Check if proof was successful
const lastStep = solution.steps[solution.steps.length - 1];
const isValid = lastStep &&
lastStep.rule !== 'Proof Not Found' &&
lastStep.rule !== 'Predicate Proof System';
if (isValid) {
return {
isValid: true,
fallacies: [],
explanation: 'The argument is VALID. A proof was constructed using first-order logic inference rules.',
counterexample: undefined
};
} else {
return {
isValid: false,
fallacies: [],
explanation: 'The argument could not be proven valid using the available inference rules. This does not necessarily mean it is invalid, as predicate logic validity is undecidable in general.',
counterexample: 'No counterexample generated (predicate logic validity is undecidable)'
};
}
} catch (error) {
return {
isValid: false,
fallacies: [],
explanation: `Error during validation: ${error instanceof Error ? error.message : 'Unknown error'}`,
counterexample: undefined
};
}
}
/**
* Validate a single formula (check if it's well-formed)
* @param formula The formula to validate
* @returns Analysis of the formula
*/
validateFormula(formula: PredicateFormula): LogicalAnalysis {
try {
// Check if formula is well-formed
this.checkWellFormed(formula);
return {
isValid: true,
fallacies: [],
explanation: 'The formula is well-formed.',
counterexample: undefined
};
} catch (error) {
return {
isValid: false,
fallacies: [{
name: 'Malformed Formula',
description: error instanceof Error ? error.message : 'Unknown error',
location: 'Formula'
}],
explanation: 'The formula is not well-formed.',
counterexample: undefined
};
}
}
/**
* Check if a formula is well-formed
* @param formula The formula to check
* @throws Error if formula is malformed
*/
private checkWellFormed(formula: PredicateFormula): void {
switch (formula.type) {
case 'variable':
case 'constant':
// Always well-formed
break;
case 'function':
// Check all arguments are well-formed
for (const arg of formula.args) {
this.checkWellFormed(arg);
}
break;
case 'predicate':
// Check all arguments are well-formed
for (const arg of formula.args) {
this.checkWellFormed(arg);
}
break;
case 'unary':
// Check operand is well-formed
this.checkWellFormed(formula.operand);
break;
case 'binary':
// Check both sides are well-formed
this.checkWellFormed(formula.left);
this.checkWellFormed(formula.right);
break;
case 'quantified':
// Check body is well-formed
this.checkWellFormed(formula.formula);
// Check variable is valid
if (!/^[a-z]$/.test(formula.variable)) {
throw new Error(`Invalid variable name: ${formula.variable}`);
}
break;
default:
throw new Error(`Unknown formula type: ${(formula as any).type}`);
}
}
}
