/**
* ASP (Answer Set Programming) Logic System
* Main system integrating all ASP components
*/
import {
LogicalSystem,
Operation,
InputFormat,
LogicResult,
ASPProgram,
ASPSolution,
DefaultTheory,
DefaultReasoningResult
} from '../types.js';
import { ASPParser } from '../parsers/aspParser.js';
import { ASPValidator } from './asp/aspValidator.js';
import { ASPFormatter } from './asp/aspFormatter.js';
import { ClingoSolver } from './asp/clingoSolver.js';
import { ASPOptimizer } from './asp/aspOptimizer.js';
import { DefaultLogicSolver } from './asp/defaultLogicSolver.js';
import { ASPVisualizer } from './visualization/asp/aspVisualizer.js';
import { ASPExplainer } from './asp/aspExplainer.js';
import { Loggers } from '../utils/logger.js';
const logger = Loggers.manager;
/**
* ASP Logic System
* Handles Answer Set Programming and default logic
*/
export class ASPLogic {
private parser: ASPParser;
private validator: ASPValidator;
private formatter: ASPFormatter;
private solver: ClingoSolver;
private optimizer: ASPOptimizer;
private defaultSolver: DefaultLogicSolver;
private visualizer: ASPVisualizer;
private explainer: ASPExplainer;
constructor() {
this.parser = new ASPParser();
this.validator = new ASPValidator();
this.formatter = new ASPFormatter();
this.solver = new ClingoSolver();
this.optimizer = new ASPOptimizer();
this.defaultSolver = new DefaultLogicSolver();
this.visualizer = new ASPVisualizer();
this.explainer = new ASPExplainer();
}
/**
* Main entry point for ASP logic operations
*/
async process(
operation: Operation,
input: string | ASPProgram | DefaultTheory,
format: InputFormat = 'natural'
): Promise<LogicResult> {
try {
logger.info('Processing ASP operation', { operation, format });
// Parse input
const parsed = this.parseInput(input, format);
// Route to appropriate operation
switch (operation) {
case 'validate':
return this.validate(parsed);
case 'formalize':
return this.formalize(parsed);
case 'visualize':
return this.visualize(parsed);
case 'solve':
return await this.solve(parsed);
default:
throw new Error(`Unsupported operation: ${operation}`);
}
} catch (error) {
logger.error('ASP processing error', { error });
return {
status: 'error',
message: error instanceof Error ? error.message : 'Unknown error',
details: {
system: 'asp' as LogicalSystem
}
};
}
}
/**
* Parse input based on format
*/
private parseInput(input: string | any, format: InputFormat): ASPProgram | DefaultTheory {
if (typeof input === 'string') {
// Check if it looks like default logic
if (this.isDefaultLogic(input)) {
return this.parseDefaultLogic(input);
}
return this.parser.parse(input, format);
}
// Already structured
return input;
}
/**
* Check if input is default logic
*/
private isDefaultLogic(input: string): boolean {
return input.toLowerCase().includes('typically') ||
input.toLowerCase().includes('by default') ||
input.toLowerCase().includes('unless') ||
input.toLowerCase().includes('normally') ||
/:\s*not\s+\w+\s*\//.test(input);
}
/**
* Parse default logic syntax
*/
private parseDefaultLogic(input: string): DefaultTheory {
const theory: DefaultTheory = {
facts: [],
rules: []
};
const lines = input.split(/\r?\n/).filter(line => line.trim());
for (const line of lines) {
// Check for default rule: "α : β / γ"
const defaultMatch = line.match(/(.+?)\s*:\s*(.+?)\s*\/\s*(.+)/);
if (defaultMatch) {
const [, prerequisite, justifications, conclusion] = defaultMatch;
theory.rules.push({
prerequisite: prerequisite.trim(),
justifications: justifications.split(',').map(j => j.trim()),
conclusion: conclusion.trim()
});
}
// Natural language defaults
else if (line.toLowerCase().includes('typically') || line.toLowerCase().includes('normally')) {
const match = line.match(/(?:typically|normally)\s+(.+?)\s+unless\s+(.+)/i);
if (match) {
const [, conclusion, exception] = match;
theory.rules.push({
prerequisite: 'true',
justifications: [`not ${exception.trim()}`],
conclusion: conclusion.trim()
});
}
}
// Facts (simple statements)
else if (!line.includes(':') && !line.includes('/')) {
theory.facts.push(line.trim());
}
}
return theory;
}
/**
* Validate ASP program
*/
private validate(input: ASPProgram | DefaultTheory): LogicResult {
if ('rules' in input && 'facts' in input && Array.isArray(input.facts) && typeof input.facts[0] === 'string') {
// It's a default theory - validate it
return {
status: 'success',
message: 'Default theory is valid',
details: {
system: 'asp' as LogicalSystem,
analysis: {
isValid: true,
fallacies: [],
explanation: 'Default theory structure is correct'
}
}
};
}
const program = input as ASPProgram;
const analysis = this.validator.validate(program);
return {
status: analysis.hasAnswerSets ? 'success' : 'warning',
message: analysis.explanation,
details: {
system: 'asp' as LogicalSystem,
analysis: {
isValid: analysis.hasAnswerSets,
fallacies: [],
explanation: analysis.explanation
}
}
};
}
/**
* Formalize to ASP syntax
*/
private formalize(input: ASPProgram | DefaultTheory): LogicResult {
let formatted: string;
if ('rules' in input && Array.isArray(input.facts) && typeof input.facts[0] === 'string') {
// Default theory
formatted = this.formatDefaultTheory(input as DefaultTheory);
} else {
// ASP program
formatted = this.formatter.formatProgram(input as ASPProgram);
}
return {
status: 'success',
message: 'Program formalized successfully',
details: {
system: 'asp' as LogicalSystem,
formalizedInput: formatted
}
};
}
/**
* Visualize ASP program
*/
private visualize(input: ASPProgram | DefaultTheory): LogicResult {
let visualization: string;
if ('rules' in input && Array.isArray(input.facts) && typeof input.facts[0] === 'string') {
// Default theory visualization
visualization = this.visualizeDefaultTheory(input as DefaultTheory);
} else {
// ASP program visualization
visualization = this.visualizer.visualizeProgram(input as ASPProgram);
}
return {
status: 'success',
message: 'Visualization generated',
details: {
system: 'asp' as LogicalSystem,
visualization
}
};
}
/**
* Solve ASP program or default theory
*/
private async solve(input: ASPProgram | DefaultTheory): Promise<LogicResult> {
// Check if default logic
const isDefaultTheory = 'rules' in input && Array.isArray(input.facts) && input.facts.length > 0 && typeof input.facts[0] === 'string';
if (isDefaultTheory) {
return this.solveDefaultTheory(input as DefaultTheory);
} else {
return this.solveASPProgram(input as ASPProgram);
}
}
/**
* Solve ASP program
*/
private async solveASPProgram(program: ASPProgram): Promise<LogicResult> {
try {
// Convert to Clingo syntax
const clingoProgram = this.parser.toClingoSyntax(program);
// Solve
const solution = await this.solver.solve(clingoProgram, { maxModels: 10 });
// Format solution
const formatted = this.formatter.formatSolution(solution);
// Generate visualization
const visualization = this.visualizer.visualizeSolution(solution);
return {
status: 'success',
message: solution.satisfiable
? `Found ${solution.totalModels} answer set(s)`
: 'No answer sets (UNSATISFIABLE)',
details: {
system: 'asp' as LogicalSystem,
solution: {
steps: [
{
index: 1,
statement: formatted,
rule: 'Stable Model Semantics',
justification: 'Computed via Clingo ASP solver'
}
],
conclusion: formatted
},
visualization
}
};
} catch (error) {
// Synchronous fallback
return {
status: 'error',
message: error instanceof Error ? error.message : 'Solving failed',
details: {
system: 'asp' as LogicalSystem,
suggestion: 'Ensure Clingo is installed: brew install clingo'
}
};
}
}
/**
* Solve default theory
*/
private async solveDefaultTheory(theory: DefaultTheory): Promise<LogicResult> {
try {
const result = await this.defaultSolver.solve(theory);
let message = `Found ${result.extensions.length} extension(s)`;
if (result.queryResult) {
if (result.queryResult.skepticallyTrue) {
message += ` - Query is skeptically TRUE`;
} else if (result.queryResult.credulouslyTrue) {
message += ` - Query is credulously TRUE`;
} else {
message += ` - Query is FALSE`;
}
}
return {
status: 'success',
message,
details: {
system: 'asp' as LogicalSystem,
solution: {
steps: result.extensions.map((ext, idx) => ({
index: idx + 1,
statement: `Extension ${ext.id}: ${ext.facts.slice(0, 5).join(', ')}${ext.facts.length > 5 ? '...' : ''}`,
rule: 'Default Logic',
justification: ext.explanation
})),
conclusion: message
}
}
};
} catch (error) {
return {
status: 'error',
message: error instanceof Error ? error.message : 'Default reasoning failed',
details: {
system: 'asp' as LogicalSystem
}
};
}
}
/**
* Format default theory
*/
private formatDefaultTheory(theory: DefaultTheory): string {
let output = '% Facts\n';
for (const fact of theory.facts) {
output += `${fact}\n`;
}
output += '\n% Default Rules\n';
for (const rule of theory.rules) {
output += `${rule.prerequisite} : ${rule.justifications.join(', ')} / ${rule.conclusion}\n`;
}
return output;
}
/**
* Visualize default theory
*/
private visualizeDefaultTheory(theory: DefaultTheory): string {
let viz = '=== Default Theory ===\n\n';
viz += `Facts: ${theory.facts.length}\n`;
viz += `Rules: ${theory.rules.length}\n\n`;
viz += '--- Facts ---\n';
for (const fact of theory.facts) {
viz += ` ${fact}\n`;
}
viz += '\n--- Default Rules ---\n';
for (const rule of theory.rules) {
viz += ` ${rule.prerequisite} : ${rule.justifications.join(', ')} / ${rule.conclusion}\n`;
}
return viz;
}
}
