import {
LogicalSystem,
Operation,
InputFormat,
LogicResult,
PredicateFormula,
PredicateArgument
} from '../types.js';
// Import parser
import { PredicateParser } from '../parsers/predicateParser.js';
// Import validator
import { PredicateValidator } from '../validators/predicateValidator.js';
// Import visualization support
import { PredicateVisualizer } from './visualization/predicate/predicateVisualizer.js';
// Import proof generation support
import { PredicateProofGenerator } from '../proof/predicateProof.js';
/**
* Predicate Logic System
* Handles first-order logic with quantifiers, variables, and predicates
*/
export class PredicateLogic {
private parser: PredicateParser;
private validator: PredicateValidator;
private visualizer: PredicateVisualizer;
private proofGenerator: PredicateProofGenerator;
constructor() {
this.parser = new PredicateParser();
this.validator = new PredicateValidator();
this.visualizer = new PredicateVisualizer();
this.proofGenerator = new PredicateProofGenerator();
}
/**
* Main entry point for predicate logic operations
* @param operation The operation to perform
* @param input Input text or structured data
* @param format Input format
* @returns Operation result
*/
process(
operation: Operation,
input: string | PredicateFormula | PredicateArgument,
format: InputFormat = 'natural'
): LogicResult {
try {
// Parse the input if it's a string
const parsedInput = typeof input === 'string'
? this.parseInput(input, format)
: input;
// Perform the requested operation
switch (operation) {
case 'validate':
return this.analyzeValidity(parsedInput);
case 'formalize':
return this.formatPredicate(parsedInput);
case 'visualize':
return this.generateVisualization(parsedInput);
case 'solve':
return this.generateProof(parsedInput);
default:
throw new Error(`Unsupported operation: ${operation}`);
}
} catch (error) {
// Return an error result
return {
status: 'error',
message: error instanceof Error ? error.message : 'Unknown error',
details: {
system: 'predicate'
}
};
}
}
/**
* Parse input text into structured predicate logic
* @param input Input text
* @param format Input format
* @returns Parsed predicate formula or argument
*/
private parseInput(
input: string,
format: InputFormat
): PredicateFormula | PredicateArgument {
// Use the parser to parse the input
return this.parser.parse(input);
}
/**
* Analyze validity of a predicate formula or argument
* @param input The formula or argument to analyze
* @returns Analysis result
*/
private analyzeValidity(
input: PredicateFormula | PredicateArgument
): LogicResult {
const isArgument = 'premises' in input;
if (isArgument) {
// Validate the argument using the validator
const analysis = this.validator.validate(input as PredicateArgument);
return {
status: 'success',
message: analysis.isValid ? 'The argument is VALID.' : 'The argument could not be proven valid.',
details: {
system: 'predicate',
analysis
}
};
} else {
// Validate the formula
const analysis = this.validator.validateFormula(input as PredicateFormula);
return {
status: 'success',
message: 'Formula validation completed.',
details: {
system: 'predicate',
analysis
}
};
}
}
/**
* Format a predicate formula or argument
* @param input The formula or argument to format
* @returns Formatting result
*/
private formatPredicate(
input: PredicateFormula | PredicateArgument
): LogicResult {
// Basic formatting logic - placeholder
const formatted = JSON.stringify(input, null, 2);
return {
status: 'success',
message: 'Input formatted successfully.',
details: {
system: 'predicate',
formalizedInput: formatted
}
};
}
/**
* Generate a visualization for a predicate formula or argument
* @param input The formula or argument to visualize
* @returns Visualization result
*/
private generateVisualization(
input: PredicateFormula | PredicateArgument
): LogicResult {
// Use the visualizer to generate different types of visualizations
const parseTree = this.visualizer.visualize(input, 'parseTree', 'svg');
// Return the result
return {
status: 'success',
message: 'Visualization generated successfully.',
details: {
system: 'predicate',
visualization: parseTree
}
};
}
/**
* Generate a proof for a predicate formula or argument
* @param input The formula or argument to prove
* @returns Proof result
*/
private generateProof(
input: PredicateFormula | PredicateArgument
): LogicResult {
// Check if input is an argument (has premises and conclusion)
if ('premises' in input) {
// Use the proof generator for arguments
const argument = input as PredicateArgument;
const solution = this.proofGenerator.generateProof(argument);
return {
status: 'success',
message: 'Proof generated successfully.',
details: {
system: 'predicate',
solution
}
};
} else {
// For standalone formulas, provide basic analysis
return {
status: 'success',
message: 'Formula analyzed (proof requires premises and conclusion).',
details: {
system: 'predicate',
solution: {
steps: [
{
index: 1,
statement: 'Formula provided without premises.',
rule: 'Analysis',
justification: 'A full proof requires both premises and a conclusion.'
}
],
conclusion: 'Please provide premises and a conclusion to generate a proof.'
}
}
};
}
}
}