「‍」 Lingenic

Commitment Logic

(⤓.md ≡ ◇.md); γ ≜ [2026-07-17T135416.643, 2026-10-22T054143.488] ∧ |γ| = 3

Commitment Logic

Origin. Hamblin (1970) introduced commitment stores into formal dialectic, replacing an account of dialogue in terms of what speakers believe with one in terms of what they have publicly undertaken. Walton and Krabbe (1995) built the systematic theory, classifying dialogue types — persuasion, negotiation, inquiry, deliberation, information-seeking, eristic — and giving each its own commitment rules. Singh (1998) and Fornara and Colombetti (2002) carried the idea into multi-agent systems in response to a specific problem: the mentalistic semantics of KQML and FIPA-ACL define a message by the sender's beliefs and intentions, which no observer can check.

Models. A commitment is a social relation rather than a mental state: a debtor is committed to a creditor for a condition. It is created, discharged, cancelled or released by public acts, so its status is observable and compliance is decidable by a third party. Dialogue state is the commitment store, a public record updated by moves; the rules of a dialogue game say which moves are permitted given the store and which commitments a move incurs. Conditional commitments carry the contractual structure, the antecedent detaching the consequent.

Formalism.

Commitment: C(x, y, p): x committed to y that p. Social fact. Public record. Cancellable.

Operations: Create(x, y, p): x commits to y that p. Cancel(x, y, p): x withdraws commitment. Discharge: p becomes true.

Commitment store: CS: set of active commitments. Updated by moves. Public record. Dialogue state.

Conditional commitment: CC(x, y, p, q): if p then C(x, y, q). Triggers on antecedent. Contractual.

Dialogue rules: Permissible moves given CS. Obligations from commitments. Violation conditions.

Assertion: Assert(x, p) creates C(x, H, p). H = hearer(s). Commitment to defend.

Challenge: Challenge(y, p) challenges C(x, H, p). Requires defense. Dialogue obligation.

Singh's operations: Create, Discharge, Cancel, Release, Delegate, Assign. Delegate: change the debtor. Assign: change the creditor.

Lifecycle: null → conditional (CC created) detached: antecedent holds, becomes C satisfied: consequent brought about violated: consequent fails while active cancelled by debtor; released by creditor expired: antecedent never holds

Agent communication: ACL semantics via commitments. Observable, verifiable. Social rather than mental.

Example: Merchant m, customer c. CC(m, c, paid, delivered). c pays: detach to C(m, c, delivered). m delivers: discharged. m does not: violated — read off the store, no mental state consulted.

Symbols.

SymbolUnicodeNameMeaning
CU+0043Latin capital letter C / CommitmentC(x, y, p) : x is committed to y for p
→U+2192Rightwards arrow / TransitionStep in the commitment lifecycle
(U+0028Left parenthesisOpens an argument list
)U+0029Right parenthesisCloses an argument list
,U+002CCommaSeparates arguments
xU+0078Latin small letter x / DebtorAgent who undertakes the commitment
yU+0079Latin small letter y / CreditorAgent to whom it is owed
pU+0070Latin small letter pContent, or antecedent of a conditional commitment
qU+0071Latin small letter qConsequent of a conditional commitment
HU+0048Latin capital letter H / HearerAddressee made creditor by an assertion
CC—Conditional commitmentCC(x, y, p, q) : if p, then x is committed to y for q
CS—Commitment storePublic set of active commitments
Create—OperationBrings a commitment into being
Discharge—OperationContent is brought about; commitment satisfied
Cancel—OperationDebtor withdraws
Release—OperationCreditor frees the debtor
Delegate—OperationTransfers the debtor role
Assign—OperationTransfers the creditor role
Assert—Dialogue moveCreates a commitment to defend the content
Challenge—Dialogue moveRequires the debtor to defend a commitment

Metatheory. The case for commitments rests on a negative result about the alternative: Wooldridge (2000) argued that the mentalistic semantics of KQML and FIPA-ACL, which fix the meaning of a speech act by the sender's beliefs and intentions, cannot support any verification that an agent conforms to the language, since those states are not observable and the corresponding program-verification problem is not in general solvable. Commitment semantics were adopted because conformance becomes a property of the public store instead. Singh's repertoire — create, discharge, cancel, release, delegate, assign — induces a lifecycle that is a finite automaton, which is what makes monitoring decidable, and Yolum and Singh (2002) gave commitment protocols an operational semantics in the event calculus, so that execution becomes planning and runs no state machine anticipated remain checkable against the commitments they discharge. Extensions of branching-time logic with commitment modalities have been reduced to ordinary CTL model checking, making finite-state protocols verifiable with existing tools. Chopra and Singh (2009) isolated commitment alignment: two agents can hold divergent views of the same store, so agreement must be established rather than assumed.

Applies to. Multi-agent systems. Dialogue. Contracts. Agent communication.

Limitations. This is a family rather than one formalism — Walton and Krabbe's dialectical commitments, Singh's social commitments, the event-calculus and branching-time renderings differ on which operations exist and on what a violation amounts to, so a protocol written in one is not directly a protocol in another. The theory records that a commitment was made but says nothing about when cancellation is legitimate: no principle separates a permitted withdrawal from a breach except further commitments stipulated by hand, and that regress has no fixed point inside the formalism. Commitments about commitments are expressible only by nesting, which the operational accounts restrict or forbid. The public store is an idealization, since agents observe messages rather than the store and their views can diverge. Nothing in the framework enforces anything: a violation is recorded, and sanction lies outside the logic.

© 2026 Lingenic LLC