import { PredicateLogic } from './predicate.js';
import { PredicateArgument, PredicateFormula } from '../types.js';
describe('PredicateLogic - Inference Rules', () => {
let predicateLogic: PredicateLogic;
beforeEach(() => {
predicateLogic = new PredicateLogic();
});
describe('Universal Instantiation (UI)', () => {
it('should validate ∀x P(x), therefore P(a)', () => {
const input = '∀x P(x), therefore P(a)';
const result = predicateLogic.process('validate', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.analysis?.isValid).toBe(true);
expect(result.details.analysis?.explanation).toContain('VALID');
});
it('should generate proof with UI rule for ∀x P(x) ⊢ P(a)', () => {
const input = '∀x P(x), therefore P(a)';
const result = predicateLogic.process('solve', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.solution?.steps).toBeDefined();
const steps = result.details.solution!.steps;
expect(steps.some(step => step.rule.includes('Universal Instantiation'))).toBe(true);
});
it('should handle ∀x P(x), therefore P(socrates)', () => {
const input = '∀x P(x), therefore P(socrates)';
const result = predicateLogic.process('validate', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.analysis?.isValid).toBe(true);
});
});
describe('Existential Generalization (EG)', () => {
it('should validate P(a), therefore ∃x P(x)', () => {
const input = 'P(a), therefore ∃x P(x)';
const result = predicateLogic.process('validate', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.analysis?.isValid).toBe(true);
});
it('should generate proof with EG rule for P(a) ⊢ ∃x P(x)', () => {
const input = 'P(a), therefore ∃x P(x)';
const result = predicateLogic.process('solve', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.solution?.steps).toBeDefined();
const steps = result.details.solution!.steps;
expect(steps.some(step => step.rule.includes('Existential Generalization'))).toBe(true);
});
it('should handle P(socrates), therefore ∃x P(x)', () => {
const input = 'P(socrates), therefore ∃x P(x)';
const result = predicateLogic.process('validate', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.analysis?.isValid).toBe(true);
});
});
describe('Modus Ponens with Universal Instantiation', () => {
it('should validate ∀x (P(x) → Q(x)), P(a), therefore Q(a)', () => {
const input = '∀x (P(x) implies Q(x)), P(a), therefore Q(a)';
const result = predicateLogic.process('validate', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.analysis?.isValid).toBe(true);
});
it('should generate proof with UI and MP rules', () => {
const input = '∀x (P(x) implies Q(x)), P(a), therefore Q(a)';
const result = predicateLogic.process('solve', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.solution?.steps).toBeDefined();
const steps = result.details.solution!.steps;
expect(steps.some(step => step.rule.includes('Universal Instantiation'))).toBe(true);
expect(steps.some(step => step.rule.includes('Modus Ponens'))).toBe(true);
});
it('should handle classic syllogism: ∀x (Human(x) → Mortal(x)), Human(socrates), therefore Mortal(socrates)', () => {
const input = '∀x (Human(x) implies Mortal(x)), Human(socrates), therefore Mortal(socrates)';
const result = predicateLogic.process('validate', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.analysis?.isValid).toBe(true);
});
});
describe('Invalid Arguments', () => {
it('should reject ∃x P(x), therefore P(a) as invalid', () => {
const input = '∃x P(x), therefore P(a)';
const result = predicateLogic.process('validate', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.analysis?.isValid).toBe(false);
expect(result.details.analysis?.explanation).toContain('could not be proven valid');
});
it('should reject P(a), therefore ∀x P(x) as invalid', () => {
const input = 'P(a), therefore ∀x P(x)';
const result = predicateLogic.process('validate', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.analysis?.isValid).toBe(false);
});
it('should reject invalid modus ponens: P(a), ∀x (Q(x) → R(x)), therefore R(a)', () => {
const input = 'P(a), ∀x (Q(x) implies R(x)), therefore R(a)';
const result = predicateLogic.process('validate', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.analysis?.isValid).toBe(false);
});
});
describe('Parser Tests', () => {
it('should parse quantified formulas', () => {
const input = '∀x P(x)';
const result = predicateLogic.process('formalize', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.formalizedInput).toBeDefined();
});
it('should parse predicates with arguments', () => {
const input = 'Human(socrates)';
const result = predicateLogic.process('formalize', input, 'symbolic');
expect(result.status).toBe('success');
});
it('should parse complex formulas', () => {
const input = '∀x (Human(x) implies Mortal(x))';
const result = predicateLogic.process('formalize', input, 'symbolic');
expect(result.status).toBe('success');
});
it('should parse arguments with multiple premises', () => {
const input = '∀x (P(x) implies Q(x)), P(a), Q(a) implies R(a), therefore R(a)';
const result = predicateLogic.process('formalize', input, 'symbolic');
expect(result.status).toBe('success');
});
});
describe('Existential Introduction', () => {
it('should validate ∀x P(x), therefore ∃x P(x)', () => {
const input = '∀x P(x), therefore ∃x P(x)';
const result = predicateLogic.process('validate', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.analysis?.isValid).toBe(true);
});
});
describe('Direct Match', () => {
it('should recognize when conclusion is already a premise', () => {
const input = 'P(a), Q(a), therefore P(a)';
const result = predicateLogic.process('validate', input, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.analysis?.isValid).toBe(true);
});
});
describe('Complex Arguments', () => {
it.skip('should handle nested quantifiers', () => {
// TODO: Implement support for nested quantifiers and multi-arg predicates
const input = '∀x ∀y P(x,y), therefore P(a,b)';
const result = predicateLogic.process('validate', input, 'symbolic');
expect(result.status).toBe('success');
// This may not be directly provable with current rules, but should not error
});
it('should handle multiple predicates', () => {
const input = '∀x (P(x) and Q(x)), therefore P(a) and Q(a)';
const result = predicateLogic.process('validate', input, 'symbolic');
expect(result.status).toBe('success');
// May not be provable without additional rules
});
});
});
