We present a formalization of the proof of the correspondence between cumulative non-monotonic reasoning and System C in a proof assistant. Reasoning based on System C is the cornerstone of non-monotonic reasoning and was given a semantics via cumulative models by Kraus, Lehmann and Magidor. Our proof is inspired by the original proof and written in the proof system Rocq and focuses on propositional logic. Due to the features of Rocq, the proof implicitly yields a verified implementation of System C reasoning.
Let Σ = {, , , . . .} be a finite set of propositional atoms, and let ℒ be a propositional language over Σ (including implication and bi-implication). The set of propositional interpretations over Σ is denoted by Ω and |= is the usual model relation. The set of models of is denoted by Mod() . Classical propositional entailment is denoted by |= and is defined by |= if Mod() ⊆ Mod().
Any relation |∼ ⊆ ℒ × ℒ will be denoted here as a consequence relation. A central notion
for consequence relations is monotonicity, stating that if |∼ , then also ∧ |∼ . The
propositional entailment relation |= from above satisfies monotonicity. Consequence relations that
violate monotonicity are denoted as non-monotonic. In the seminal work by Gabbay [
∧ |∼ |= ↔ |∼ |∼ (Ref) |∼ (Reflexivity) (CM) (Cautious Monotonicity) (RW) |= → |∼ (Right Weakening) (LLE) (Left Logical Equivalence) |∼ (Cut) ∧ |∼ |∼
|∼ (Ref) is a basic property of consequence relations. (LLE) ensures that consequences respect classical equivalence, (RW) provides classical conclusions, (Cut) provides plausible conclusions, and (CM) is a restricted form of monotonicity. The System C postulates are widely accepted as the minimal requirements for good rational non-monotonic reasoning. A consequence relation |∼ is called cumulative if System C is satisfied by |∼ . When we axiomatically claim that a consequence |∼ should hold, we call |∼ a conditional assertion. For a set of conditional assertions K, we write K |= |∼ if there is a proof for |∼ via the System C when assuming the assertions in K. For every cumulative consequence relation |∼, there is a set K that gives rise to |∼.
In the following, we present a general semantic approach to System C that goes back to Kraus,
Lehmann and Magidor [
Reasoning over O is then implemented by considering only minimal elements with respect to ≺ . For a strict partial order ≺ ⊆ × on a set and a subset ⊆ , an element ∈ is called minimal in with respect to ≺ if for each ∈ holds ̸≺ . Then, min(, ≺) is the set of all ∈ that are minimal in with respect to ≺ . In the context of a state-order model, we let () = { ∈ | ℓ() ⊆ Mod()} . Definition 1. For a state-order model O = ⟨, ℓ, ≺⟩, we let |∼ O if min((), ≺) ⊆ ().
To fully capture cumulative reasoning, one has to guarantee that minimal elements exist. A set ⊆ is called smooth with respect to ≺ if for all ∈ , either ∈ min(, ≺) or there exist ∈ min(, ≺) such that ≺ . We say a relation ≺ is smooth if () is smooth for all formulas ∈ ℒ.
Definition 2. A cumulative model is a state-order model W = ⟨, ℓ, ≺⟩ where ≺ is smooth.
Note that in the context of this paper, where we restrict our investigations to propositional logic, it is
suficient to consider only cumulative models where is finite [
Kraus, Lehmann and Magidor establish a fundamental correspondence between cumulative
consequence relations and consequence relations based on cumulative models [
Theorem 1 ([
In the following, we give an outline of the proof of Theorem 1 by Kraus, Lehmann and Magidor. [Soundness.] The soundness direction proves that cumulative models satisfy all System C rules. The proof treats each System C postulate individually, with particular attention to Cut and Cautious Monotonicity. For Cut, if all minimal elements of () satisfy and all minimal elements of ( ∧ ) satisfy , then any minimal element of () satisfies and therefore ∧ . Since it is minimal in () and ( ∧ ) ⊆ () , it is also minimal in ( ∧ ) . For Cautious Monotonicity, assume |∼ W and |∼ W , then prove ∧ |∼ W . Take any state minimal in ( ∧ ) ; since ∈ () , by the smoothness condition, either is minimal in () or there exists ′ minimal in () such that ′ ≺ . If ′ exists, then ′ |= (by |∼ W ), so ′ ∈ () ∩ () , making ′ ∈ ( ∧ ) , contradicting the minimality of . Therefore, is minimal in (), and since |∼ W , we conclude |= . [Completeness.] The completeness direction constructs a canonical model based on the cumulative consequence relation |∼ that induces the same consequence relation. A model ∈ Mod() of is normal for if for all ∈ with |∼ holds |= . For two formulas and , we write ∼ if |∼ and |∼ . The canonical model W = (, ℓ, ≺) for |∼ is defined by:
= ℒ/ ∼ ℓ([] ∼ ) = { ∈ Ω | is normal for } (states are ∼ equivalence classes)
(labels are all normal world) [] ∼ ≺ [] ∼ if [] ∼ ̸= [] ∼ and there is ∈ [] ∼ with |∼ The proof is then by showing two central insights: (A) A normal world for satisfies if and only if |∼ . (B) For every formula , the state []
∼ is the unique minimal element in min((), ≺).
Because of (B) and ℓ([] ∼ ) = { ∈ Ω | is normal for } , it holds |∼ W if and only if all normal worlds for satisfy . Because of (A), the latter is equivalent to stating that |∼ holds. In summary, we obtain that |∼ if and only if |∼ W .
Rocq is an interactive theorem prover based on the Calculus of Inductive Constructions (CIC) [
The fundamental principle of interactive proving consists of a dialogue between a human and a machine. Proofs are constructed step-by-step using tactics, which are commands that transform proof goals. The proof state consists of a context (available hypotheses and definitions) and goals (statements to be proven). Common tactics essential for our formalization include: • intros: Introduces hypotheses and variables from implications and quantifications • apply: Applies existing theorems or hypotheses to transform goals • induction: Performs structural induction over inductively defined types • destruct: Performs case analysis on data structures or logical connectives • split: Splits conjunctive goals into separate subgoals • unfold: Expands definitions to reveal underlying structure This interactive approach provides significant advantages over both manual proofs and fully automatic systems. Manual proofs may contain errors or use implicit assumptions, while automatic provers often fail on complex problems and provide little insight when they do fail. Interactive proving ensures absolute correctness while maintaining human control over proof strategies.
Here we present our implementations of cumulative reasoning and reasoning based on cumulative
models in Rocq. Instead of implementing propositional logic, we use an existing library by Dakai Guo
and Wensheng Yu [
Cumulative consequences are based on finite inferences via System C from some set of conditional assertions K. We define conditional assertions as formula pairs through ConditionalAssertion and use InKB to check membership in knowledge bases. Cumulative consequences K |= |∼ are implemented as an application of the System C rules as derivation steps in the following type CumulCons:
The type CumulCons takes four parameters. First, KnowledgeBase K that contains the conditional assertions, an Ensemble Formula Γ , which represents a set of formulas, and formulas p and q representing premise and conclusion. The return type Prop indicates that this is a logical property. The set of formulas Γ is here for technical reasons, and it is meant to explicitly represent the valid formulas of propositional logic. Lines 3-4 implement Ref through universal quantification, using parameter p twice for reflexivity. Lines 5-8 define LLE with line 6 requiring the equivalence of formulas and line 7 using recursive CumulCons calls. The RW constructor (lines 9-12) follows a similar structure, but with implication instead of equivalence. Both Cut (lines 13-16) and CM (lines 17-20) use two recursive premises, where Cut removes conjunctions from premises while Cautious Monotonicity introduces them. Lines 21-23 implement a query to the set of conditional assertions K. Our implementation also employs Rocq’s ability to introduce intuitive notation for better readability:
Notation "K ⊕ Γ ⊢ p |∼ q" := (CumulCons K Γ p q) (at level 80).
For formalizing cumulative models (Definition 1), we use a record type, which provides advantages over separate definitions or inductive types through bundled related components with automatic projection:
For the states States (line 2), we define them as abstract Type, which allows us to instantiate them with arbitrary objects (as the original definition). The function Labeling (line 3) represents a direct mapping of the labeling function from the KLM definition, where State (defined in line 7) is a function that assigns truth values to formulas. This represents a functional implementation, giving each state directly an interpretation function. The implemented labeling function is also adapted to propositional logic and simplified, since each world corresponds exactly to one truth value assignment. The preference relation PreferenceRel (line 4) is implemented as a binary relation of type Prop. The record type initially contains no restrictions in the definition – properties like the smoothness condition are formulated later as separate axioms, maintaining separation between structures and properties for modular proof construction.
For formalizing minimal elements, we additionally introduce the definition of MinimalElements: Definition MinimalElements (model : CumulModel) (formula : Formula) : Ensemble (States model) := fun state => entails (Labeling model state) formula /\ ~ exists state’, entails (Labeling model state’) formula /\
PreferenceRel model state’ state. With forall state (line 3), we ensure that the inference relation must hold in all minimal states, and with the implication (line 4), we ensure that only minimal states are considered. In Lines 7-8, we define a short notation for semantic consequence relations in cumulative models.
The function MinimalElements (lines 1-2) implements min((), ≺) as a function with parameters model and formula, returning an ensemble of states (a set of states). The implementation first checks that the formula holds in the state (line 4), and second, that no preferred state exists in which the formula also holds (lines 5-7). This corresponds directly to the mathematical definition given in Section 2.
We implementing consequences |∼ W from a cumulative model W as function SemanticEntails. For that, we employ the implementation MinimalElements for checking whether a conclusion conclusion holds in all minimal states from premise premise:
Definition SemanticEntails (model : CumulModel) (premise conclusion : Formula) : Prop := forall state, In (States model) (MinimalElements model premise) state -> entails (Labeling model state) conclusion.
Notation "model : premise |w∼ conclusion" := (SemanticEntails model premise conclusion) (at level 80).
Since we consider only finite logical languages, it is suficient to consider finite cumulative models [
In (States model) (MinimalElements model formula) minimal_state.
As a premise, we set with entails (line 2) that the formula holds in the current state. Then we declare the existence of a minimal state via the existential quantifier (line 3). We construct the properties of the minimal state: ensuring the formula also holds in the minimal state (line 4), the disjunction (lines 5-6) stating the minimal state is preferred or identical to the original state, and finally (line 6) that this minimal state is an element of MinimalElements for the given formula.
In this section, we present our formalization of Theorem 1 in Rocq. The implementation of the final theorem is given in the following:
Line 4-9 state the theorem, and the remaining lines represent the proof, which is separated into subproofs for soundness and completeness. In the remainder of this section, we present the implementation of these proofs.
The soundness proof shows that all consequence relations that a cumulative model induces satisfy System C. This proof is formalized as a named soundness_klm, which calls subproofs for each System C rule. We implement a separate lemma for each rule of System C that proves that semantic consequences satisfy the corresponding postulate. Due to space limitations, we consider here only the implementation of some System C properties.
The lemma soundness_reflexivity shows that each consequence relation induced from a cumulative model satisfies reflexivity (Ref). Technically, (Ref) holds if a formula holds in all minimal states of , i.e., min((), ≺) ⊆ () . In our Rocq formalization, this corresponds to the statement model : formula |∼w formula.
Lemma soundness_reflexivity : forall (model : CumulModel) (formula : Formula),
// SemanticEntails model premise conclusion
Lines 1-3 claim that reflexivity is satisfied by |∼ W , while lines 4-8 develop the corresponding proof. The proof starts by making the components of the goals available to the prover by unfolding definitions. In Line 5, we unfold the definitions of “ model : formula |∼ formula ” (SemanticEntails) from Line 3 and then unfold MinimalElements (which appears implicitly by unfolding SemanticEntails). In Line 6, we fill the variables in unfolded definitions with elements from our assumption provided in Line 2. We obtain a proof goal entails (Labeling model state) formula, which corresponds to stating that the minimal states of formula in the cumulative model satisfy formula. With exact H_satisfies tells the prover to check the truth of the last goal by employing unification.
In lemma soundness_RW is for proving satisfaction of Right Weakening (RW). The proof uses the implication property H_imp to directly derive that the conclusion also holds in minimal states. Our proof goal is to show that when model : r |∼w p and p -> q hold, then model : r |∼w q also holds, demonstrating that an implication is preserved in the minimal state for r. 1 Lemma soundness_RW : 2 forall (model : CumulModel) (p q r : Formula), 3 (forall state, entails (Labeling model state) p -> 4 entails (Labeling model state) q) -> 5 model : r |w∼ p -> 6 model : r |w∼ q. 7 Proof. 8 unfold SemanticEntails, MinimalElements. 9 intros model p q r H_imp H_entails state H_minimal. 10 apply H_imp. 11 apply H_entails; assumption. 12 Qed.
We first unfold the definition of SemanticEntails and MinimalElements (line 8). After introducing all necessary variables and hypotheses (line 9), hypothesis H_imp states that p implies q, H_entails is the hypothesis that p typically follows from r, and H_minimal states that state is minimal for r.
Our proof goal is entails (Labeling model state) q. We first apply hypothesis H_imp (line 10) to change our proof goal to entails (Labeling model state) p. We then show that p holds in state by applying hypothesis H_entails to H_minimal (line 11). Since we already have H_minimal that corresponds exactly to this condition, we can directly solve the proof goal with assumption and complete the proof. 5.1.3. Cut Rule The proof for Cut is formalized in lemma soundness_Cut. The challenge here lies in showing that p |∼ r holds when both p |∼ q and p ∧ q |∼ r hold. We want to show that in minimal states where p holds, q also holds, to then prove that r must also hold in these states.
We unfold the definitions of SemanticEntails and MinimalElements (line 7) and introduce variables and hypotheses (lines 8-9). We first assert that q holds in state and prove this by applying hypothesis H_p_entails_q (lines 10-11), showing that in minimal states where p holds, q also holds.
We then apply the conjunction assumption H_conj_entails (line 12), requiring proof that state is minimal for (p ∧ q). We use split (line 13) to split into two subgoals. For the first subgoal, we use lemma entails_conjunction with rewrite (line 14) to resolve the conjunction. For the second subgoal, we prove minimality through contradiction (lines 16-22). From the fact that (p ∧ q) holds in state’, it follows that p also holds in state’, contradicting the assumption that state is minimal for p. This demonstrates a transitivity property of the cumulative consequence relation.
The main soundness theorem combines all individual lemmas through structural induction over the inductive type CumulCons:
Theorem soundness_klm : forall (K : KnowledgeBase) (Γ : Ensemble Formula) (p q : Formula), K ⊕ Γ ⊢ p |∼ q -> K ⊕ Γ |= p |w∼ q.
Proof. intros K Γ p q H_cons. unfold CumulativeModelEntails. intros model H_satisfies. induction H_cons. - apply soundness_reflexivity. - apply soundness_LLE with p. + intros state. unfold SatisfiesKnowledgeBases in H_satisfies. destruct H_satisfies as [_ H_classical].
unfold SatisfiesClassicalKB in H_classical.
After introducing variables and unfolding CumulativeModelEntails (lines 5-7), we use structural induction over H_cons (line 9). This creates five separate proof goals corresponding to each System C rule.
Reflexivity (line 11) directly applies the proven lemma soundness_reflexivity.
LLE (lines 13-22) requires transforming the syntactic equivalence from the universe of reference Γ into semantic equivalence in the model. We extract the equivalence from Γ using SatisfiesClassicalKB (lines 15-16), use the model’s satisfaction to obtain semantic equivalence (line 18), and apply entails_equivalence to convert to the form needed by soundness_LLE (line 20).
RW (lines 24-33) similarly transforms syntactic implication to semantic implication. We extract the implication from Γ (lines 26-27), apply the model’s respect for classical truths in Γ (line 29), and use simpl to simplify the entailment definition (line 31).
Cut and CM (lines 35-41) are simpler since they work purely with cumulative consequence relations without requiring knowledge base transformations. Both apply the corresponding lemmas with their respective induction hypotheses (IHH_cons1 and IHH_cons2).
Base (lines 43-47) handles the crucial new case where conditional assertions are directly used from the knowledge base K. We unfold SatisfiesKnowledgeBases to access the conditional component (line 43), extract SatisfiesConditionalKB (line 45), and directly apply it to the conditional assertion from K (line 46).
This modular approach demonstrates that each System C rule is individually sound, and their combination through structural induction establishes the complete soundness of the system. The theorem proves that syntactic derivability in System C implies semantic validity in all cumulative models respecting the knowledge base.
For formalizing completeness of the KLM theorem, we show that every cumulative consequence relation defined by System C rules is representable by a cumulative model. We prove completeness through contradiction by constructing a canonical model that serves as a counterexample.
The main challenge lies in constructing a canonical model from syntactic information. The proof is
close to the construction given by Kraus, Lehmann and Magidor [
We construct the canonical model using maximal consistent sets as states: 1
Definition CanonicalModel : CumulModel := {|
States := CanonicalStates; Labeling := fun w p => valuemaxf w p;
PreferenceRel := CanonicalPreferenceRel Line 1 defines states as ensembles of formulas (maximal consistent sets). Lines 3-4 implement the preference relation from Definition 3.21 of Kraus, Lehmann and Magidor: 1 is preferred over 2 if there exists a formula that is derivable in 1 but not in 2. Lines 6-11 construct the canonical model using library function valuemaxf for the labeling function.
We introduce several axioms to handle the complexity of the canonical model construction. The key axiom ensures existence of appropriate maximal consistent sets:
Axiom exists_maximal_consistent : forall K Γ p q, ∼ (CumulCons K Γ p q) -> exists w, maximal_consistent_set w /\ Γ ⊆ w /\ p ∈ w /\ ∼ q ∈ w.
Lines 1-5 formalize the existence of maximal consistent sets: if is not derivable from under Γ , then there exists a maximal consistent set containing Γ and but not . This axiom establishes the bridge between syntactic non-derivability and semantic representation, enabling us to construct a counterexample in the main proof.
We also need the axiom canonical_entails to establish semantic interpretation:
Axiom canonical_entails : forall (w : CanonicalStates) (p : Formula), maximal_consistent_set w -> entails (Labeling CanonicalModel w) p <-> p ∈ w.
Lines 1-4 establish that in maximal consistent set , formula holds semantically if and only if is an element of . This connects the semantic interpretation in the canonical model with set membership in maximal consistent sets.
The main completeness theorem demonstrates that semantic validity implies syntactic derivability through contradiction: 14 assert (H_satisfies : 15 SatisfiesKnowledgeBase CanonicalModel K )Γ. 16 apply canonical_satisfies_kbs with (w := w); auto. 18 assert (H_minimal : In CanonicalStates 19 (MinimalElements CanonicalModel p) w). 20 apply minimal_elements_canonical; auto. 22 assert (H_entails_q : 23 entails (Labeling CanonicalModel w) q). 24 apply H_sem; auto. 26 assert (H_q_in_w : q ∈ w). 27 apply canonical_entails; auto. 29 contradiction. 30 Qed.
The proof uses classical logic to case split on whether CumulCons K Γ holds (line 6). If it holds (line 7), we are done. Otherwise (lines 8-24), we construct a maximal consistent set using the axiom exists_maximal_consistent (lines 11-12), which guarantees that contains Γ and but not .
We then show the canonical model satisfies the knowledge base (lines 14-16) and prove is minimal for (lines 18-20). Next, we apply the semantic validity assumption to derive that must hold in (lines 22-23), since is a minimal state where holds and the semantic relation requires to hold in all such states. Using the canonical interpretation, we conclude ∈ (lines 26-27). This directly contradicts the construction of where ∈/ (from line 11), completing the proof by contradiction. The contradiction shows that our assumption ∼CumulCons Γ was false, therefore the syntactic derivability Γ : |∼ must hold.
This completeness proof demonstrates that the canonical model construction provides exactly the counterexample needed to show that every semantically valid inference is syntactically derivable, completing the second direction of the KLM representation theorem.
The formalization of the KLM representation theorem in Rocq demonstrates both the feasibility and challenges of mechanizing complex non-monotonic logical systems. Our approach successfully captures all essential components while revealing important insights about the formal verification of infinite mathematical structures.
The encoding of System C through inductive types proved highly efective, with each rule naturally
represented as a constructor in CumulCons. This design enables structural induction for soundness
proofs and provides clear correspondence to the mathematical definition by Kraus, Lehmann and
Magidor [
Interactive proving with Rocq revealed both the power and limitations of current proof assistants.
Tactics like induction, apply, and destruct enable elegant proof construction, but type errors and
unclear documentation create significant learning barriers. The external library [
The restriction to propositional logic serves multiple purposes: it simplifies the smoothness condition, reduces the complexity of maximal consistent set construction, and focuses attention on the representation theorem’s essential structure. This limitation is strategic rather than fundamental, as the modular design supports future extension to predicate logic. Our completeness proof through canonical model construction follows the approach of Kraus, Lehmann and Magidor while adapting to Rocq’s constructive foundation. The use of maximal consistent sets as states, rather than equivalence classes, reflects practical considerations in formal verification while maintaining mathematical equivalence. The soundness direction proved more straightforward, with each System C rule verified independently through structural induction. The formalization reveals important connections between diferent areas of logic and computer science. The use of inductive types for inference systems, record types for mathematical structures, and axiomatic abstraction for complex constructions provides a methodology applicable to other logical systems.
The representation theorem for cumulative reasoning by Kraus, Lehmann and Magidor [
We have achieved our main goal of creating a complete formalization of the KLM theorem in Rocq. The formalization encompasses all components: System C with its five rules was completely formalized on the syntactic level, while cumulative models with states, labeling functions, and preference relations were defined semantically using maximal consistent sets as states. The soundness proof in theorem soundness_klm demonstrates that every System C derivable consequence is semantically valid, secured through structural induction over CumulCons with separate lemmas for each rule. The completeness proof in theorem completeness_klm shows that every semantically valid consequence is syntactically derivable, using contradiction with a canonical model construction. Both proofs were verified by Rocq, confirming their correctness.
Here, we restrict ourselves to propositional logic, which keeps the complexity manageable while preserving essential aspects of the representation theorem. The modular proof structure facilitates future extensions, and the axiomatization of complex constructions allows for a focus on core concepts without losing theoretical rigor. The formalization provides several key insights reflecting the challenges of mechanizing complex logical systems. The infinite size of the canonical model poses the central challenge, leading to our axioms that circumvent this complexity. We distinguished between theoretically justified axioms and those abstracting complex constructions, enabling focus on the KLM theorem’s core concepts while maintaining formal rigor. The formalization successfully covers the complete KLM theorem with machine-verified correctness for the propositional case. All five System C rules are precisely encoded, cumulative models are formally represented, and the bidirectional equivalence between syntax and semantics is proven. The modular structure enables extensions, while axiomatization keeps the approach accessible.
Researchers in non-monotonic reasoning have explored automated reasoning approaches before.
Related work includes KLMLean and KLMLean 2.0 by Pozzato [
Note that our formalization creates a verified library for KLM-style reasoning that can be extended to other systems and applied to practical AI systems through code extraction. The strategic balance between axiomatic abstraction and constructive proof provides a methodology for similar formalizations, showing how to handle infinite constructions while maintaining focus on core theoretical concepts.
In future work, we aim to formalize more theorems from knowledge representation and reasoning.
The closest theorem to the work here is the representation theorem by KLM for System P, which is an
extension of System P by one additional rule [
∨ |∼
This rule states that if typically follows from both and , then also follows from ∨ . Semantically,
System P requires preferential models with transitive preference relations, unlike System C, which only
involves irreflexivity. The modular approach from this paper allows for the implementation of this
additional rule easily. For that we would add an additional constructor in CumulCons (see Section 4.1:
Many other definitions also require only minor adjustments. A challenge is to implement a semantic
representation of System P. This is by preferential models (which difer from cumulative models). Part
of this challenge is that known canonical constructions for preferential models may produce infinite
objects, even for finite languages [
During the preparation of this work, the authors used Grammarly in order to: Grammar and spelling check, Paraphrase and reword. After using this tool/service, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content.