import { LogicManager } from './logicManager.js';
import { LogicalSystem } from './types.js';
import { Loggers } from './utils/logger.js';
const logger = Loggers.server;
export interface Contradiction {
statement1: string;
statement2: string;
reason: string;
severity: 'direct' | 'logical' | 'contextual';
}
export interface ContradictionReport {
hasContradictions: boolean;
contradictions: Contradiction[];
consistentSubsets?: string[][];
recommendations?: string[];
}
export class ContradictionDetector {
private logicManager: LogicManager;
constructor(logicManager: LogicManager) {
this.logicManager = logicManager;
}
/**
* Detect contradictions in a set of statements
* @param statements Array of logical statements
* @param system Logical system to use for checking
* @returns Contradiction report
*/
async detectContradictions(
statements: string[],
system: LogicalSystem = 'propositional'
): Promise<ContradictionReport> {
logger.info(`Detecting contradictions in ${statements.length} statements using ${system}`);
const contradictions: Contradiction[] = [];
// Check for direct contradictions (A and ¬A)
this.checkDirectContradictions(statements, contradictions);
// Check for logical contradictions (pairwise entailment of negation)
if (system === 'propositional' || system === 'predicate' || system === 'modal') {
await this.checkLogicalContradictions(statements, system, contradictions);
}
// Check for contextual contradictions
this.checkContextualContradictions(statements, contradictions);
// Find consistent subsets if contradictions exist
let consistentSubsets: string[][] | undefined;
let recommendations: string[] | undefined;
if (contradictions.length > 0) {
consistentSubsets = this.findMaximalConsistentSubsets(statements, contradictions);
recommendations = this.generateRecommendations(contradictions, statements);
}
return {
hasContradictions: contradictions.length > 0,
contradictions,
consistentSubsets,
recommendations
};
}
/**
* Check for direct contradictions (syntactic)
*/
private checkDirectContradictions(statements: string[], contradictions: Contradiction[]): void {
for (let i = 0; i < statements.length; i++) {
for (let j = i + 1; j < statements.length; j++) {
const s1 = statements[i].toLowerCase().trim();
const s2 = statements[j].toLowerCase().trim();
// Check for explicit negation patterns
if (this.isDirectNegation(s1, s2)) {
contradictions.push({
statement1: statements[i],
statement2: statements[j],
reason: 'Direct contradiction: one statement is the negation of the other',
severity: 'direct'
});
}
}
}
}
/**
* Check if one statement is the direct negation of another
*/
private isDirectNegation(s1: string, s2: string): boolean {
// Remove common negation patterns
const negPatterns = ['not ', '¬', 'it is false that ', 'it is not true that '];
for (const pattern of negPatterns) {
if (s1.startsWith(pattern)) {
const core1 = s1.substring(pattern.length).trim();
if (core1 === s2) return true;
}
if (s2.startsWith(pattern)) {
const core2 = s2.substring(pattern.length).trim();
if (core2 === s1) return true;
}
}
return false;
}
/**
* Check for logical contradictions using the logic system
*/
private async checkLogicalContradictions(
statements: string[],
system: LogicalSystem,
contradictions: Contradiction[]
): Promise<void> {
// For each pair, check if they jointly entail a contradiction
for (let i = 0; i < statements.length; i++) {
for (let j = i + 1; j < statements.length; j++) {
// Try to validate "s1 AND s2 AND ¬(s1 AND s2)"
const combined = `(${statements[i]}) and (${statements[j]})`;
try {
const result = await this.logicManager.process(
system,
'validate',
`${combined} therefore false`,
'natural'
);
// If the conjunction entails false, we have a contradiction
if (result.status === 'success' && result.details?.analysis?.isValid) {
contradictions.push({
statement1: statements[i],
statement2: statements[j],
reason: 'Logical contradiction: these statements cannot both be true',
severity: 'logical'
});
}
} catch (error) {
// Skip if validation fails
logger.debug(`Could not check contradiction between statements ${i} and ${j}`);
}
}
}
}
/**
* Check for contextual contradictions (domain-specific)
*/
private checkContextualContradictions(statements: string[], contradictions: Contradiction[]): void {
// Check for contradictory quantifiers
for (let i = 0; i < statements.length; i++) {
for (let j = i + 1; j < statements.length; j++) {
const s1 = statements[i].toLowerCase();
const s2 = statements[j].toLowerCase();
// Enhanced patterns to be more flexible with extra words
// Pattern: "All X ... Y" vs "Some X ... not ... Y"
const allPattern = /all (\w+)/;
const someNotPattern = /some (\w+).*?\b(not|don't|doesn't|didn't|won't|wouldn't|can't|cannot|couldn't|shouldn't|mustn't|haven't|hasn't|hadn't|isn't|aren't|wasn't|weren't|do not|does not|did not|will not|would not|can not|could not|should not|must not|have not|has not|had not|is not|are not|was not|were not)\b/;
const notAllPattern = /not all (\w+)/;
const allMatch = s1.match(allPattern);
const someNotMatch = s2.match(someNotPattern);
const notAllMatch = s2.match(notAllPattern);
// Check: "All X..." vs "Some X...not..."
if (allMatch && someNotMatch && allMatch[1] === someNotMatch[1]) {
contradictions.push({
statement1: statements[i],
statement2: statements[j],
reason: 'Contextual contradiction: universal claim conflicts with existential counterexample',
severity: 'contextual'
});
continue; // Skip checking reverse for this pair
}
// Check: "All X..." vs "Not all X..."
if (allMatch && notAllMatch && allMatch[1] === notAllMatch[1]) {
contradictions.push({
statement1: statements[i],
statement2: statements[j],
reason: 'Contextual contradiction: universal claim directly negated',
severity: 'contextual'
});
continue; // Skip checking reverse for this pair
}
// Also check the reverse direction
const allMatch2 = s2.match(allPattern);
const someNotMatch2 = s1.match(someNotPattern);
const notAllMatch2 = s1.match(notAllPattern);
// Check: "Some X...not..." vs "All X..."
if (allMatch2 && someNotMatch2 && allMatch2[1] === someNotMatch2[1]) {
contradictions.push({
statement1: statements[i],
statement2: statements[j],
reason: 'Contextual contradiction: universal claim conflicts with existential counterexample',
severity: 'contextual'
});
continue;
}
// Check: "Not all X..." vs "All X..."
if (allMatch2 && notAllMatch2 && allMatch2[1] === notAllMatch2[1]) {
contradictions.push({
statement1: statements[i],
statement2: statements[j],
reason: 'Contextual contradiction: universal claim directly negated',
severity: 'contextual'
});
}
}
}
}
/**
* Find maximal consistent subsets
*/
private findMaximalConsistentSubsets(
statements: string[],
contradictions: Contradiction[]
): string[][] {
const subsets: string[][] = [];
// Build contradiction graph
const contradictsWith = new Map<number, Set<number>>();
for (let i = 0; i < statements.length; i++) {
contradictsWith.set(i, new Set());
}
for (const c of contradictions) {
const i1 = statements.indexOf(c.statement1);
const i2 = statements.indexOf(c.statement2);
if (i1 >= 0 && i2 >= 0) {
contradictsWith.get(i1)!.add(i2);
contradictsWith.get(i2)!.add(i1);
}
}
// Find maximal consistent subsets (greedy approach)
const used = new Set<number>();
while (used.size < statements.length) {
const subset: number[] = [];
for (let i = 0; i < statements.length; i++) {
if (used.has(i)) continue;
// Check if i is consistent with current subset
const conflicts = Array.from(contradictsWith.get(i)!);
if (!conflicts.some(c => subset.includes(c))) {
subset.push(i);
}
}
if (subset.length > 0) {
subsets.push(subset.map(i => statements[i]));
subset.forEach(i => used.add(i));
} else {
break;
}
}
return subsets;
}
/**
* Generate recommendations for resolving contradictions
*/
private generateRecommendations(contradictions: Contradiction[], statements: string[]): string[] {
const recommendations: string[] = [];
if (contradictions.length === 0) {
return ['No contradictions detected. The set of statements appears consistent.'];
}
recommendations.push(`Found ${contradictions.length} contradiction(s) in ${statements.length} statements.`);
// Count by severity
const direct = contradictions.filter(c => c.severity === 'direct').length;
const logical = contradictions.filter(c => c.severity === 'logical').length;
const contextual = contradictions.filter(c => c.severity === 'contextual').length;
if (direct > 0) {
recommendations.push(
`${direct} direct contradiction(s): Remove one statement from each contradictory pair.`
);
}
if (logical > 0) {
recommendations.push(
`${logical} logical contradiction(s): These statements cannot all be true simultaneously.`
);
}
if (contextual > 0) {
recommendations.push(
`${contextual} contextual contradiction(s): Check domain assumptions and quantifier scope.`
);
}
recommendations.push(
'Consider revising or removing contradictory statements to maintain consistency.'
);
return recommendations;
}
}
