import { ModalFormula, ModalArgument, ModalSystem, KripkeFrame, Countermodel } from '../types.js';
import { PropositionalValidator } from './propositionalValidator.js';
import { Loggers } from '../utils/logger.js';
const logger = Loggers.modal;
export class ModalValidator {
private propValidator: PropositionalValidator;
private systemConstraintCache = new Map<string, boolean>();
private lastCountermodel: Countermodel | null = null;
constructor() {
this.propValidator = new PropositionalValidator();
}
/**
* Get the last countermodel found during validation
*/
getLastCountermodel(): Countermodel | null {
return this.lastCountermodel;
}
/**
* Calculate the modal depth of a formula (max nesting of modal operators)
*/
private modalDepth(formula: ModalFormula): number {
if (!('type' in formula) || formula.type !== 'modal') {
// Check for nested formulas in propositional structure
if ('type' in formula) {
if (formula.type === 'unary' && 'operand' in formula) {
return this.modalDepth(formula.operand as ModalFormula);
}
if (formula.type === 'binary' && 'left' in formula && 'right' in formula) {
return Math.max(
this.modalDepth(formula.left as ModalFormula),
this.modalDepth(formula.right as ModalFormula)
);
}
}
return 0;
}
return 1 + this.modalDepth(formula.operand);
}
/**
* Count subformulas for model bound calculation
*/
private countSubformulas(formula: ModalFormula): number {
if (!('type' in formula)) return 1;
switch (formula.type) {
case 'variable':
return 1;
case 'modal':
case 'unary':
return 1 + this.countSubformulas((formula as any).operand);
case 'binary':
const f = formula as any;
return 1 + this.countSubformulas(f.left) + this.countSubformulas(f.right);
default:
return 1;
}
}
/**
* Get bound on model size based on formula and system
* Uses finite model property for modal logics
*/
private getModelBound(formula: ModalFormula, system: ModalSystem): number {
const depth = this.modalDepth(formula);
const subformulas = this.countSubformulas(formula);
// For most modal systems, we can bound model size
// K, T, D, B, K4, KB, S4, S5 all have finite model property
// Bound: 2^depth for depth-based approach
// Or: subformulas for subformula-based approach
const depthBound = Math.min(4, Math.pow(2, depth));
const subformulaBound = Math.min(4, Math.ceil(Math.log2(subformulas + 1)) + 1);
// Use the smaller bound, but at least 2 worlds
return Math.max(2, Math.min(depthBound, subformulaBound));
}
/**
* Check if a modal formula is valid in all Kripke frames for the given system
* Uses bounded model checking for performance
*/
isValid(formula: ModalFormula, system: ModalSystem = 'K'): boolean {
logger.debug(`Checking validity of modal formula in system ${system}`);
this.lastCountermodel = null;
const modelBound = this.getModelBound(formula, system);
logger.debug(`Using model bound: ${modelBound} worlds`);
// Generate test frames based on the modal system with bounded size
const testFrames = this.generateTestFramesBounded(formula, system, modelBound);
// Check if formula is true in all worlds of all frames
for (const frame of testFrames) {
for (const world of frame.worlds) {
if (!this.evaluateInWorld(formula, frame, world)) {
// Store countermodel
this.lastCountermodel = this.extractCountermodel(formula, frame, world);
return false;
}
}
}
return true;
}
/**
* Check if a modal argument is valid
*/
isArgumentValid(argument: ModalArgument): boolean {
logger.debug(`Validating modal argument in system ${argument.system}`);
this.lastCountermodel = null;
// An argument is valid if there's no frame where all premises are true but conclusion is false
// Collect all atomic formulas from premises and conclusion
const allFormulas = [...argument.premises, argument.conclusion];
const atoms = new Set<string>();
for (const formula of allFormulas) {
this.extractAtoms(formula).forEach(a => atoms.add(a));
}
// Calculate bound based on all formulas
const maxDepth = Math.max(...allFormulas.map(f => this.modalDepth(f)));
const maxSubformulas = Math.max(...allFormulas.map(f => this.countSubformulas(f)));
const modelBound = Math.max(2, Math.min(4, Math.pow(2, maxDepth)));
logger.debug(`Using model bound: ${modelBound} worlds for argument validation`);
// Generate test frames based on the collected atoms with bounded size
const testFrames = this.generateTestFramesFromAtomsBounded(atoms, argument.system, modelBound);
for (const frame of testFrames) {
for (const world of frame.worlds) {
const premisesTrue = argument.premises.every((p: ModalFormula) =>
this.evaluateInWorld(p, frame, world)
);
const conclusionTrue = this.evaluateInWorld(argument.conclusion, frame, world);
if (premisesTrue && !conclusionTrue) {
logger.debug(`Counterexample found in world ${world}`);
// Store countermodel for argument
this.lastCountermodel = this.extractArgumentCountermodel(argument, frame, world);
return false;
}
}
}
return true;
}
/**
* Extract countermodel for a formula
*/
private extractCountermodel(formula: ModalFormula, frame: KripkeFrame, world: string): Countermodel {
return {
frame,
failingWorld: world,
explanation: `Formula fails at world ${world} in this Kripke frame`,
premiseEvaluations: {},
conclusionEvaluation: this.evaluateInWorld(formula, frame, world)
};
}
/**
* Extract countermodel for an argument
*/
private extractArgumentCountermodel(
argument: ModalArgument,
frame: KripkeFrame,
world: string
): Countermodel {
const premiseEvals: { [premise: string]: boolean } = {};
argument.premises.forEach((premise, idx) => {
premiseEvals[`P${idx + 1}`] = this.evaluateInWorld(premise, frame, world);
});
return {
frame,
failingWorld: world,
explanation: `All premises are true but conclusion is false at world ${world}`,
premiseEvaluations: premiseEvals,
conclusionEvaluation: this.evaluateInWorld(argument.conclusion, frame, world)
};
}
/**
* Evaluate a modal formula at a specific world in a Kripke frame
*/
private evaluateInWorld(formula: ModalFormula, frame: KripkeFrame, world: string): boolean {
// Handle modal operators
if ('type' in formula && formula.type === 'modal') {
const accessibleWorlds = this.getAccessibleWorlds(frame, world);
if (formula.operator === '□' || formula.operator === 'necessary') {
// □φ is true at w iff φ is true at all worlds accessible from w
return accessibleWorlds.every((w: string) => this.evaluateInWorld(formula.operand, frame, w));
} else {
// ◇φ is true at w iff φ is true at some world accessible from w
return accessibleWorlds.some((w: string) => this.evaluateInWorld(formula.operand, frame, w));
}
}
// Handle propositional formulas (pass frame and world for nested modal formulas)
return this.evaluatePropositional(formula, frame.valuation[world] || {}, frame, world);
}
/**
* Get worlds accessible from a given world
*/
private getAccessibleWorlds(frame: KripkeFrame, world: string): string[] {
return frame.accessibility
.filter(([from, _]: [string, string]) => from === world)
.map(([_, to]: [string, string]) => to);
}
/**
* Evaluate propositional formulas using the world's valuation
* Note: This is called from evaluateInWorld and should not be used directly for modal formulas
*/
private evaluatePropositional(formula: any, valuation: { [prop: string]: boolean }, frame?: KripkeFrame, world?: string): boolean {
if (formula.type === 'variable') {
return valuation[formula.name] || false;
}
// If we encounter a modal formula in propositional context, we need frame/world
if (formula.type === 'modal') {
if (!frame || !world) {
throw new Error('Modal formula encountered without frame/world context');
}
return this.evaluateInWorld(formula, frame, world);
}
switch (formula.type) {
case 'negation':
return !this.evaluatePropositional(formula.operand, valuation, frame, world);
case 'unary':
return !this.evaluatePropositional(formula.operand, valuation, frame, world);
case 'binary':
if (formula.operator === 'and' || formula.operator === '∧') {
return this.evaluatePropositional(formula.left, valuation, frame, world) &&
this.evaluatePropositional(formula.right, valuation, frame, world);
} else if (formula.operator === 'or' || formula.operator === '∨') {
return this.evaluatePropositional(formula.left, valuation, frame, world) ||
this.evaluatePropositional(formula.right, valuation, frame, world);
} else if (formula.operator === 'implies' || formula.operator === '→') {
const antTrue = this.evaluatePropositional(formula.left, valuation, frame, world);
const consTrue = this.evaluatePropositional(formula.right, valuation, frame, world);
return !antTrue || consTrue;
} else if (formula.operator === 'iff' || formula.operator === '↔') {
const leftTrue = this.evaluatePropositional(formula.left, valuation, frame, world);
const rightTrue = this.evaluatePropositional(formula.right, valuation, frame, world);
return leftTrue === rightTrue;
}
default:
return false;
}
}
/**
* Check if formula is valid in a specific frame
*/
private isValidInFrame(formula: ModalFormula, frame: KripkeFrame, world: string): boolean {
return this.evaluateInWorld(formula, frame, world);
}
/**
* Generate test frames with bounded model checking
*/
private generateTestFramesBounded(
formula: ModalFormula,
system: ModalSystem,
maxWorlds: number
): KripkeFrame[] {
const atoms = this.extractAtoms(formula);
return this.generateTestFramesFromAtomsBounded(atoms, system, maxWorlds);
}
/**
* Generate test frames from a set of atoms with bounded size
*/
private generateTestFramesFromAtomsBounded(
atoms: Set<string>,
system: ModalSystem,
maxWorlds: number
): KripkeFrame[] {
const frames: KripkeFrame[] = [];
const atomArray = Array.from(atoms);
// Limit total frames to prevent explosion
const MAX_FRAMES = 100;
let frameCount = 0;
// Generate frames with 1 to maxWorlds
for (let numWorlds = 1; numWorlds <= maxWorlds && frameCount < MAX_FRAMES; numWorlds++) {
const worlds = Array.from({ length: numWorlds }, (_, i) => `w${i}`);
// Generate different accessibility relations based on the system
const accessibilityOptions = this.generateAccessibilityRelations(worlds, system);
// Limit accessibility options
const limitedAccessibility = accessibilityOptions.slice(0, Math.ceil(20 / numWorlds));
for (const accessibility of limitedAccessibility) {
if (frameCount >= MAX_FRAMES) break;
// Generate representative valuations (not all possible ones)
const valuations = this.generateRepresentativeValuations(worlds, atomArray);
for (const valuation of valuations) {
if (frameCount >= MAX_FRAMES) break;
frames.push({ worlds, accessibility, valuation });
frameCount++;
}
}
}
logger.debug(`Generated ${frames.length} test frames (bounded)`);
return frames;
}
/**
* Generate representative valuations instead of all possible ones
* This reduces from 2^(w*a) to a manageable set
*/
private generateRepresentativeValuations(
worlds: string[],
atoms: string[]
): { [world: string]: { [prop: string]: boolean } }[] {
const valuations: { [world: string]: { [prop: string]: boolean } }[] = [];
// Strategy: Generate key representative cases
// 1. All false
// 2. All true
// 3. Each atom true in different worlds (counterexamples for axioms)
// 4. Each atom false in different worlds (more counterexamples)
// 5. Some mixed combinations
const cases = [
// All false
() => {
const val: { [world: string]: { [prop: string]: boolean } } = {};
worlds.forEach(w => {
val[w] = {};
atoms.forEach(a => { val[w][a] = false; });
});
return val;
},
// All true
() => {
const val: { [world: string]: { [prop: string]: boolean } } = {};
worlds.forEach(w => {
val[w] = {};
atoms.forEach(a => { val[w][a] = true; });
});
return val;
},
// Each atom true in first world only
...atoms.map(targetAtom => () => {
const val: { [world: string]: { [prop: string]: boolean } } = {};
worlds.forEach((w, wi) => {
val[w] = {};
atoms.forEach(a => {
val[w][a] = a === targetAtom && wi === 0;
});
});
return val;
}),
// Each atom false in first world only (CRITICAL for T axiom counterexample)
...atoms.map(targetAtom => () => {
const val: { [world: string]: { [prop: string]: boolean } } = {};
worlds.forEach((w, wi) => {
val[w] = {};
atoms.forEach(a => {
val[w][a] = !(a === targetAtom && wi === 0);
});
});
return val;
}),
// Each atom false in last world only (CRITICAL for S4 axiom counterexample in T)
...atoms.map(targetAtom => () => {
const val: { [world: string]: { [prop: string]: boolean } } = {};
worlds.forEach((w, wi) => {
val[w] = {};
atoms.forEach(a => {
val[w][a] = !(a === targetAtom && wi === worlds.length - 1);
});
});
return val;
}),
// Each atom true in each world individually
...worlds.flatMap((targetWorld, twi) =>
atoms.map(targetAtom => () => {
const val: { [world: string]: { [prop: string]: boolean } } = {};
worlds.forEach((w, wi) => {
val[w] = {};
atoms.forEach(a => {
val[w][a] = a === targetAtom && wi === twi;
});
});
return val;
})
),
// Mixed cases
...Array.from({ length: Math.min(5, atoms.length) }, (_, i) => () => {
const val: { [world: string]: { [prop: string]: boolean } } = {};
worlds.forEach((w, wi) => {
val[w] = {};
atoms.forEach((a, ai) => {
// Create patterns based on indices
val[w][a] = ((wi + ai + i) % 2) === 0;
});
});
return val;
})
];
cases.forEach(caseGen => {
valuations.push(caseGen());
});
return valuations.slice(0, 40); // Increased limit for better coverage
}
/**
* Generate accessibility relations based on modal system properties
* Uses lazy subset generation for O(n) memory instead of O(2^n)
*/
private generateAccessibilityRelations(worlds: string[], system: ModalSystem): Array<[string, string]>[] {
const relations: Array<[string, string]>[] = [];
// Generate base relations (all possible world pairs)
const allPairs: Array<[string, string]> = [];
for (const w1 of worlds) {
for (const w2 of worlds) {
allPairs.push([w1, w2]);
}
}
// Lazily generate and filter subsets until we have enough valid relations
// Use more relations for systems that need them (like T, which needs counterexamples for S4)
const MAX_RELATIONS = worlds.length <= 2 ? 10 : 30;
const subsetGenerator = this.generateSubsetsLazy(allPairs);
for (const subset of subsetGenerator) {
// Check if this subset satisfies the system constraints
if (this.satisfiesSystemConstraints(subset, worlds, system)) {
relations.push(subset);
// Early termination: stop once we have enough relations
if (relations.length >= MAX_RELATIONS) {
break;
}
}
}
return relations;
}
/**
* Check if accessibility relation satisfies system constraints (with caching)
*/
private satisfiesSystemConstraints(
relation: Array<[string, string]>,
worlds: string[],
system: ModalSystem
): boolean {
// Create cache key
const key = `${system}:${worlds.join(',')}:${relation.map(r => r.join('-')).join(';')}`;
if (this.systemConstraintCache.has(key)) {
return this.systemConstraintCache.get(key)!;
}
const result = this.checkSystemConstraints(relation, worlds, system);
this.systemConstraintCache.set(key, result);
return result;
}
/**
* Actually check system constraints
*/
private checkSystemConstraints(
relation: Array<[string, string]>,
worlds: string[],
system: ModalSystem
): boolean {
// K: No special constraints
if (system === 'K') return true;
// Check reflexivity (T, B, S4, S5, KD45)
const needsReflexivity = ['T', 'B', 'S4', 'S5', 'KD45'].includes(system);
if (needsReflexivity) {
for (const w of worlds) {
if (!relation.some(([from, to]) => from === w && to === w)) {
return false;
}
}
}
// D, KD45: Serial (each world accesses at least one world)
if (system === 'D' || system === 'KD45') {
for (const w of worlds) {
if (!relation.some(([from, _]) => from === w)) {
return false;
}
}
}
// Check transitivity (K4, S4, S5, KD45)
const needsTransitivity = ['K4', 'S4', 'S5', 'KD45'].includes(system);
if (needsTransitivity) {
for (const [w1, w2] of relation) {
for (const [w2p, w3] of relation) {
if (w2 === w2p && !relation.some(([from, to]) => from === w1 && to === w3)) {
return false;
}
}
}
}
// Check symmetry (B, KB, S5, KD45)
const needsSymmetry = ['B', 'KB', 'S5', 'KD45'].includes(system);
if (needsSymmetry) {
for (const [w1, w2] of relation) {
if (!relation.some(([from, to]) => from === w2 && to === w1)) {
return false;
}
}
}
// Euclidean property for KD45 (alternative to transitivity + symmetry)
if (system === 'KD45') {
// If wRx and wRy, then xRy (Euclidean)
for (const [w, x] of relation) {
for (const [wp, y] of relation) {
if (w === wp && !relation.some(([from, to]) => from === x && to === y)) {
return false;
}
}
}
}
return true;
}
/**
* Lazily generate subsets of an array using a generator
* This yields subsets one at a time, allowing early termination
* Memory complexity: O(n) instead of O(2^n)
*
* @param arr - Array to generate subsets from
* @yields Each subset as an array
*/
private *generateSubsetsLazy<T>(arr: T[]): Generator<T[], void, undefined> {
const n = arr.length;
const totalSubsets = Math.pow(2, n);
// Iterate through all binary representations from 0 to 2^n - 1
for (let i = 0; i < totalSubsets; i++) {
const subset: T[] = [];
// Check each bit position to determine if element is included
for (let j = 0; j < n; j++) {
if ((i & (1 << j)) !== 0) {
subset.push(arr[j]);
}
}
yield subset;
}
}
/**
* Extract atomic propositions from a formula
*/
private extractAtoms(formula: ModalFormula): Set<string> {
const atoms = new Set<string>();
if ('type' in formula) {
switch (formula.type) {
case 'variable':
atoms.add(formula.name);
break;
case 'modal':
this.extractAtoms(formula.operand).forEach(a => atoms.add(a));
break;
case 'unary':
this.extractAtoms(formula.operand).forEach(a => atoms.add(a));
break;
case 'binary':
this.extractAtoms(formula.left).forEach(a => atoms.add(a));
this.extractAtoms(formula.right).forEach(a => atoms.add(a));
break;
}
}
return atoms;
}
}
