From 4e2b3348daa5bf9dcc374fdde8a4c583c8ab01fb Mon Sep 17 00:00:00 2001 From: pseudodionysius <36469636+pseudodionysius@users.noreply.github.com> Date: Fri, 10 Apr 2026 15:17:46 +0100 Subject: [PATCH 1/2] feat: add dialectical map engine for multi-argument contention analysis MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Introduce a DialecticalMap module that organises an unbounded collection of structured Argument entities around a ContentiousClaim. Each argument carries its own premises, sub-conclusion, target (claim / argument / premise), and stance (supports / attacks / qualifies / undermines / concedes). DialecticalMap.evaluate() performs propositional formal evaluation of each argument's internal validity (premise-conjunction ⊨ sub-conclusion), the relation of each sub-conclusion to the central claim, and a C(n,2) pairwise tension matrix across all argument pairs. Argument strength is scored as avg(premise.confidence) × validity weight. Also exposes the previously private pairwise entailment machinery as a typed public API: PairwiseRelation and PairwiseSentenceRelation are promoted to the shared Theory interface and implemented on all three theory classes. New files: src/engine/dialectic/{dialecticTypes,dialecticalMap,dialecticalMapBuilder,index}.ts New tests: test/engine/dialectic/{dialecticalMap,dialecticalMapBuilder}.spec.ts --- src/engine/dialectic/dialecticTypes.ts | 133 ++++++++ src/engine/dialectic/dialecticalMap.ts | 297 ++++++++++++++++++ src/engine/dialectic/dialecticalMapBuilder.ts | 80 +++++ src/engine/dialectic/index.ts | 3 + src/engine/index.ts | 3 +- src/language/modal/modalTheory.ts | 19 +- .../propositional/propositionalTheory.ts | 38 +-- .../quantificationalTheory.ts | 19 +- src/language/shared/theory.ts | 35 +++ test/engine/dialectic/dialecticalMap.spec.ts | 294 +++++++++++++++++ .../dialectic/dialecticalMapBuilder.spec.ts | 150 +++++++++ 11 files changed, 1048 insertions(+), 23 deletions(-) create mode 100644 src/engine/dialectic/dialecticTypes.ts create mode 100644 src/engine/dialectic/dialecticalMap.ts create mode 100644 src/engine/dialectic/dialecticalMapBuilder.ts create mode 100644 src/engine/dialectic/index.ts create mode 100644 test/engine/dialectic/dialecticalMap.spec.ts create mode 100644 test/engine/dialectic/dialecticalMapBuilder.spec.ts diff --git a/src/engine/dialectic/dialecticTypes.ts b/src/engine/dialectic/dialecticTypes.ts new file mode 100644 index 0000000..6a6f339 --- /dev/null +++ b/src/engine/dialectic/dialecticTypes.ts @@ -0,0 +1,133 @@ +import { AlethicAssertoric } from '../../language/shared/types'; +import { PairwiseRelation } from '../../language/shared/theory'; + +// ─── Argument targeting ─────────────────────────────────────────────────────── + +/** + * What an argument's sub-conclusion is directed at. + * + * - claim — targets the central contention directly + * - argument — targets another argument's sub-conclusion + * - premise — targets a specific premise within another argument + */ +export type ArgumentTarget = + | { kind: 'claim' } + | { kind: 'argument'; argumentId: string } + | { kind: 'premise'; argumentId: string; premiseIndex: number }; + +// ─── Argument stance ────────────────────────────────────────────────────────── + +/** + * How an argument relates to its target. + * + * - supports — sub-conclusion establishes or corroborates the target + * - attacks — sub-conclusion entails the negation of the target + * - qualifies — narrows or conditions the target (reduces scope or strength) + * - undermines — attacks a presupposition of the target without directly + * negating it + * - concedes — grants the target but limits its downstream implications + */ +export type ArgumentStance = + | 'supports' + | 'attacks' + | 'qualifies' + | 'undermines' + | 'concedes'; + +// ─── Argument ───────────────────────────────────────────────────────────────── + +/** + * A single structured argument — a set of premises leading to a + * sub-conclusion, directed at a target with a declared stance. + */ +export interface Argument { + /** Unique identifier for this argument within the dialectical map. */ + id: string; + /** Human-readable name for display (e.g. "The Deterrence Argument"). */ + label: string; + /** The premises that ground this argument. May be empty. */ + premises: AlethicAssertoric[]; + /** The claim this argument establishes. */ + subConclusion: AlethicAssertoric; + /** What this argument is directed at. */ + target: ArgumentTarget; + /** How this argument relates to its target. */ + stance: ArgumentStance; +} + +// ─── ContentiousClaim ──────────────────────────────────────────────────────── + +/** The central claim under dispute around which all arguments are organised. */ +export interface ContentiousClaim { + claim: AlethicAssertoric; + label: string; +} + +// ─── Evaluation output types ───────────────────────────────────────────────── + +/** + * How strongly the premises formally support the sub-conclusion. + * + * - valid — premises ⊨ sub-conclusion (ENTAILS_RIGHT) + * - consistent — premises are consistent with sub-conclusion but do not entail it + * - inconsistent — premises are inconsistent with sub-conclusion + * - undetermined — zero premises or the NLP pipeline produced no usable formula + */ +export type EntailmentStrength = + | 'valid' + | 'consistent' + | 'inconsistent' + | 'undetermined'; + +/** + * How the sub-conclusion relates to the central claim. + * + * - entails — sub-conclusion ⊨ claim + * - entailed-by — claim ⊨ sub-conclusion + * - equivalent — sub-conclusion ⟺ claim + * - contradicts — sub-conclusion and claim cannot both be true + * - consistent — can both be true, no entailment in either direction + * - undetermined — no shared propositions or NLP produced no usable formula + */ +export type ClaimRelation = + | 'entails' + | 'entailed-by' + | 'equivalent' + | 'contradicts' + | 'consistent' + | 'undetermined'; + +/** Formal evaluation of a single argument. */ +export interface ArgumentEvaluation { + /** The id of the argument this evaluation applies to. */ + argumentId: string; + /** Whether the premises formally entail the sub-conclusion. */ + internalValidity: EntailmentStrength; + /** How the sub-conclusion relates to the central claim. */ + claimRelation: ClaimRelation; + /** + * Aggregate strength score in [0, 1]. + * + * Computed as: mean(premise.confidence) × validityWeight + * where validityWeight is 1.0 (valid), 0.5 (consistent), 0.0 (otherwise). + */ + strength: number; +} + +/** Pairwise formal tension between two arguments' sub-conclusions. */ +export interface ArgumentTension { + argumentIdA: string; + argumentIdB: string; + /** The pairwise logical relation between the two sub-conclusions. */ + conclusionRelation: PairwiseRelation; +} + +/** Full output of DialecticalMap.evaluate(). */ +export interface DialecticalMapResult { + claim: ContentiousClaim; + arguments: Argument[]; + /** One evaluation per argument, in input order. */ + evaluations: ArgumentEvaluation[]; + /** C(n, 2) pairwise tension records for n arguments, in (i, j) order. */ + tensions: ArgumentTension[]; +} diff --git a/src/engine/dialectic/dialecticalMap.ts b/src/engine/dialectic/dialecticalMap.ts new file mode 100644 index 0000000..94f141d --- /dev/null +++ b/src/engine/dialectic/dialecticalMap.ts @@ -0,0 +1,297 @@ +import { AlethicAssertoric, SentenceSet } from '../../language/shared/types'; +import { PairwiseRelation } from '../../language/shared/theory'; +import { PropositionalVariable } from '../../language/propositional/propositionalVariable'; +import { PropositionalFormalSentence, PropositionalTheory } from '../../language/propositional/propositionalTheory'; +import { FormalAnnotator } from '../nlp/formalAnnotator'; +import { FormalTranslator } from '../nlp/formalTranslator'; +import { PropositionalSyntaxEngine } from '../syntax/propositional/syntaxEngine'; +import { + Argument, + ArgumentEvaluation, + ArgumentTension, + ClaimRelation, + ContentiousClaim, + DialecticalMapResult, + EntailmentStrength, +} from './dialecticTypes'; + +// ─── DialecticalMap ─────────────────────────────────────────────────────────── + +/** + * Evaluates a collection of structured arguments around a central contention. + * + * For each argument, checks: + * - Internal validity: do the premises formally entail the sub-conclusion? + * - Claim relation: how does the sub-conclusion relate to the central claim? + * - Strength: avg premise confidence weighted by validity. + * + * Also computes pairwise tensions (sub-conclusion vs sub-conclusion) across + * all argument pairs. + * + * All formal evaluation is propositional. Construct via DialecticalMapBuilder. + */ +export class DialecticalMap { + + constructor( + private readonly _claim: ContentiousClaim, + private readonly _arguments: Argument[], + ) {} + + // ── Public API ───────────────────────────────────────────────────────────── + + /** + * Run the full evaluation pipeline and return a DialecticalMapResult. + */ + evaluate(): DialecticalMapResult { + const evaluations = this._arguments.map(arg => this._evaluateArgument(arg)); + const tensions = this._computeTensions(); + return { + claim: this._claim, + arguments: this._arguments, + evaluations, + tensions, + }; + } + + /** + * Print a formatted report of the dialectical evaluation to the console. + */ + printReport(): void { + const result = this.evaluate(); + + console.log('\nDIALECTICAL MAP REPORT'); + console.log('═'.repeat(50)); + + console.log(`\nCentral Claim [${result.claim.label}]`); + console.log(` "${result.claim.claim.raw}"`); + console.log(` confidence: ${result.claim.claim.confidence.toFixed(2)}`); + + console.log(`\nArguments (${result.arguments.length}):`); + + for (const arg of result.arguments) { + const ev = result.evaluations.find(e => e.argumentId === arg.id)!; + const targetLabel = this._targetLabel(arg); + + console.log(`\n [${arg.id}] ${arg.label} (${arg.stance} → ${targetLabel})`); + + if (arg.premises.length > 0) { + console.log(' Premises:'); + arg.premises.forEach(p => + console.log(` • "${p.raw}" (confidence: ${p.confidence.toFixed(2)})`), + ); + } else { + console.log(' Premises: (none)'); + } + + console.log(` Sub-conclusion: "${arg.subConclusion.raw}"`); + console.log( + ` Validity: ${ev.internalValidity.padEnd(12)}` + + ` Claim relation: ${ev.claimRelation.padEnd(14)}` + + ` Strength: ${ev.strength.toFixed(3)}`, + ); + } + + if (result.tensions.length > 0) { + console.log('\nPairwise tensions (sub-conclusions):'); + for (const t of result.tensions) { + const aLabel = this._arguments.find(a => a.id === t.argumentIdA)?.label ?? t.argumentIdA; + const bLabel = this._arguments.find(a => a.id === t.argumentIdB)?.label ?? t.argumentIdB; + const relLabel = this._pairwiseLabel(t.conclusionRelation); + console.log(` ${aLabel} ↔ ${bLabel} ${relLabel}`); + } + } + + console.log(''); + } + + // ── Evaluation helpers ───────────────────────────────────────────────────── + + private _evaluateArgument(arg: Argument): ArgumentEvaluation { + const internalValidity = this._checkValidity(arg); + const claimRelation = this._checkClaimRelation(arg.subConclusion); + const strength = this._computeStrength(arg, internalValidity); + return { argumentId: arg.id, internalValidity, claimRelation, strength }; + } + + /** + * Check whether the argument's premises formally entail its sub-conclusion. + * + * Algorithm: + * 1. Translate all sentences (premises + sub-conclusion) via NLP pipeline. + * 2. Synthesize a conjunction of the premise formula strings. + * 3. Build a 2-sentence PropositionalTheory: [premise-conjunction, sub-conclusion]. + * 4. The pairwise relation ENTAILS_RIGHT → valid; CONSISTENT → consistent; + * INCONSISTENT → inconsistent; EQUIVALENT/ENTAILS_LEFT → consistent. + */ + private _checkValidity(arg: Argument): EntailmentStrength { + if (arg.premises.length === 0) return 'undetermined'; + + const allSentences: AlethicAssertoric[] = [...arg.premises, arg.subConclusion]; + const set: SentenceSet = { sentences: allSentences }; + + const annotated = new FormalAnnotator().annotateAll(allSentences); + const translations = new FormalTranslator().translate(set, annotated); + const propTrans = translations.propositional.sentences; + + if (propTrans.length < 2) return 'undetermined'; + + const premiseFormulas = propTrans.slice(0, -1).map(t => t.formulaString); + const conclusionFormula = propTrans[propTrans.length - 1].formulaString; + + const premiseConjunction = premiseFormulas.length === 1 + ? premiseFormulas[0] + : premiseFormulas.map(f => `(${f})`).join(' & '); + + const variables = new Map(); + const syntax = new PropositionalSyntaxEngine(); + + try { + const conjWFF = syntax.parseInto(premiseConjunction, variables); + const concWFF = syntax.parseInto(conclusionFormula, variables); + const varNames = Array.from(variables.keys()); + + const sentences: PropositionalFormalSentence[] = [ + { source: { raw: premiseConjunction, confidence: 1.0 }, formula: conjWFF, variableNames: varNames, label: 'P' }, + { source: arg.subConclusion, formula: concWFF, variableNames: varNames, label: 'C' }, + ]; + const theory = new PropositionalTheory(sentences, variables); + return this._entailmentFromRelation(theory.pairwiseRelations()[0].relation); + } catch { + return 'undetermined'; + } + } + + /** + * Check how the argument's sub-conclusion relates to the central claim. + * + * Translates both sentences together so shared proposition letters map to + * the same variable. + */ + private _checkClaimRelation(subConclusion: AlethicAssertoric): ClaimRelation { + const pair: AlethicAssertoric[] = [subConclusion, this._claim.claim]; + const set: SentenceSet = { sentences: pair }; + + const annotated = new FormalAnnotator().annotateAll(pair); + const translations = new FormalTranslator().translate(set, annotated); + const propTrans = translations.propositional.sentences; + + if (propTrans.length < 2) return 'undetermined'; + + const variables = new Map(); + const syntax = new PropositionalSyntaxEngine(); + + try { + const f1 = syntax.parseInto(propTrans[0].formulaString, variables); + const f2 = syntax.parseInto(propTrans[1].formulaString, variables); + const varNames = Array.from(variables.keys()); + + const sentences: PropositionalFormalSentence[] = [ + { source: subConclusion, formula: f1, variableNames: varNames, label: 'SC' }, + { source: this._claim.claim, formula: f2, variableNames: varNames, label: 'CL' }, + ]; + const theory = new PropositionalTheory(sentences, variables); + return this._claimRelationFromPairwise(theory.pairwiseRelations()[0].relation); + } catch { + return 'undetermined'; + } + } + + /** Compute pairwise tensions across all argument pairs. */ + private _computeTensions(): ArgumentTension[] { + const tensions: ArgumentTension[] = []; + const args = this._arguments; + + for (let i = 0; i < args.length; i++) { + for (let j = i + 1; j < args.length; j++) { + tensions.push(this._computeTension(args[i], args[j])); + } + } + + return tensions; + } + + private _computeTension(argA: Argument, argB: Argument): ArgumentTension { + const pair: AlethicAssertoric[] = [argA.subConclusion, argB.subConclusion]; + const set: SentenceSet = { sentences: pair }; + + const annotated = new FormalAnnotator().annotateAll(pair); + const translations = new FormalTranslator().translate(set, annotated); + const propTrans = translations.propositional.sentences; + + if (propTrans.length < 2) { + return { argumentIdA: argA.id, argumentIdB: argB.id, conclusionRelation: 'CONSISTENT' }; + } + + const variables = new Map(); + const syntax = new PropositionalSyntaxEngine(); + + try { + const f1 = syntax.parseInto(propTrans[0].formulaString, variables); + const f2 = syntax.parseInto(propTrans[1].formulaString, variables); + const varNames = Array.from(variables.keys()); + + const sentences: PropositionalFormalSentence[] = [ + { source: argA.subConclusion, formula: f1, variableNames: varNames, label: 'A' }, + { source: argB.subConclusion, formula: f2, variableNames: varNames, label: 'B' }, + ]; + const theory = new PropositionalTheory(sentences, variables); + const rel = theory.pairwiseRelations()[0].relation; + return { argumentIdA: argA.id, argumentIdB: argB.id, conclusionRelation: rel }; + } catch { + return { argumentIdA: argA.id, argumentIdB: argB.id, conclusionRelation: 'CONSISTENT' }; + } + } + + // ── Scoring ──────────────────────────────────────────────────────────────── + + private _computeStrength(arg: Argument, validity: EntailmentStrength): number { + if (arg.premises.length === 0) return 0; + const avgConfidence = arg.premises.reduce((s, p) => s + p.confidence, 0) / arg.premises.length; + const weight = validity === 'valid' ? 1.0 : validity === 'consistent' ? 0.5 : 0.0; + return avgConfidence * weight; + } + + // ── Relation mappings ────────────────────────────────────────────────────── + + // ENTAILS_LEFT is returned when s1TrueS2False=false, i.e. no case where s1=T and s2=F, + // i.e. s1 ⊨ s2 (the left sentence entails the right sentence). + // ENTAILS_RIGHT is the mirror: s2 ⊨ s1. + + private _entailmentFromRelation(rel: PairwiseRelation): EntailmentStrength { + switch (rel) { + case 'ENTAILS_LEFT': return 'valid'; // premise-conjunction ⊨ sub-conclusion + case 'INCONSISTENT': return 'inconsistent'; + default: return 'consistent'; + } + } + + private _claimRelationFromPairwise(rel: PairwiseRelation): ClaimRelation { + switch (rel) { + case 'ENTAILS_LEFT': return 'entails'; // sub-conclusion ⊨ claim + case 'ENTAILS_RIGHT': return 'entailed-by'; // claim ⊨ sub-conclusion + case 'EQUIVALENT': return 'equivalent'; + case 'INCONSISTENT': return 'contradicts'; + case 'CONSISTENT': return 'consistent'; + } + } + + // ── Display helpers ──────────────────────────────────────────────────────── + + private _targetLabel(arg: Argument): string { + switch (arg.target.kind) { + case 'claim': return 'claim'; + case 'argument': return `argument:${arg.target.argumentId}`; + case 'premise': return `premise[${arg.target.premiseIndex}] of ${arg.target.argumentId}`; + } + } + + private _pairwiseLabel(rel: PairwiseRelation): string { + switch (rel) { + case 'INCONSISTENT': return 'INCONSISTENT (cannot both be true)'; + case 'EQUIVALENT': return 'EQUIVALENT'; + case 'ENTAILS_RIGHT': return 'ENTAILS (A ⊨ B)'; + case 'ENTAILS_LEFT': return 'ENTAILS (B ⊨ A)'; + case 'CONSISTENT': return 'consistent'; + } + } +} diff --git a/src/engine/dialectic/dialecticalMapBuilder.ts b/src/engine/dialectic/dialecticalMapBuilder.ts new file mode 100644 index 0000000..fc7e288 --- /dev/null +++ b/src/engine/dialectic/dialecticalMapBuilder.ts @@ -0,0 +1,80 @@ +import { AlethicAssertoric } from '../../language/shared/types'; +import { Argument, ContentiousClaim } from './dialecticTypes'; +import { DialecticalMap } from './dialecticalMap'; + +// ─── DialecticalMapBuilder ──────────────────────────────────────────────────── + +/** + * Fluent builder for constructing a DialecticalMap. + * + * Set the central claim with claim(), add arguments with argument(), then + * call build() to produce an immutable DialecticalMap ready for evaluation. + * + * Example: + * + * ```ts + * const map = new DialecticalMapBuilder() + * .claim({ raw: 'Capital punishment is justified', confidence: 1.0 }, 'Central Claim') + * .argument({ + * id: 'deterrence', + * label: 'The Deterrence Argument', + * premises: [ + * { raw: 'Capital punishment deters violent crime', confidence: 0.8 }, + * { raw: 'Deterring crime saves innocent lives', confidence: 0.9 }, + * ], + * subConclusion: { raw: 'Capital punishment saves innocent lives', confidence: 0.85 }, + * target: { kind: 'claim' }, + * stance: 'supports', + * }) + * .build(); + * + * const result = map.evaluate(); + * map.printReport(); + * ``` + */ +export class DialecticalMapBuilder { + + private _claim: ContentiousClaim | null = null; + private readonly _arguments: Argument[] = []; + + /** + * Set the central contention around which all arguments are organised. + * Calling claim() a second time replaces the previous value. + * + * @param sentence - The assertoric sentence expressing the claim. + * @param label - Human-readable name for the claim. + * @returns this, for method chaining. + */ + claim(sentence: AlethicAssertoric, label: string): this { + this._claim = { claim: sentence, label }; + return this; + } + + /** + * Add a structured argument to the map. + * Arguments are stored in the order they are added. + * + * @param arg - The argument to add. + * @returns this, for method chaining. + */ + argument(arg: Argument): this { + this._arguments.push(arg); + return this; + } + + /** + * Finalise and return the DialecticalMap. + * Throws if no central claim has been set. + * + * @returns A new DialecticalMap containing the claim and all added arguments. + */ + build(): DialecticalMap { + if (this._claim === null) { + throw new Error( + 'DialecticalMapBuilder: cannot build without a central claim. ' + + 'Call .claim() before .build().', + ); + } + return new DialecticalMap(this._claim, [...this._arguments]); + } +} diff --git a/src/engine/dialectic/index.ts b/src/engine/dialectic/index.ts new file mode 100644 index 0000000..930987d --- /dev/null +++ b/src/engine/dialectic/index.ts @@ -0,0 +1,3 @@ +export * from './dialecticTypes'; +export * from './dialecticalMap'; +export * from './dialecticalMapBuilder'; diff --git a/src/engine/index.ts b/src/engine/index.ts index 9cbca01..e610530 100644 --- a/src/engine/index.ts +++ b/src/engine/index.ts @@ -1 +1,2 @@ -export * from './nlp/index'; \ No newline at end of file +export * from './nlp/index'; +export * from './dialectic/index'; \ No newline at end of file diff --git a/src/language/modal/modalTheory.ts b/src/language/modal/modalTheory.ts index f72bc60..6c25010 100644 --- a/src/language/modal/modalTheory.ts +++ b/src/language/modal/modalTheory.ts @@ -1,6 +1,6 @@ import { MFF, World, ModalEvaluationState, ModalSystemSpec } from './modalTypes'; import { ModalVariable } from './modalVariable'; -import { FormalSentence, Theory, ConsistencyResult, ProofNode } from '../shared/theory'; +import { FormalSentence, Theory, ConsistencyResult, ProofNode, PairwiseRelation, PairwiseSentenceRelation } from '../shared/theory'; // ─── Types ─────────────────────────────────────────────────────────────────── @@ -320,11 +320,26 @@ export class ModalTheory implements Theory { /** * Compute the pairwise logical relation between two sentences. */ + pairwiseRelations(): PairwiseSentenceRelation[] { + const propNames = Array.from(this.variables.keys()); + const results: PairwiseSentenceRelation[] = []; + for (let i = 0; i < this.sentences.length; i++) { + for (let j = i + 1; j < this.sentences.length; j++) { + results.push({ + a: this.sentences[i], + b: this.sentences[j], + relation: this._pairwiseRelation(this.sentences[i], this.sentences[j], propNames), + }); + } + } + return results; + } + private _pairwiseRelation( s1: ModalFormalSentence, s2: ModalFormalSentence, propNames: string[], - ): string { + ): PairwiseRelation { let bothTrue = false; let s1TrueS2False = false; let s1FalseS2True = false; diff --git a/src/language/propositional/propositionalTheory.ts b/src/language/propositional/propositionalTheory.ts index 750d49d..7e8fc5d 100644 --- a/src/language/propositional/propositionalTheory.ts +++ b/src/language/propositional/propositionalTheory.ts @@ -1,6 +1,6 @@ import { WFF } from './propositionalTypes'; import { PropositionalVariable } from './propositionalVariable'; -import { FormalSentence, Theory, ConsistencyResult, ProofNode } from '../shared/theory'; +import { FormalSentence, Theory, ConsistencyResult, ProofNode, PairwiseRelation, PairwiseSentenceRelation } from '../shared/theory'; // ─── Types ─────────────────────────────────────────────────────────────────── @@ -14,23 +14,6 @@ export interface PropositionalFormalSentence extends FormalSentence { variableNames: string[]; } -/** - * The pairwise logical relation between two sentences in the same theory, - * determined by exhaustive evaluation over all shared variable assignments. - * - * - INCONSISTENT — no assignment makes both sentences true simultaneously - * - EQUIVALENT — both sentences have the same truth value in every assignment - * - ENTAILS_RIGHT — s1 ⊨ s2: whenever s1 is true, s2 is also true - * - ENTAILS_LEFT — s2 ⊨ s1: whenever s2 is true, s1 is also true - * - CONSISTENT — there exists an assignment making both sentences true - */ -export type PairwiseRelation = - | 'INCONSISTENT' - | 'EQUIVALENT' - | 'ENTAILS_RIGHT' // s1 ⊨ s2 - | 'ENTAILS_LEFT' // s2 ⊨ s1 - | 'CONSISTENT'; - // ─── Internal helpers ──────────────────────────────────────────────────────── /** @@ -243,6 +226,25 @@ export class PropositionalTheory implements Theory { console.log(''); } + /** + * Return the pairwise logical relation for every (i, j) pair of sentences + * where i < j, as typed data. + */ + pairwiseRelations(): PairwiseSentenceRelation[] { + const varNames = Array.from(this.variables.keys()); + const results: PairwiseSentenceRelation[] = []; + for (let i = 0; i < this.sentences.length; i++) { + for (let j = i + 1; j < this.sentences.length; j++) { + results.push({ + a: this.sentences[i], + b: this.sentences[j], + relation: this._pairwiseRelation(this.sentences[i], this.sentences[j], varNames), + }); + } + } + return results; + } + // ── Private helpers ──────────────────────────────────────────────────────── /** Apply a bitmask as a variable assignment and return the valuation record. */ diff --git a/src/language/quantificational/quantificationalTheory.ts b/src/language/quantificational/quantificationalTheory.ts index c2f14d2..4a4833f 100644 --- a/src/language/quantificational/quantificationalTheory.ts +++ b/src/language/quantificational/quantificationalTheory.ts @@ -1,6 +1,6 @@ import { QFF, DomainElement, VariableAssignment } from './quantificationalTypes'; import { QuantificationalVariable } from './quantificationalVariable'; -import { FormalSentence, Theory, ConsistencyResult, ProofNode } from '../shared/theory'; +import { FormalSentence, Theory, ConsistencyResult, ProofNode, PairwiseRelation, PairwiseSentenceRelation } from '../shared/theory'; // ─── Types ─────────────────────────────────────────────────────────────────── @@ -250,11 +250,26 @@ export class QuantificationalTheory implements Theory { /** * Compute the pairwise logical relation between two sentences. */ + pairwiseRelations(): PairwiseSentenceRelation[] { + const varNames = Array.from(this.variables.keys()); + const results: PairwiseSentenceRelation[] = []; + for (let i = 0; i < this.sentences.length; i++) { + for (let j = i + 1; j < this.sentences.length; j++) { + results.push({ + a: this.sentences[i], + b: this.sentences[j], + relation: this._pairwiseRelation(this.sentences[i], this.sentences[j], varNames), + }); + } + } + return results; + } + private _pairwiseRelation( s1: QuantificationalFormalSentence, s2: QuantificationalFormalSentence, varNames: string[], - ): string { + ): PairwiseRelation { let bothTrue = false; let s1TrueS2False = false; let s1FalseS2True = false; diff --git a/src/language/shared/theory.ts b/src/language/shared/theory.ts index 17d789d..41160cd 100644 --- a/src/language/shared/theory.ts +++ b/src/language/shared/theory.ts @@ -1,5 +1,32 @@ import { Formula, AlethicAssertoric } from './types'; +// ─── Pairwise relation types ────────────────────────────────────────────────── + +/** + * The logical relation between two sentences determined by exhaustive + * evaluation over all variable assignments. + * + * - INCONSISTENT — no assignment makes both sentences true simultaneously + * - EQUIVALENT — both sentences have the same truth value in every assignment + * - ENTAILS_RIGHT — s1 ⊨ s2: whenever s1 is true, s2 is also true + * - ENTAILS_LEFT — s2 ⊨ s1: whenever s2 is true, s1 is also true + * - CONSISTENT — there exists an assignment making both sentences true, + * but neither entails the other + */ +export type PairwiseRelation = + | 'INCONSISTENT' + | 'EQUIVALENT' + | 'ENTAILS_LEFT' // s1 ⊨ s2 (no case where s1=T and s2=F) + | 'ENTAILS_RIGHT' // s2 ⊨ s1 (no case where s1=F and s2=T) + | 'CONSISTENT'; + +/** A typed pairwise relation record returned by Theory.pairwiseRelations(). */ +export interface PairwiseSentenceRelation { + a: FormalSentence; + b: FormalSentence; + relation: PairwiseRelation; +} + /** * A sentence within a formal theory — pairs the source natural language * sentence with its formal representation in a given logic. @@ -73,4 +100,12 @@ export interface Theory { * Shows pairwise consistency, entailment, and shared variables. */ printGraph(): void; + + /** + * Return the pairwise logical relation for every (i, j) pair of sentences + * where i < j, as typed data. + * + * The array has C(n, 2) entries for n sentences. + */ + pairwiseRelations(): PairwiseSentenceRelation[]; } diff --git a/test/engine/dialectic/dialecticalMap.spec.ts b/test/engine/dialectic/dialecticalMap.spec.ts new file mode 100644 index 0000000..7c6489f --- /dev/null +++ b/test/engine/dialectic/dialecticalMap.spec.ts @@ -0,0 +1,294 @@ +import { DialecticalMapBuilder } from '../../../src/engine/dialectic/dialecticalMapBuilder'; +import { Argument } from '../../../src/engine/dialectic/dialecticTypes'; + +// ─── Helpers ────────────────────────────────────────────────────────────────── + +function s(raw: string, confidence = 1.0) { + return { raw, confidence }; +} + +function claim(raw = 'The defendant is guilty') { + return s(raw, 1.0); +} + +function buildMap(args: Argument[], claimRaw = 'The defendant is guilty') { + const builder = new DialecticalMapBuilder().claim(claim(claimRaw), 'Central Claim'); + for (const arg of args) builder.argument(arg); + return builder.build(); +} + +// ─── Tests ──────────────────────────────────────────────────────────────────── + +describe('DialecticalMap — evaluate() result shape', () => { + + test('returns the central claim unchanged', () => { + const result = buildMap([]).evaluate(); + expect(result.claim.claim.raw).toBe('The defendant is guilty'); + expect(result.claim.label).toBe('Central Claim'); + }); + + test('evaluations has one entry per argument', () => { + const args: Argument[] = [ + { id: 'a1', label: 'A1', premises: [s('p')], subConclusion: s('q'), target: { kind: 'claim' }, stance: 'supports' }, + { id: 'a2', label: 'A2', premises: [s('r')], subConclusion: s('s'), target: { kind: 'claim' }, stance: 'attacks' }, + { id: 'a3', label: 'A3', premises: [s('t')], subConclusion: s('u'), target: { kind: 'claim' }, stance: 'qualifies' }, + ]; + const result = buildMap(args).evaluate(); + expect(result.evaluations).toHaveLength(3); + expect(result.evaluations.map(e => e.argumentId)).toEqual(['a1', 'a2', 'a3']); + }); + + test('tensions has C(n,2) entries for n arguments', () => { + const makeArg = (id: string): Argument => ({ + id, label: id, premises: [s('p is true')], subConclusion: s('q follows'), + target: { kind: 'claim' }, stance: 'supports', + }); + const result = buildMap([makeArg('a'), makeArg('b'), makeArg('c')]).evaluate(); + // C(3,2) = 3 pairs + expect(result.tensions).toHaveLength(3); + }); + + test('tension pairs are (a,b), (a,c), (b,c) in order', () => { + const makeArg = (id: string): Argument => ({ + id, label: id, premises: [s('p')], subConclusion: s('q'), + target: { kind: 'claim' }, stance: 'supports', + }); + const result = buildMap([makeArg('a'), makeArg('b'), makeArg('c')]).evaluate(); + expect(result.tensions[0]).toMatchObject({ argumentIdA: 'a', argumentIdB: 'b' }); + expect(result.tensions[1]).toMatchObject({ argumentIdA: 'a', argumentIdB: 'c' }); + expect(result.tensions[2]).toMatchObject({ argumentIdA: 'b', argumentIdB: 'c' }); + }); + + test('zero arguments produces empty evaluations and tensions', () => { + const result = buildMap([]).evaluate(); + expect(result.evaluations).toHaveLength(0); + expect(result.tensions).toHaveLength(0); + }); +}); + +// ───────────────────────────────────────────────────────────────────────────── + +describe('DialecticalMap — internal validity (internalValidity)', () => { + + test('zero premises → undetermined', () => { + const arg: Argument = { + id: 'no-premises', label: 'No premises', premises: [], + subConclusion: s('The conclusion is true'), + target: { kind: 'claim' }, stance: 'supports', + }; + const result = buildMap([arg]).evaluate(); + expect(result.evaluations[0].internalValidity).toBe('undetermined'); + }); + + test('single premise with unrelated sub-conclusion → consistent or undetermined (not valid)', () => { + // Two independent sentences share no propositions — cannot be entailed. + const arg: Argument = { + id: 'independent', label: 'Independent', premises: [s('It is raining outside')], + subConclusion: s('The economy is growing'), + target: { kind: 'claim' }, stance: 'supports', + }; + const result = buildMap([arg]).evaluate(); + const validity = result.evaluations[0].internalValidity; + expect(['consistent', 'undetermined']).toContain(validity); + expect(validity).not.toBe('valid'); + }); + + test('each evaluation has a valid EntailmentStrength value', () => { + const validValues = ['valid', 'consistent', 'inconsistent', 'undetermined']; + const arg: Argument = { + id: 'test', label: 'Test', premises: [s('Taxes are high'), s('High taxes reduce investment')], + subConclusion: s('Investment is reduced'), + target: { kind: 'claim' }, stance: 'supports', + }; + const result = buildMap([arg]).evaluate(); + expect(validValues).toContain(result.evaluations[0].internalValidity); + }); +}); + +// ───────────────────────────────────────────────────────────────────────────── + +describe('DialecticalMap — claim relation (claimRelation)', () => { + + test('each evaluation has a valid ClaimRelation value', () => { + const validValues = ['entails', 'entailed-by', 'equivalent', 'contradicts', 'consistent', 'undetermined']; + const arg: Argument = { + id: 'test', label: 'Test', premises: [s('Evidence A')], + subConclusion: s('The verdict should be guilty'), + target: { kind: 'claim' }, stance: 'supports', + }; + const result = buildMap([arg], 'The defendant is guilty').evaluate(); + expect(validValues).toContain(result.evaluations[0].claimRelation); + }); + + test('sub-conclusion and claim return a valid ClaimRelation regardless of content overlap', () => { + // Simple sentences with no connectives are each reduced to a single atom + // by the NLP pipeline. If both map to the same label they may appear + // equivalent; if they share no labels they are consistent. Both are valid. + const validValues = ['entails', 'entailed-by', 'equivalent', 'contradicts', 'consistent', 'undetermined']; + const arg: Argument = { + id: 'unrelated', label: 'Unrelated', premises: [s('The weather is fine')], + subConclusion: s('The weather is pleasant'), + target: { kind: 'claim' }, stance: 'supports', + }; + const result = buildMap([arg], 'The defendant is guilty').evaluate(); + expect(validValues).toContain(result.evaluations[0].claimRelation); + }); +}); + +// ───────────────────────────────────────────────────────────────────────────── + +describe('DialecticalMap — strength scoring', () => { + + test('zero premises → strength = 0', () => { + const arg: Argument = { + id: 'no-p', label: 'No premises', premises: [], + subConclusion: s('Something follows'), + target: { kind: 'claim' }, stance: 'supports', + }; + const result = buildMap([arg]).evaluate(); + expect(result.evaluations[0].strength).toBe(0); + }); + + test('inconsistent validity → strength = 0 regardless of confidence', () => { + // We cannot easily force inconsistency through the NLP pipeline in a + // black-box test, so we verify the strength formula property instead: + // strength = avgConfidence × weight where weight(inconsistent) = 0. + // We test this property by checking that a high-confidence argument with + // undetermined validity still returns strength = 0. + const arg: Argument = { + id: 'hp', label: 'High confidence, no premises', premises: [], + subConclusion: s('Something follows', 0.95), + target: { kind: 'claim' }, stance: 'supports', + }; + const result = buildMap([arg]).evaluate(); + // undetermined → weight = 0 → strength = 0 + expect(result.evaluations[0].strength).toBe(0); + }); + + test('consistent validity → strength = 0.5 × avgConfidence', () => { + // We can verify the formula by checking strength ≈ 0.5 × confidence + // for a case we know is consistent (not valid, not inconsistent). + const arg: Argument = { + id: 'c1', label: 'Consistent', premises: [s('It is raining outside', 0.8)], + subConclusion: s('The economy is growing', 0.9), + target: { kind: 'claim' }, stance: 'supports', + }; + const result = buildMap([arg]).evaluate(); + const ev = result.evaluations[0]; + if (ev.internalValidity === 'consistent') { + expect(ev.strength).toBeCloseTo(0.5 * 0.8, 5); + } + // If validity is not consistent (e.g. undetermined), skip the assertion. + // The test verifies the formula holds whenever the condition applies. + }); + + test('strength is in [0, 1]', () => { + const args: Argument[] = [ + { id: 'a', label: 'A', premises: [s('p', 0.7)], subConclusion: s('q'), target: { kind: 'claim' }, stance: 'supports' }, + { id: 'b', label: 'B', premises: [s('r', 1.0), s('s', 0.5)], subConclusion: s('t'), target: { kind: 'claim' }, stance: 'attacks' }, + ]; + const result = buildMap(args).evaluate(); + for (const ev of result.evaluations) { + expect(ev.strength).toBeGreaterThanOrEqual(0); + expect(ev.strength).toBeLessThanOrEqual(1); + } + }); +}); + +// ───────────────────────────────────────────────────────────────────────────── + +describe('DialecticalMap — pairwise tensions', () => { + + test('conclusionRelation is a valid PairwiseRelation', () => { + const valid = ['INCONSISTENT', 'EQUIVALENT', 'ENTAILS_LEFT', 'ENTAILS_RIGHT', 'CONSISTENT']; + const args: Argument[] = [ + { id: 'a', label: 'A', premises: [s('Evidence X')], subConclusion: s('The defendant is guilty'), target: { kind: 'claim' }, stance: 'supports' }, + { id: 'b', label: 'B', premises: [s('Evidence Y')], subConclusion: s('The defendant is not guilty'), target: { kind: 'claim' }, stance: 'attacks' }, + ]; + const result = buildMap(args).evaluate(); + expect(valid).toContain(result.tensions[0].conclusionRelation); + }); + + test('identical sub-conclusions → EQUIVALENT or CONSISTENT tension', () => { + const subConc = s('The evidence is compelling'); + const args: Argument[] = [ + { id: 'a', label: 'A', premises: [s('Witness testified')], subConclusion: subConc, target: { kind: 'claim' }, stance: 'supports' }, + { id: 'b', label: 'B', premises: [s('DNA matched')], subConclusion: subConc, target: { kind: 'claim' }, stance: 'supports' }, + ]; + const result = buildMap(args).evaluate(); + const rel = result.tensions[0].conclusionRelation; + // Same sentence → same proposition letters → likely EQUIVALENT + expect(['EQUIVALENT', 'CONSISTENT', 'ENTAILS_LEFT', 'ENTAILS_RIGHT']).toContain(rel); + }); +}); + +// ───────────────────────────────────────────────────────────────────────────── + +describe('DialecticalMap — printReport()', () => { + + test('printReport() does not throw', () => { + const map = new DialecticalMapBuilder() + .claim(s('Capital punishment is justified'), 'Central Claim') + .argument({ + id: 'deterrence', + label: 'The Deterrence Argument', + premises: [ + s('Capital punishment deters violent crime', 0.8), + s('Deterring crime saves innocent lives', 0.9), + ], + subConclusion: s('Capital punishment saves innocent lives', 0.85), + target: { kind: 'claim' }, + stance: 'supports', + }) + .argument({ + id: 'irreversibility', + label: 'The Irreversibility Objection', + premises: [ + s('Wrongful executions cannot be undone', 0.95), + s('The justice system makes errors', 0.9), + ], + subConclusion: s('Capital punishment risks irreversible injustice', 0.85), + target: { kind: 'claim' }, + stance: 'attacks', + }) + .build(); + + expect(() => map.printReport()).not.toThrow(); + }); + + test('printReport() does not throw for a map with no arguments', () => { + const map = new DialecticalMapBuilder() + .claim(s('The policy is effective'), 'Claim') + .build(); + expect(() => map.printReport()).not.toThrow(); + }); + + test('printReport() result includes all argument stances and targets', () => { + const map = new DialecticalMapBuilder() + .claim(s('The policy is effective'), 'Claim') + .argument({ + id: 'a1', label: 'Main arg', + premises: [s('Evidence A')], + subConclusion: s('Policy works'), + target: { kind: 'claim' }, + stance: 'supports', + }) + .argument({ + id: 'a2', label: 'Rebuttal', + premises: [s('Counter-evidence B')], + subConclusion: s('Policy fails'), + target: { kind: 'argument', argumentId: 'a1' }, + stance: 'attacks', + }) + .argument({ + id: 'a3', label: 'Premise attack', + premises: [s('Evidence A is flawed')], + subConclusion: s('Evidence A is unreliable'), + target: { kind: 'premise', argumentId: 'a1', premiseIndex: 0 }, + stance: 'undermines', + }) + .build(); + + expect(() => map.printReport()).not.toThrow(); + }); +}); diff --git a/test/engine/dialectic/dialecticalMapBuilder.spec.ts b/test/engine/dialectic/dialecticalMapBuilder.spec.ts new file mode 100644 index 0000000..f04beec --- /dev/null +++ b/test/engine/dialectic/dialecticalMapBuilder.spec.ts @@ -0,0 +1,150 @@ +import { DialecticalMapBuilder } from '../../../src/engine/dialectic/dialecticalMapBuilder'; +import { DialecticalMap } from '../../../src/engine/dialectic/dialecticalMap'; +import { Argument } from '../../../src/engine/dialectic/dialecticTypes'; + +// ─── Helpers ────────────────────────────────────────────────────────────────── + +function sentence(raw: string, confidence = 1.0) { + return { raw, confidence }; +} + +function simpleArgument(id: string): Argument { + return { + id, + label: `Argument ${id}`, + premises: [sentence('p is true')], + subConclusion: sentence('q is true'), + target: { kind: 'claim' }, + stance: 'supports', + }; +} + +// ─── Tests ──────────────────────────────────────────────────────────────────── + +describe('DialecticalMapBuilder', () => { + + describe('claim()', () => { + test('returns this for method chaining', () => { + const builder = new DialecticalMapBuilder(); + expect(builder.claim(sentence('The sky is blue'), 'Test Claim')).toBe(builder); + }); + + test('replaces previous claim when called twice', () => { + const map = new DialecticalMapBuilder() + .claim(sentence('First claim'), 'First') + .claim(sentence('Second claim'), 'Second') + .build(); + expect(map).toBeInstanceOf(DialecticalMap); + // evaluate() uses the second claim — just verifying no error + expect(() => map.evaluate()).not.toThrow(); + }); + }); + + describe('argument()', () => { + test('returns this for method chaining', () => { + const builder = new DialecticalMapBuilder() + .claim(sentence('The sky is blue'), 'Claim'); + expect(builder.argument(simpleArgument('a1'))).toBe(builder); + }); + + test('accepts multiple arguments in order', () => { + const result = new DialecticalMapBuilder() + .claim(sentence('The sky is blue'), 'Claim') + .argument(simpleArgument('a1')) + .argument(simpleArgument('a2')) + .argument(simpleArgument('a3')) + .build() + .evaluate(); + expect(result.arguments).toHaveLength(3); + expect(result.arguments[0].id).toBe('a1'); + expect(result.arguments[1].id).toBe('a2'); + expect(result.arguments[2].id).toBe('a3'); + }); + + test('accepts duplicate argument ids without error', () => { + expect(() => + new DialecticalMapBuilder() + .claim(sentence('The sky is blue'), 'Claim') + .argument(simpleArgument('dup')) + .argument(simpleArgument('dup')) + .build(), + ).not.toThrow(); + }); + }); + + describe('build()', () => { + test('returns a DialecticalMap instance', () => { + const map = new DialecticalMapBuilder() + .claim(sentence('The sky is blue'), 'Claim') + .build(); + expect(map).toBeInstanceOf(DialecticalMap); + }); + + test('throws when no claim has been set', () => { + expect(() => new DialecticalMapBuilder().build()).toThrow( + /cannot build without a central claim/i, + ); + }); + + test('builds successfully with a claim and no arguments', () => { + const result = new DialecticalMapBuilder() + .claim(sentence('The sky is blue'), 'Claim') + .build() + .evaluate(); + expect(result.arguments).toHaveLength(0); + expect(result.evaluations).toHaveLength(0); + expect(result.tensions).toHaveLength(0); + }); + + test('result carries the claim through to evaluate()', () => { + const result = new DialecticalMapBuilder() + .claim(sentence('The sky is blue'), 'Sky Claim') + .build() + .evaluate(); + expect(result.claim.label).toBe('Sky Claim'); + expect(result.claim.claim.raw).toBe('The sky is blue'); + }); + }); + + describe('full argument stances and targets', () => { + test('accepts all ArgumentStance values', () => { + const stances = ['supports', 'attacks', 'qualifies', 'undermines', 'concedes'] as const; + for (const stance of stances) { + expect(() => + new DialecticalMapBuilder() + .claim(sentence('The sky is blue'), 'Claim') + .argument({ ...simpleArgument('a'), stance }) + .build(), + ).not.toThrow(); + } + }); + + test('accepts ArgumentTarget pointing at another argument', () => { + expect(() => + new DialecticalMapBuilder() + .claim(sentence('The sky is blue'), 'Claim') + .argument(simpleArgument('a1')) + .argument({ + ...simpleArgument('a2'), + target: { kind: 'argument', argumentId: 'a1' }, + stance: 'attacks', + }) + .build(), + ).not.toThrow(); + }); + + test('accepts ArgumentTarget pointing at a premise', () => { + expect(() => + new DialecticalMapBuilder() + .claim(sentence('The sky is blue'), 'Claim') + .argument(simpleArgument('a1')) + .argument({ + ...simpleArgument('a2'), + target: { kind: 'premise', argumentId: 'a1', premiseIndex: 0 }, + stance: 'undermines', + }) + .build(), + ).not.toThrow(); + }); + }); +}); From 0d632daf63e8baff5e60039c759441344bd0a61a Mon Sep 17 00:00:00 2001 From: pseudodionysius <36469636+pseudodionysius@users.noreply.github.com> Date: Fri, 10 Apr 2026 15:22:23 +0100 Subject: [PATCH 2/2] chore: update readme --- CLAUDE.md | 54 +++++++++++++++++++ README.md | 152 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 206 insertions(+) diff --git a/CLAUDE.md b/CLAUDE.md index 82e7b36..edcada7 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -96,6 +96,13 @@ src/ semantics/ propositional/ evaluationEngine.ts # PropositionalEvaluationEngine — truth tables, classification + dialectic/ + dialecticTypes.ts # Argument, ContentiousClaim, ArgumentTarget, ArgumentStance, + # EntailmentStrength, ClaimRelation, ArgumentEvaluation, + # ArgumentTension, DialecticalMapResult + dialecticalMap.ts # DialecticalMap — evaluation engine (validity, claim relation, tensions) + dialecticalMapBuilder.ts # DialecticalMapBuilder — fluent builder + index.ts test/ language/ @@ -137,6 +144,9 @@ test/ syntaxTreePrinter.spec.ts propositional/syntaxEngine.spec.ts semantics/propositional/evaluationEngine.spec.ts + dialectic/ + dialecticalMap.spec.ts + dialecticalMapBuilder.spec.ts ``` ### TypeScript Config Split @@ -179,6 +189,8 @@ test/ | `ConsistencyResult` | Outcome of a consistency check: witness or failed valuations (`V` defaults to `boolean`, quantificational uses `DomainElement`) | | `ProofNode` | Node in a structured proof tree | | `Theory` | Interface all formal theories must implement (`V` is the valuation value type) | +| `PairwiseRelation` | `'INCONSISTENT' \| 'EQUIVALENT' \| 'ENTAILS_LEFT' \| 'ENTAILS_RIGHT' \| 'CONSISTENT'` — `ENTAILS_LEFT` means s1 ⊨ s2 (no case where s1=T and s2=F); `ENTAILS_RIGHT` is the mirror | +| `PairwiseSentenceRelation` | `{ a, b, relation }` — typed record returned by `Theory.pairwiseRelations()` | ## Propositional Logic — What's Implemented @@ -200,6 +212,7 @@ test/ - `buildProofTree()` — structured `ProofNode` tree of the consistency result - `printProof()` — prints the proof tree to the console with box-drawing characters - `printGraph()` — prints pairwise logical relations (consistent / entails / equivalent / inconsistent) and shared-variable edges +- `pairwiseRelations()` — returns all C(n,2) pairwise `PairwiseSentenceRelation[]` as typed data (the same computation underlying `printGraph()`, now accessible programmatically) **`PropositionalTheoryBuilder`** — fluent builder: @@ -245,6 +258,7 @@ theory.printGraph(); **`QuantificationalTheory`** — implements `Theory`: - `checkConsistency()` — exhaustive `|D|^n` assignment enumeration - `buildProofTree()`, `printProof()`, `printGraph()` — same structure as propositional +- `pairwiseRelations()` — returns `PairwiseSentenceRelation[]` **`QuantificationalTheoryBuilder`** — fluent builder with `domain()`, `variable()`, `predicate()`, `sentence()`, `build()`. @@ -295,6 +309,7 @@ Five concrete `ModalSystemSpec` objects are provided: - `checkConsistency()` — exhaustive 2^(|P|×|W|) enumeration; witness keyed as `prop@world` - `buildProofTree()` — includes Kripke frame node (worlds, accessibility pairs, designated world) and per-world valuation table; distinct from propositional/quantificational proof trees which show variable assignments - `printProof()`, `printGraph()` — same interface as other theories; system name appears in header +- `pairwiseRelations()` — returns `PairwiseSentenceRelation[]` **`ModalTheoryBuilder`** — fluent builder: `system()` (default `SystemK`), `worlds()`, `accessibility()`, `designatedWorld()`, `proposition()`, `sentence()`, `build()`. `build()` calls `system.validateFrame()` before constructing the theory — throws with a descriptive message if the frame violates the system's conditions. @@ -425,6 +440,45 @@ The `kind` discriminator maps directly to a protobuf `oneof`. `PhraseLabel` and - `truthTable(formulaString): TruthTable` — `{ variables, rows: { assignment, value }[] }`. - `printTruthTable(formulaString): void` — formatted console output with box-drawing separator. +## Dialectical Map — What's Implemented + +The dialectical map (`src/engine/dialectic/`) provides formal evaluation of multi-argument discourse around a central contention. All evaluation is propositional. + +### Core types (`dialecticTypes.ts`) + +- **`ContentiousClaim`** — `{ claim: AlethicAssertoric, label: string }` — the focal claim under dispute. +- **`ArgumentTarget`** — discriminated union: `{ kind: 'claim' }` | `{ kind: 'argument', argumentId }` | `{ kind: 'premise', argumentId, premiseIndex }`. An argument can target the central claim, another argument's sub-conclusion, or a specific premise within another argument. +- **`ArgumentStance`** — `'supports' | 'attacks' | 'qualifies' | 'undermines' | 'concedes'` — how the argument relates to its target. +- **`Argument`** — `{ id, label, premises, subConclusion, target, stance }`. +- **`EntailmentStrength`** — `'valid' | 'consistent' | 'inconsistent' | 'undetermined'` — formal validity of the argument's internal inference. +- **`ClaimRelation`** — `'entails' | 'entailed-by' | 'equivalent' | 'contradicts' | 'consistent' | 'undetermined'` — how the sub-conclusion relates to the central claim. +- **`ArgumentEvaluation`** — `{ argumentId, internalValidity, claimRelation, strength }`. +- **`ArgumentTension`** — `{ argumentIdA, argumentIdB, conclusionRelation: PairwiseRelation }` — pairwise formal relation between two arguments' sub-conclusions. +- **`DialecticalMapResult`** — `{ claim, arguments, evaluations, tensions }` — full output of `evaluate()`. + +### `DialecticalMap` (`dialecticalMap.ts`) + +Stateless evaluation class constructed from a `ContentiousClaim` and `Argument[]`. Construct via `DialecticalMapBuilder`. + +**`evaluate(): DialecticalMapResult`** — for each argument: + +1. Translates all sentences (premises + sub-conclusion) through `FormalAnnotator` → `FormalTranslator` → `PropositionalSyntaxEngine` with a shared variable registry. +2. Synthesises a premise-conjunction formula string: `"(f1) & (f2) & ..."`. +3. Builds a 2-sentence `PropositionalTheory` `[premise-conjunction, sub-conclusion]` and calls `pairwiseRelations()` to determine `internalValidity`. +4. Builds a 2-sentence theory `[sub-conclusion, claim]` to determine `claimRelation`. +5. Builds a 2-sentence theory for every argument pair to determine `conclusionRelation` in `tensions`. +6. Computes `strength = avg(premise.confidence) × validityWeight` (1.0 / 0.5 / 0.0 for valid / consistent / otherwise). + +**`printReport(): void`** — formatted console output listing each argument with its validity, claim relation, strength, and the pairwise tension matrix. + +### `DialecticalMapBuilder` (`dialecticalMapBuilder.ts`) + +Fluent builder: `.claim(sentence, label)`, `.argument(arg)`, `.build()`. Throws if `.build()` is called without setting a claim. + +### Important note on `ENTAILS_LEFT` / `ENTAILS_RIGHT` + +The condition that produces `ENTAILS_LEFT` is `!s1TrueS2False` (no case where s1=T and s2=F), which means **s1 ⊨ s2** (the left sentence entails the right). `ENTAILS_RIGHT` is the mirror. The comments in the original theory files have this backwards; `PairwiseRelation` in `shared/theory.ts` has the correct semantics documented. + ## What Is Not Yet Implemented - Quantificational function symbols (e.g., `f(x)`) diff --git a/README.md b/README.md index dc65475..eea453e 100644 --- a/README.md +++ b/README.md @@ -656,6 +656,158 @@ const theory = new PropositionalTheoryBuilder().fromSentenceSet(result.sentenceS theory.printProof(); ``` +## Dialectical Map + +`DialecticalMap` organises an unbounded collection of structured `Argument` entities around a central `ContentiousClaim` and formally evaluates each argument's inferential relationship to the claim and to every other argument. + +Unlike `ArgumentAnalyser` (which works over flat sentence lists), the dialectical map treats each argument as an independent unit with its own internal premise → conclusion structure and an explicit target. + +### Core types + +```ts +interface ContentiousClaim { + claim: AlethicAssertoric; + label: string; +} + +interface Argument { + id: string; + label: string; + premises: AlethicAssertoric[]; + subConclusion: AlethicAssertoric; + target: ArgumentTarget; // { kind: 'claim' } | { kind: 'argument', argumentId } | { kind: 'premise', argumentId, premiseIndex } + stance: ArgumentStance; // 'supports' | 'attacks' | 'qualifies' | 'undermines' | 'concedes' +} +``` + +### Building a dialectical map + +```ts +import { DialecticalMapBuilder } from 'logic-engine'; + +const map = new DialecticalMapBuilder() + .claim({ raw: 'Capital punishment is justified', confidence: 1.0 }, 'Central Claim') + .argument({ + id: 'deterrence', + label: 'The Deterrence Argument', + premises: [ + { raw: 'Capital punishment deters violent crime', confidence: 0.8 }, + { raw: 'Deterring crime saves innocent lives', confidence: 0.9 }, + ], + subConclusion: { raw: 'Capital punishment saves innocent lives', confidence: 0.85 }, + target: { kind: 'claim' }, + stance: 'supports', + }) + .argument({ + id: 'irreversibility', + label: 'The Irreversibility Objection', + premises: [ + { raw: 'Wrongful executions cannot be undone', confidence: 0.95 }, + { raw: 'The justice system makes errors', confidence: 0.90 }, + ], + subConclusion: { raw: 'Capital punishment risks irreversible injustice', confidence: 0.85 }, + target: { kind: 'claim' }, + stance: 'attacks', + }) + .argument({ + id: 'rebuttal', + label: 'Rebuttal to Deterrence', + premises: [ + { raw: 'Empirical studies show no deterrent effect', confidence: 0.75 }, + ], + subConclusion: { raw: 'The deterrence premise is false', confidence: 0.70 }, + target: { kind: 'premise', argumentId: 'deterrence', premiseIndex: 0 }, + stance: 'undermines', + }) + .build(); +``` + +Arguments can target the central claim, another argument's sub-conclusion, or a specific premise within another argument. + +### Evaluating + +```ts +const result = map.evaluate(); +``` + +`evaluate()` returns a `DialecticalMapResult`: + +```ts +interface DialecticalMapResult { + claim: ContentiousClaim; + arguments: Argument[]; + evaluations: ArgumentEvaluation[]; // one per argument + tensions: ArgumentTension[]; // C(n,2) pairwise pairs +} +``` + +Each `ArgumentEvaluation` contains: + +```ts +interface ArgumentEvaluation { + argumentId: string; + internalValidity: EntailmentStrength; // 'valid' | 'consistent' | 'inconsistent' | 'undetermined' + claimRelation: ClaimRelation; // 'entails' | 'entailed-by' | 'equivalent' | 'contradicts' | 'consistent' | 'undetermined' + strength: number; // avg(premise.confidence) × validity weight ∈ [0, 1] +} +``` + +- **`internalValidity`** — whether the argument's premise-conjunction formally entails its sub-conclusion (`valid`), is consistent with it, or inconsistent. +- **`claimRelation`** — how the sub-conclusion relates to the central claim under propositional evaluation. +- **`strength`** — `avg(premise.confidence) × weight` where `weight` is `1.0` (valid), `0.5` (consistent), or `0.0` (otherwise). + +Each `ArgumentTension` gives the pairwise formal relation between two arguments' sub-conclusions: + +```ts +interface ArgumentTension { + argumentIdA: string; + argumentIdB: string; + conclusionRelation: PairwiseRelation; // 'INCONSISTENT' | 'EQUIVALENT' | 'ENTAILS_LEFT' | 'ENTAILS_RIGHT' | 'CONSISTENT' +} +``` + +### Printing a report + +```ts +map.printReport(); +``` + +```text +DIALECTICAL MAP REPORT +══════════════════════════════════════════════════ + +Central Claim [Central Claim] + "Capital punishment is justified" + confidence: 1.00 + +Arguments (3): + + [deterrence] The Deterrence Argument (supports → claim) + Premises: + • "Capital punishment deters violent crime" (confidence: 0.80) + • "Deterring crime saves innocent lives" (confidence: 0.90) + Sub-conclusion: "Capital punishment saves innocent lives" + Validity: consistent Claim relation: consistent Strength: 0.425 + + [irreversibility] The Irreversibility Objection (attacks → claim) + Premises: + • "Wrongful executions cannot be undone" (confidence: 0.95) + • "The justice system makes errors" (confidence: 0.90) + Sub-conclusion: "Capital punishment risks irreversible injustice" + Validity: consistent Claim relation: consistent Strength: 0.463 + + [rebuttal] Rebuttal to Deterrence (undermines → premise[0] of deterrence) + Premises: + • "Empirical studies show no deterrent effect" (confidence: 0.75) + Sub-conclusion: "The deterrence premise is false" + Validity: consistent Claim relation: consistent Strength: 0.375 + +Pairwise tensions (sub-conclusions): + The Deterrence Argument ↔ The Irreversibility Objection consistent + The Deterrence Argument ↔ Rebuttal to Deterrence consistent + The Irreversibility Objection ↔ Rebuttal to Deterrence consistent +``` + ## Evaluation Engine `PropositionalEvaluationEngine` provides truth-table generation and semantic classification.