/**
* Default Logic Solver
* Translates default logic to ASP and computes extensions
*/
import { DefaultTheory, DefaultRule, DefaultExtension, DefaultReasoningResult } from '../../types.js';
import { ClingoSolver } from './clingoSolver.js';
import { Loggers } from '../../utils/logger.js';
const logger = Loggers.manager;
export class DefaultLogicSolver {
private solver: ClingoSolver;
constructor() {
this.solver = new ClingoSolver();
}
/**
* Solve default theory
*/
async solve(theory: DefaultTheory, query?: string, mode?: 'credulous' | 'skeptical'): Promise<DefaultReasoningResult> {
// Translate default theory to ASP
const aspProgram = this.translateToASP(theory);
// Solve with Clingo
const solution = await this.solver.solve(aspProgram, { maxModels: 0 });
// Convert answer sets to extensions
const extensions = this.convertToExtensions(solution.answerSets, theory);
// Answer query if provided
let queryResult;
if (query) {
queryResult = this.answerQuery(extensions, query, mode);
}
return {
extensions,
query,
queryResult
};
}
/**
* Translate default theory to ASP (dl2asp algorithm)
*/
private translateToASP(theory: DefaultTheory): string {
let program = '';
// Add facts
for (const fact of theory.facts) {
program += `${fact.toLowerCase().replace(/[^a-z0-9_(),]/g, '_')}.\n`;
}
program += '\n';
// Translate each default rule
for (let i = 0; i < theory.rules.length; i++) {
const rule = theory.rules[i];
const ruleId = `r${i}`;
program += this.translateDefaultRule(rule, ruleId);
}
return program;
}
/**
* Translate single default rule using dl2asp
* Default: α : β / γ
* Translation:
* γ :- α, not blocked_r.
* {neg_β} :- α.
* blocked_r :- α, neg_β.
* :- β, neg_β.
*/
private translateDefaultRule(rule: DefaultRule, ruleId: string): string {
let asp = '';
const prerequisite = this.cleanFormula(rule.prerequisite);
const conclusion = this.cleanFormula(rule.conclusion);
// Main rule: conclusion if prerequisite and not blocked
asp += `${conclusion} :- ${prerequisite}, not blocked_${ruleId}.\n`;
// For each justification
for (let j = 0; j < rule.justifications.length; j++) {
const justification = this.cleanFormula(rule.justifications[j]);
const negJust = `neg_${this.atomName(justification)}_${ruleId}`;
// Choice: justification can be negated
asp += `{${negJust}} :- ${prerequisite}.\n`;
// Blocking: if negation is chosen, block the rule
asp += `blocked_${ruleId} :- ${prerequisite}, ${negJust}.\n`;
// Consistency: justification and its negation can't both hold
asp += `:- ${justification}, ${negJust}.\n`;
}
asp += '\n';
return asp;
}
/**
* Clean formula for ASP
*/
private cleanFormula(formula: string): string {
return formula.toLowerCase()
.replace(/[^a-z0-9_(),\s]/g, '')
.replace(/\s+/g, '_');
}
/**
* Extract atom name from formula
*/
private atomName(formula: string): string {
return formula.toLowerCase()
.replace(/[^a-z0-9]/g, '_')
.replace(/^_+|_+$/g, '');
}
/**
* Convert answer sets to default extensions
*/
private convertToExtensions(answerSets: any[], theory: DefaultTheory): DefaultExtension[] {
const extensions: DefaultExtension[] = [];
for (let i = 0; i < answerSets.length; i++) {
const answerSet = answerSets[i];
// Filter out auxiliary atoms
const facts = answerSet.atoms
.map((atom: any) => {
const atomStr = `${atom.predicate}(${atom.terms.join(',')})`;
return atomStr;
})
.filter((fact: string) =>
!fact.startsWith('blocked_') &&
!fact.startsWith('neg_')
);
// Determine which defaults were applied
const appliedDefaults = theory.rules
.map((rule, idx) => {
const blocked = answerSet.atoms.some((atom: any) =>
atom.predicate === `blocked_r${idx}`
);
return blocked ? null : rule.id || rule.conclusion;
})
.filter((id: any): id is string => id !== null);
extensions.push({
id: `ext${i + 1}`,
facts,
appliedDefaults,
explanation: `Extension ${i + 1} with ${facts.length} facts`
});
}
return extensions;
}
/**
* Answer query against extensions
*/
private answerQuery(
extensions: DefaultExtension[],
query: string,
mode: 'credulous' | 'skeptical' = 'skeptical'
): any {
const cleanQuery = this.cleanFormula(query);
const supportingExtensions: number[] = [];
for (let i = 0; i < extensions.length; i++) {
const ext = extensions[i];
if (ext.facts.some(fact => fact.includes(cleanQuery))) {
supportingExtensions.push(i);
}
}
const credulouslyTrue = supportingExtensions.length > 0;
const skepticallyTrue = supportingExtensions.length === extensions.length;
return {
credulouslyTrue,
skepticallyTrue,
supportingExtensions
};
}
}
