// Types for logical systems
// Common types across all logical systems
export type LogicalSystem = 'syllogistic' | 'propositional' | 'predicate' | 'mathematical' | 'modal' | 'temporal' | 'fuzzy' | 'deontic' | 'smt' | 'probabilistic' | 'asp' | 'auto';
export type Operation = 'validate' | 'formalize' | 'visualize' | 'solve';
export type InputFormat = 'natural' | 'symbolic' | 'mixed';
// Import error types
import { EnhancedLogicError } from './errorHandler.js';
// Basic result interface
export interface LogicResult {
status: 'success' | 'error' | 'warning';
message: string;
code?: string;
details: {
system: LogicalSystem;
formalizedInput?: string;
analysis?: LogicalAnalysis;
visualization?: string;
solution?: LogicalSolution;
errorType?: string;
location?: string;
suggestion?: string;
example?: string;
originalInput?: string;
};
}
// Success result type
export type LogicSuccess = Omit<LogicResult, 'status'> & { status: 'success' };
// Warning result type
export type LogicWarning = Omit<LogicResult, 'status'> & { status: 'warning' };
// Error can now be either the simple error or the enhanced error
export type LogicError = EnhancedLogicError | (Omit<LogicResult, 'status'> & { status: 'error' });
// Analysis types
export interface LogicalAnalysis {
isValid: boolean;
fallacies: LogicalFallacy[];
explanation: string;
counterexample?: string;
}
export interface LogicalFallacy {
name: string;
description: string;
location: string;
}
// Solution types
export interface LogicalSolution {
steps: SolutionStep[];
conclusion: string;
}
export interface SolutionStep {
index: number;
statement: string;
rule: string;
justification: string;
}
// Syllogistic Logic Types
export type SyllogisticType = 'A' | 'E' | 'I' | 'O';
export interface SyllogisticStatement {
type: SyllogisticType;
subject: string;
predicate: string;
}
export interface SyllogisticArgument {
majorPremise: SyllogisticStatement;
minorPremise: SyllogisticStatement;
conclusion: SyllogisticStatement;
}
// Propositional Logic Types
export type PropositionalOperator =
'and' | 'or' | 'not' | 'implies' | 'iff' | 'xor' |
'∧' | '∨' | '¬' | '→' | '↔' | '⊕';
export type PropositionalFormula =
| { type: 'variable'; name: string }
| { type: 'unary'; operator: 'not' | '¬'; operand: PropositionalFormula }
| {
type: 'binary';
operator: Exclude<PropositionalOperator, 'not' | '¬'>;
left: PropositionalFormula;
right: PropositionalFormula
};
export interface PropositionalArgument {
premises: PropositionalFormula[];
conclusion: PropositionalFormula;
}
// Modal Logic Types
export type ModalOperator = 'necessary' | 'possible' | '□' | '◇';
export type ModalSystem = 'K' | 'T' | 'D' | 'B' | 'K4' | 'KB' | 'S4' | 'S5' | 'KD45';
export type ModalFormula =
| PropositionalFormula
| { type: 'modal'; operator: ModalOperator; operand: ModalFormula };
export interface ModalArgument {
premises: ModalFormula[];
conclusion: ModalFormula;
system: ModalSystem;
}
export interface ModalSemantics {
worlds: Set<string>;
relations: Map<string, Set<string>>;
valuations: Map<string, Map<string, boolean>>;
}
export interface KripkeFrame {
worlds: string[];
accessibility: Array<[string, string]>;
valuation: { [world: string]: { [prop: string]: boolean } };
}
export interface Countermodel {
frame: KripkeFrame;
failingWorld: string;
explanation: string;
premiseEvaluations: { [premise: string]: boolean };
conclusionEvaluation: boolean;
}
// Predicate Logic Types
export type Quantifier = 'forall' | 'exists' | '∀' | '∃';
export type PredicateFormula =
| { type: 'variable'; name: string }
| { type: 'constant'; name: string }
| { type: 'function'; name: string; args: PredicateFormula[] }
| { type: 'predicate'; name: string; args: PredicateFormula[] }
| { type: 'unary'; operator: 'not' | '¬'; operand: PredicateFormula }
| {
type: 'binary';
operator: Exclude<PropositionalOperator, 'not' | '¬'>;
left: PredicateFormula;
right: PredicateFormula
}
| {
type: 'quantified';
quantifier: Quantifier;
variable: string;
formula: PredicateFormula;
};
export interface PredicateArgument {
premises: PredicateFormula[];
conclusion: PredicateFormula;
}
// Mathematical Logic Types
export type MathematicalOperator =
'+' | '-' | '*' | '/' | '%' | '=' | '<' | '>' | '<=' | '>=' | '!=' |
'sum' | 'product' | 'difference' | 'ratio' | 'power';
export type MathematicalTerm =
| { type: 'number'; value: number }
| { type: 'variable'; name: string }
| { type: 'operation'; operator: MathematicalOperator; operands: MathematicalTerm[] }
| { type: 'sequence'; name: string; index: number }
| { type: 'constraint'; condition: MathematicalCondition };
export type MathematicalCondition =
| { type: 'equals'; left: MathematicalTerm; right: MathematicalTerm }
| { type: 'compare'; operator: '<' | '>' | '<=' | '>='; left: MathematicalTerm; right: MathematicalTerm }
| { type: 'range'; value: MathematicalTerm; min: number; max: number }
| { type: 'pattern'; sequence: MathematicalTerm[]; pattern: string };
export interface MathematicalArgument {
terms: MathematicalTerm[];
constraints: MathematicalCondition[];
question: string;
}
export interface SequencePattern {
type: 'arithmetic' | 'geometric' | 'quadratic' | 'fibonacci' | 'custom';
parameters: number[];
confidence: number;
formula: string;
}
// Temporal Logic Types
export type TemporalOperator = 'G' | 'F' | 'X' | 'U' | 'R' | 'W';
export type TemporalFormula =
| { type: 'atom'; name: string }
| { type: 'negation'; operand: TemporalFormula }
| { type: 'and'; left: TemporalFormula; right: TemporalFormula }
| { type: 'or'; left: TemporalFormula; right: TemporalFormula }
| { type: 'implication'; left: TemporalFormula; right: TemporalFormula }
| { type: 'temporal'; operator: TemporalOperator; operands: TemporalFormula[] };
export interface TemporalArgument {
premises: TemporalFormula[];
conclusion: TemporalFormula;
}
export interface TemporalTrace {
states: Array<{
time: number;
propositions: Map<string, boolean>;
}>;
}
// Fuzzy Logic Types
export type FuzzyOperator = 'AND' | 'OR' | 'NOT' | 'IMPLIES';
export type FuzzyHedge = 'very' | 'somewhat' | 'slightly' | 'extremely';
export interface FuzzySet {
name: string;
membershipFunction: (x: number) => number;
domain: [number, number];
}
export interface FuzzyFormula {
type: 'atom' | 'compound' | 'hedged';
atom?: string;
operator?: FuzzyOperator;
hedge?: FuzzyHedge;
operands?: FuzzyFormula[];
degree?: number;
}
// Deontic Logic Types
export type DeonticOperator = 'O' | 'P' | 'F' | 'OB' | 'PM' | 'IM';
export type DeonticFormula =
| { type: 'atom'; name: string }
| { type: 'negation'; operand: DeonticFormula }
| { type: 'and'; left: DeonticFormula; right: DeonticFormula }
| { type: 'or'; left: DeonticFormula; right: DeonticFormula }
| { type: 'implication'; left: DeonticFormula; right: DeonticFormula }
| { type: 'deontic'; operator: DeonticOperator; operand: DeonticFormula };
// SMT (Satisfiability Modulo Theories) Types
export type SMTVariableType = 'Int' | 'Real' | 'Bool' | 'String' | 'BitVec' | 'Array';
export interface SMTVariable {
name: string;
type: SMTVariableType;
bitWidth?: number; // For BitVec types
}
export interface SMTConstraint {
type: 'constraint' | 'soft';
expression: string;
weight?: number; // For soft constraints
name?: string;
}
export interface SMTOptimization {
direction: 'minimize' | 'maximize';
objective: string;
name?: string;
}
export interface SMTProblem {
variables: SMTVariable[];
constraints: SMTConstraint[];
optimization?: SMTOptimization;
}
export type SMTStatus = 'sat' | 'unsat' | 'unknown';
export interface SMTSolution {
status: SMTStatus;
model?: { [variable: string]: string | number | boolean };
objectiveValue?: number;
unsatCore?: string[];
reason?: string;
}
export interface SMTAnalysis {
isSatisfiable: boolean;
explanation: string;
counterexample?: string;
solution?: SMTSolution;
}
// Probabilistic Logic Types
export interface ProbabilisticFact {
probability: number;
fact: string;
label?: string;
}
export interface ProbabilisticRule {
head: string;
body: string[];
probability?: number; // For probabilistic rules like 0.7::rain :- clouds.
label?: string;
}
export interface ProbabilisticProgram {
facts: ProbabilisticFact[];
rules: ProbabilisticRule[];
evidence?: Record<string, boolean>; // Observed facts
queries?: string[];
}
export interface ProbabilisticQuery {
query: string; // e.g., "rain"
evidence?: Record<string, boolean>; // e.g., {"clouds": true}
program?: ProbabilisticProgram; // Background knowledge
}
export interface DerivationStep {
stepNumber: number;
rule: string;
probability: number;
dependencies: string[];
}
export interface ProbabilisticResult {
query: string;
probability: number;
evidence?: Record<string, boolean>;
explanation?: string;
derivationTrace?: DerivationStep[];
confidence?: {
lower: number;
upper: number;
};
}
export interface BayesianInference {
prior: Record<string, number>; // Prior probabilities
posterior: Record<string, number>; // Posterior after evidence
likelihood: number;
evidence: Record<string, boolean>;
method: 'exact' | 'approximate';
explanation?: string;
}
export interface ParameterLearningRequest {
program: ProbabilisticProgram; // Program structure (rules)
trainingData: Array<{ // Observed examples
evidence: Record<string, boolean>;
query: string;
observed: boolean;
}>;
learningRate?: number;
maxIterations?: number;
algorithm?: 'em' | 'gradient_descent' | 'lbfgs';
}
export interface LearnedProgram {
program: ProbabilisticProgram; // Program with learned probabilities
accuracy: number; // Training accuracy
testAccuracy?: number; // Test set accuracy (if provided)
convergenceInfo: {
iterations: number;
finalLoss: number;
converged: boolean;
};
parameterChanges: Array<{
parameter: string;
before: number;
after: number;
}>;
}
export interface DecisionProblem {
states: string[]; // Possible world states
actions: string[]; // Available actions
utilities: Record<string, number>; // State → utility mapping
transitionModel: ProbabilisticProgram; // P(state | action, evidence)
evidence?: Record<string, boolean>;
horizon?: number; // For sequential decisions
}
export interface DecisionRecommendation {
recommendedAction: string;
expectedUtility: number;
confidence: number;
alternatives: Array<{
action: string;
expectedUtility: number;
probability: number;
}>;
riskAnalysis: {
bestCase: { utility: number; probability: number };
worstCase: { utility: number; probability: number };
variance: number;
};
explanation: string;
}
export type ExplanationType = 'trace' | 'counterfactual' | 'graphical' | 'narrative';
export type DetailLevel = 'brief' | 'detailed' | 'technical';
export interface ExplanationRequest {
result: ProbabilisticResult | BayesianInference | DecisionRecommendation;
explanationType: ExplanationType;
detail: DetailLevel;
}
export interface ProbabilisticExplanation {
type: string;
summary: string;
details: string[];
visualization?: string; // ASCII art or description
counterfactuals?: Array<{
hypothesis: string;
probability: number;
comparison: string;
}>;
keyFactors: Array<{
factor: string;
impact: number; // How much this affects the result
direction: 'increases' | 'decreases';
}>;
}
export interface ProbabilisticAnalysis {
isValid: boolean;
errors: string[];
warnings: string[];
explanation: string;
}
// ASP (Answer Set Programming) Types
export interface ASPAtom {
predicate: string;
terms: (string | number)[];
negation?: 'classical' | 'default' | 'none'; // ¬ vs not vs positive
}
export interface ASPRule {
head: ASPAtom | ASPAtom[]; // Single atom or disjunctive head
body: ASPLiteral[];
type: 'normal' | 'choice' | 'disjunctive' | 'constraint';
weight?: number; // For weak constraints
priority?: number; // For weak constraints
}
export interface ASPLiteral {
atom: ASPAtom;
negation: 'classical' | 'default' | 'none'; // ¬ vs not vs positive
}
export interface ASPConstraint {
type: 'integrity' | 'weak';
body: ASPLiteral[];
weight?: number; // For weak constraints
priority?: number; // For weak constraints
terms?: string[]; // For weak constraint terms
}
export interface ChoiceRule {
head: ASPAtom[];
bounds: { lower: number; upper: number };
body: ASPLiteral[];
}
export interface ASPProgram {
rules: ASPRule[];
facts: ASPAtom[];
constraints: ASPConstraint[];
weakConstraints?: ASPConstraint[];
choices?: ChoiceRule[];
}
export interface AnswerSet {
id: number;
atoms: ASPAtom[];
cost?: number[]; // For optimized solutions (multi-level costs)
isOptimal?: boolean;
}
export interface ASPSolution {
answerSets: AnswerSet[];
totalModels: number;
optimal?: boolean;
computationTime: number;
satisfiable: boolean;
}
export interface ASPAnalysis {
hasAnswerSets: boolean;
answerSetCount: number;
explanation: string;
cautiousConsequences?: ASPAtom[]; // True in all answer sets
braveConsequences?: ASPAtom[]; // True in some answer set
unsatCore?: ASPRule[];
conflicts?: ASPConflict[];
}
export interface ASPConflict {
type: 'constraint_violation' | 'circular_dependency' | 'contradiction';
involvedRules: ASPRule[];
explanation: string;
location?: string;
}
export interface OptimizationObjective {
direction: 'minimize' | 'maximize';
expression: string;
weight: number;
priority: number; // Multi-level: priority 2 > priority 1
description?: string;
}
export interface ASPOptimizationProblem {
program: ASPProgram;
objectives: OptimizationObjective[];
boundOptimum?: number;
}
export interface OptimizationResult {
optimalModels: AnswerSet[];
optimumCost: number[]; // Multi-level costs [level1, level2, ...]
totalModelsChecked: number;
improvementTrace: Array<{
iteration: number;
cost: number[];
model: AnswerSet;
}>;
explanation: string;
}
// Default Logic Types (integrated with ASP)
export interface DefaultRule {
id?: string;
prerequisite: string; // α
justifications: string[]; // β (what must be consistent)
conclusion: string; // γ
priority?: number;
naturalLanguage?: string;
}
export interface DefaultTheory {
facts: string[];
rules: DefaultRule[];
}
export interface DefaultExtension {
id: string;
facts: string[]; // Deductively closed set
appliedDefaults: string[];
explanation: string;
}
export interface DefaultReasoningResult {
extensions: DefaultExtension[];
query?: string;
queryResult?: {
credulouslyTrue: boolean; // True in some extension
skepticallyTrue: boolean; // True in all extensions
supportingExtensions: number[];
};
conflicts?: Array<{
default1: string;
default2: string;
reason: string;
}>;
}
// ASP Explanation Types
export interface DerivationNode {
atom: string;
derivedBy: {
rule: ASPRule;
premises: DerivationNode[];
negativeConditions: string[]; // What was checked not to hold
};
depth: number;
}
export interface RuleApplication {
step: number;
rule: ASPRule;
substitution: Record<string, string>;
derived: string;
justification: string;
}
export interface ASPExplanation {
type: 'derivation' | 'stability' | 'why_not' | 'comparison';
summary: string;
derivationTree?: DerivationNode;
ruleApplications: RuleApplication[];
visualization?: string;
insights: string[];
}
