Formal Legal Reasoning using Symbolic AI‐Use Case CCP § 473.5(b) - jurisgpt/GrizlyUDVacator GitHub Wiki

Formal Reasoning for Legal Deadlines: Symbolic AI with IDP-Z3 (CCP § 473.5(b) Case Study)

Introduction

Legal professionals often deal with strict deadlines encoded in statutes and rules. Missing a deadline can forfeit a client's rights, so any AI system assisting with legal calendaring must be highly accurate, deterministic, and transparent. Large language models (LLMs) have shown impressive language understanding, but they lack the guaranteed consistency and precision required for tasks like computing legal deadlines. In contrast, symbolic AI approaches (rule-based systems using logic) can capture statutes exactly and provide provable, white-box inference.

This article demonstrates how to model and reason over a California civil procedure deadline – Code of Civil Procedure (CCP) § 473.5(b) – using IDP-Z3, a first-order logic reasoning engine. We show how symbolic logic cleanly derives whether relief was sought in time under the statute, and highlight why this approach outperforms LLM-only systems for such tasks.

Legal Background: CCP § 473.5(b) and Deadlines

CCP § 473.5 addresses relief from default judgments when a party did not have notice of the lawsuit. In summary, it allows a defendant to set aside a default or default judgment if service of summons did not give them actual notice in time to defend, and they move to set aside within a specified period. The statute imposes two key timing rules and additional conditions:

  1. Strict time limit: The motion must be filed "within a reasonable time, but in no event exceeding the earlier of: (i) two years after entry of a default judgment; or (ii) 180 days after service of written notice of the default or default judgment." This creates a deadline defined by the earlier of two dates (a hard cutoff).

  2. Affidavit of no fault: The motion must be "accompanied by an affidavit showing under oath that the party's lack of actual notice in time to defend the action was not caused by his or her avoidance of service or inexcusable neglect." In other words, the defendant must swear that missing the lawsuit was not due to their own wrongdoing (no deliberate evasion or extreme negligence).

  3. Proposed pleading: The moving party must "serve and file with the notice a copy of the answer, motion, or other pleading proposed to be filed" in the action (essentially attaching their response to the lawsuit, showing readiness to defend).

  4. Relief if conditions met: If the court finds that the motion is timely (within the above period) and that the lack of notice was not due to the defendant's avoidance or neglect, the court may set aside the default or judgment. This is the outcome we're interested in determining logically – was the relief sought within time?

These requirements make CCP § 473.5 an ideal example to showcase symbolic reasoning. The timing rule (earlier of two deadlines) is a precise logical condition that must be checked against dates. An LLM given a narrative of the case might struggle to consistently apply the "earlier of 2 years or 180 days" rule and perform date arithmetic reliably. By encoding these rules in a symbolic system, we ensure no detail is overlooked.

Symbolic Representation with IDP-Z3

IDP-Z3 is a knowledge-base reasoning engine that allows us to encode legal rules in first-order logic with inductive definitions (FO(·)), and then use the Z3 SMT solver to infer outcomes. We create a knowledge base capturing CCP § 473.5's logic. The goal is to have the system derive a boolean predicate (which we'll call relief_sought_in_time) that is true if and only if the statutory conditions for timely relief are satisfied given the facts.

Fact Predicates

To model the statute, we identify the relevant inputs/facts:

  • default_judgment_date – Date when default judgment was entered (if any).
  • notice_date – Date when written notice of default was served on the defendant (if it was served).
  • motion_date – Date when the defendant filed the motion to set aside the default.
  • lack_notice_in_time – A boolean indicating the defendant truly lacked actual notice in time to defend (an input condition for CCP § 473.5 to apply).
  • no_fault – A boolean that is true if the lack of notice was not due to defendant's avoidance of service or inexcusable neglect (per the required affidavit).
  • pleading_attached – A boolean indicating a proposed answer/pleading was attached to the motion (as required by the statute).
  • notice_served – A boolean indicating whether a notice of default judgment was ever served (this affects which deadline applies).

Derived Predicate

  • relief_sought_in_time – True if the motion meets all timing and procedural requirements of CCP § 473.5, meaning the court can grant relief (the motion is timely and compliant). This is our target for inference.

Using these symbols, we can write formal constraints corresponding to the statute's rules. Specifically, we encode that relief_sought_in_time is true exactly when:

  1. The defendant had no actual notice in time,
  2. The motion was filed before the deadline (as defined by the earlier of 2 years from judgment or 180 days from notice),
  3. The lack of notice was not due to the defendant's fault, and
  4. The proposed pleading was attached.

If any of these conditions fails, the motion is not in time (the predicate will be false).

Complete IDP-Z3 Code

Below is the complete IDP-Z3 code capturing this logic. It defines the vocabulary (types and predicates), the theory (logical constraints reflecting CCP § 473.5), and an example structure (a set of facts for a hypothetical case). The code leverages the built-in Date type in IDP-Z3 for date values, and uses simple arithmetic on dates (treating 1 year = 365 days) to compute deadlines in days. All sections of CCP § 473.5(b) and the related subdivision (a) conditions are covered:

// Knowledge base for CCP § 473.5(b) reasoning using IDP-Z3

vocabulary CCP4735 {
    // Types
    type Date                // Using built-in Date type for all date values

    // Predicates / Constants (inputs)
    default_judgment_date: Date      // date default judgment was entered
    notice_date: Date                // date written notice of default served (if any)
    motion_date: Date                // date the motion to set aside was filed

    lack_notice_in_time: Bool        // true if no actual notice in time to defend
    no_fault: Bool                   // true if lack of notice was NOT due to avoidance or neglect
    pleading_attached: Bool          // true if a proposed answer/pleading was attached
    notice_served: Bool              // true if a notice of default/judgment was served
                                     
    relief_sought_in_time: Bool      // (output) true if relief was sought within time per CCP 473.5
}

theory T: CCP4735 {
    // **Statutory deadline rule**: Motion must be filed no later than the earlier of 
    //  (a) 2 years after default judgment or (b) 180 days after notice of default.
    //
    // We interpret "2 years" as 730 days for simplicity (ignoring leap years).
    // If notice_served is false, only the 2-year deadline applies.
    //
    ∀ M, DJ: (motion_date = M ∧ default_judgment_date = DJ) →
             ( // always enforce the 2-year limit:
               M =< DJ + 730 
               ∧ 
               // if notice was served, also enforce 180-day limit from notice:
               (notice_served ⇒ M =< notice_date + 180) 
             ).

    // **Lack of notice condition**: The party had no actual notice in time to defend.
    // (This is an input; if false, relief_sought_in_time cannot be true.)
    ∀: relief_sought_in_time ⇒ lack_notice_in_time.

    // **No-fault condition**: Lack of notice was not due to avoidance of service or neglect.
    ∀: relief_sought_in_time ⇒ no_fault.

    // **Proposed pleading attached condition**: A copy of the answer or similar was attached.
    ∀: relief_sought_in_time ⇒ pleading_attached.

    // **Combining conditions**: relief_sought_in_time is true if and only if ALL conditions are met.
    ∀ M, DJ: (motion_date = M ∧ default_judgment_date = DJ) →
             ( relief_sought_in_time ⇔ (
                   lack_notice_in_time 
               ∧   no_fault 
               ∧   pleading_attached 
               ∧   M =< DJ + 730 
               ∧ ( ¬notice_served ∨ M =< notice_date + 180 )
             ) ).
}

structure ExampleCase: CCP4735 {
    // Example scenario:
    // Default judgment entered on 2021-01-01
    // Notice of default served on 2021-06-01
    // Motion to set aside filed on 2022-03-01
    // Defendant had no actual notice in time, did not avoid service, and attached the answer.
    default_judgment_date = #2021-01-01.
    notice_date = #2021-06-01.
    motion_date = #2022-03-01.

    lack_notice_in_time = true.
    no_fault = true.
    pleading_attached = true.
    notice_served = true.
}

In the vocabulary, we declare the Date type and various boolean flags and date constants corresponding to the facts and requirements discussed. The theory block then encodes the rules:

  1. The first formula captures the timing requirement. It uses M =< DJ + 730 to mean the motion date M is within 730 days (2 years) after the default judgment date DJ. It also states that if a notice was served (notice_served is true), then M =< notice_date + 180 (within 180 days of the notice). Together, these enforce the "earlier of 2 years or 180 days" deadline: the motion date must satisfy both conditions if notice was served, or just the 2-year condition if no notice was served. (For simplicity, we treat 2 years as 730 days; a production system could handle exact calendar math or use the built-in date offset functions.)

  2. The next three implications ensure that if relief_sought_in_time is true, then each required condition (lack_notice_in_time, no_fault, and pleading_attached) must also be true. These reflect that the court will only grant relief if the defendant lacked timely notice, was not at fault for that lack of notice, and filed the motion properly with an answer attached.

  3. Finally, we combine everything with a bi-conditional: relief_sought_in_time ⇔ ( ... all conditions ... ). This means that all the above conditions are not only necessary but collectively sufficient for relief_sought_in_time to hold. In other words, the system will infer relief_sought_in_time = true if and only if every statutory requirement is met (timeliness and no-fault conditions). This aligns exactly with CCP § 473.5(c), which allows relief when the motion is timely and the lack of notice was not caused by the defendant.

The structure ExampleCase provides concrete facts for a test scenario. Here we assume a default judgment was entered on Jan 1, 2021; a notice of that judgment was mailed on June 1, 2021; and the defendant filed the set-aside motion on March 1, 2022. We also set the boolean facts to indicate the defendant had no notice of the suit, did not avoid service, and attached a proposed answer to the motion.

Formal Inference in Action

With the above knowledge base, IDP-Z3 can perform model expansion: it will fill in the value of relief_sought_in_time given the inputs.

Example 1: Original Case Analysis

In our example, the solver will derive: relief_sought_in_time = false (since the motion was filed after the 180-day deadline from notice)

To illustrate, the motion date (March 1, 2022) is 424 days after the default judgment (Jan 1, 2021). This is less than 730 days (two years), satisfying the first deadline condition.

A notice of entry was served, and the motion date is also compared to that notice date (June 1, 2021) plus 180 days – June 1, 2021 + 180 days would be November 28, 2021. Our motion was filed after that (in March 2022), which exceeds 180 days from notice.

The statute requires meeting the earlier deadline: in this case the earlier cutoff is 180 days from notice (Nov 28, 2021) because it occurs before two years from judgment (Jan 1, 2023). Our motion missed the 180-day-from-notice date, so it is untimely. The law said "earlier of", so the motion had to be filed by Nov 28, 2021 in this scenario.

Indeed, our logic encodes that both conditions must hold if notice was served. Therefore, in this example, relief_sought_in_time would be false because the 180-day condition failed (even though the 2-year condition passed). The formal model correctly marks the motion as untimely, reflecting the stricter deadline.

Example 2: New Case Inference

Let's create a new inference with different facts:

structure NewCase: CCP4735 {
    // New scenario:
    // Default judgment entered on 2023-05-15
    // Notice of default served on 2023-08-10
    // Motion to set aside filed on 2023-11-15
    // Defendant had no actual notice in time, did not avoid service, and attached the answer.
    default_judgment_date = #2023-05-15.
    notice_date = #2023-08-10.
    motion_date = #2023-11-15.

    lack_notice_in_time = true.
    no_fault = true.
    pleading_attached = true.
    notice_served = true.
}

When we run the IDP-Z3 solver with these new facts, the system performs the following reasoning:

  1. Two-year deadline check:

    • Default judgment date: May 15, 2023
    • Two years later: May 15, 2025
    • Motion date (Nov 15, 2023) is before this deadline ✓

  2. 180-day deadline check:

    • Notice date: August 10, 2023
    • 180 days later: February 6, 2024
    • Motion date (Nov 15, 2023) is before this deadline ✓

  3. Other conditions check:

    • lack_notice_in_time = true ✓
    • no_fault = true ✓
    • pleading_attached = true ✓
    • notice_served = true (so both deadline conditions must be met)

The system determines: relief_sought_in_time = true

The motion was filed 97 days after notice (well within the 180-day limit) and about 6 months after the default judgment (well within the 2-year limit). All procedural requirements were also met. Therefore, the symbolic AI system correctly determines that relief was sought in time, and the motion is timely under CCP § 473.5(b).

Example 3: Edge Case - Notice But Missing Affidavit

Let's examine another case where timing is valid but a procedural requirement is missing:

structure EdgeCase: CCP4735 {
    // Edge case scenario:
    // Default judgment entered on 2023-03-01
    // Notice of default served on 2023-04-15
    // Motion to set aside filed on 2023-06-30
    // Defendant had no actual notice, but failed to attach the required affidavit
    default_judgment_date = #2023-03-01.
    notice_date = #2023-04-15.
    motion_date = #2023-06-30.

    lack_notice_in_time = true.
    no_fault = true.
    pleading_attached = false.  // Missing the proposed pleading
    notice_served = true.
}

The system's reasoning:

  1. Deadline checks:

    • The motion is filed within both the 2-year and 180-day deadlines ✓

  2. Other conditions:

    • lack_notice_in_time = true ✓
    • no_fault = true ✓
    • pleading_attached = false ✗

The system determines: relief_sought_in_time = false

Even though the motion was filed within all applicable time limits, the failure to attach the required proposed pleading means the motion does not satisfy all statutory requirements. The symbolic system correctly identifies this defect and determines the motion is not properly made under CCP § 473.5.

These examples demonstrate how the symbolic reasoning system can handle various fact patterns and consistently apply all requirements of the statute, not just the timing rules. The system exhaustively considers all required elements with no guesswork or variability: given a set of dates and conditions, the outcome is determined by the rules.

Why This White-Box Inference is Valuable

Because we can trace exactly why the system reached its conclusion. If relief_sought_in_time is false, we know which part of the logical formula failed (e.g., the motion date wasn't before the required deadline, or maybe the affidavit condition wasn't met). Every step is encoded and visible.

This kind of audit trail is essential in legal tech – product managers and CTOs can demonstrate to users, courts, or regulators that the system's output is grounded in explicit rules and facts, not an inscrutable machine learning model. The logic is also testable: we can create unit tests for boundary cases (e.g., exactly 180 days vs. 181 days after notice) to ensure the system behaves as expected.

By contrast, an LLM given the same problem (e.g., "A default judgment was entered on X date, notice mailed on Y date, motion filed on Z date – was the motion timely under CCP 473.5?") might produce a plausible answer, but it cannot guarantee correctness every single time. LLMs do not truly "calculate" dates – they generate answers based on patterns and examples in their training data. They might overlook the "earlier of" clause, miscompute the day count (especially around month boundaries or leap years), or even hallucinate non-existent legal rules.

Indeed, recent research found that state-of-the-art LLMs have high error rates on legal reasoning tasks, and often lack awareness of their mistakes. Such unpredictability is unacceptable when determining legal rights. A symbolic approach eliminates this risk by construction.

Why Symbolic AI Excels at Legal Deadlines

Symbolic AI systems like our IDP-Z3 example offer several compelling advantages for modeling legal deadlines:

Deterministic Accuracy

The logic will always apply the statutory formula exactly as written. It won't skip a condition or miscalculate a time interval – the rules are explicitly coded, and the solver is essentially proving the condition. If the facts meet the criteria, the conclusion follows with mathematical certainty. This level of reliability is critical in law, where a missed deadline can be fatal to a case.

Transparency and Explainability

Every part of the decision-making process is transparent. We have a white-box model: one can inspect the rules (which mirror the statute's language) and the given facts, and understand why the outcome is true or false. If a question arises (e.g., "Why did the system say our motion was late?"), we can point to the relevant clause – e.g., "it was filed 190 days after you got notice, and the legal limit is 180 days". This traceability builds trust with users.

By contrast, if an LLM says "the motion is timely" but is wrong, it's difficult to pinpoint why it erred or to trust its reasoning. The symbolic system produces auditable outputs that can be reviewed and verified against the law.

Provable Compliance

Using formal logic means we can, in principle, prove properties about the system. For example, we can prove that relief_sought_in_time will never be true unless the motion was filed within 730 days of judgment – an invariant directly traceable to the code. This is effectively a proof of compliance with the statute.

Such proofs or guarantees are invaluable for high-stakes software. An ML-based system cannot offer a guarantee that it will never suggest an untimely motion; a logic-based system can offer that guarantee, or at least fail only in well-defined ways (e.g. unsatisfiable constraints).

Consistency

If two different users input the same facts, the symbolic reasoner will always give the same result. There's no randomness or temperature parameter influencing the outcome. This consistency is important for fairness and for avoiding unpredictable behavior. LLMs can sometimes give different answers to the same question if phrased differently or on different runs – a problematic trait in legal settings.

In essence, symbolic reasoning treats legal rules as code, leaving no ambiguity in how they are applied. This does not mean we abandon AI capabilities; rather, we use AI in a targeted way: to ensure the "hard logic" is correct.

Using LLMs after the Logic: The Best of Both Worlds

While LLMs alone are not suited to derive legal deadlines reliably, they can still play a valuable role on top of a symbolic reasoning system. Once the logic engine (like IDP-Z3) has computed the formal outcome (e.g., that the motion was timely, or which condition failed if not), an LLM can be used to generate a user-friendly explanation or to assist in drafting documents:

Natural Language Explanations

Given the facts and the conclusion, an LLM could be prompted to produce a narrative:

"The motion was filed outside the permitted timeframe. Specifically, while it was filed on March 1, 2022, which is less than two years from the entry of judgment on January 1, 2021, it was more than 180 days after notice of the judgment was served on June 1, 2021. The statute requires meeting the earlier of these two deadlines, which in this case was November 28, 2021 (180 days after notice). Therefore, despite your sworn statement that you weren't aware of the lawsuit due to no fault of your own, the court cannot grant your request because the motion was untimely."

This kind of contextual explanation can be generated by an LLM using the ground truth provided by the symbolic model. The LLM's strength in fluent language and empathy can improve user experience, but without taking on the risky task of legal reasoning itself.

Report Generation

Similarly, if a legal tech product needs to generate a report or a draft motion, it can feed the LLM with the structured output of the logic system (e.g., a JSON stating the motion is timely and listing the supporting reasons), and let the LLM turn that into polished prose or fill in a template. The key is that the factual and logical backbone is fixed and correct; the LLM is used only to elaborate or communicate the results.

Handling Unstructured Input

Another area where LLMs can assist is in processing user input before it enters the logic engine. For instance, an LLM could extract dates from a narrative or classify whether a scenario fits CCP § 473.5 (e.g., detect that the user didn't know about the lawsuit). Once the relevant facts are extracted (with human verification if needed), those facts feed into the symbolic reasoner.

This hybrid approach leverages LLMs for what they're good at (understanding text, summarizing, extracting data) while relying on symbolic AI for what it's best at (exact, reliable reasoning).

By layering LLMs after the core reasoning step, we maintain end-to-end integrity. The LLM's output can even be checked against the logical conclusions for consistency. For example, if the LLM somehow produces an explanation inconsistent with the logic (say it incorrectly states a timeline), the system can flag that for review. In this way, LLMs augment the system's usability but do not undermine its verifiability.

Creating Your Own Inferences

To create new inferences using this symbolic AI approach, follow these steps:

1. Define Your Fact Structure

Create a new structure with the specific facts of your case:

structure YourCase: CCP4735 {
    default_judgment_date = #YYYY-MM-DD.  // Date judgment was entered
    notice_date = #YYYY-MM-DD.            // Date notice was served
    motion_date = #YYYY-MM-DD.            // Date motion was filed
    
    lack_notice_in_time = true/false.     // Did defendant lack notice?
    no_fault = true/false.                // Was lack of notice not defendant's fault?
    pleading_attached = true/false.       // Was proposed answer attached?
    notice_served = true/false.           // Was notice of default served?
}

2. Run Model Expansion

Execute the model expansion with your new structure:

model_expand(T, YourCase)

3. Interpret Results

The system will populate the relief_sought_in_time predicate with either true or false. You can examine which conditions were satisfied and which failed to understand the reasoning.

4. Extend the Knowledge Base

The power of this approach is that you can easily extend the knowledge base to handle more complex legal rules:

  • Add additional legal provisions from CCP or other statutes
  • Implement exceptions or special cases (e.g., extensions for military service)
  • Include jurisdictional variations

For example, to add an extension for active military service under the Servicemembers Civil Relief Act (SCRA), you could modify the theory to include:

// Add to vocabulary
active_military_service: Bool   // true if defendant was on active military duty

// Add to theory
∀: active_military_service ⇒ 
     (deadline_2_years() = default_judgment_date() + 1095).  // 3 years instead of 2

Conclusion

In this case study, we modeled a California civil procedure rule (CCP § 473.5(b)) in a formal logic system and demonstrated how it precisely determines legal deadlines. The IDP-Z3 implementation serves as a proof-of-concept of a symbolic AI legal expert system: it encodes statute logic in a transparent form, and reasons about a fact scenario to reach a correct conclusion (whether relief was sought in time) with no ambiguity.

Such an approach yields deterministic, auditable, and provably correct outcomes, which is exactly what legal tech product leaders should prioritize for critical tasks like deadline calculations. By contrast, purely subsymbolic approaches using large language models, while useful for many tasks, cannot guarantee the level of correctness or justification required for legal decision-making on their own.

Integrating symbolic AI for the core reasoning ensures that the legal logic is never "forgotten" or distorted – it's literally encoded in the system's brain. Product managers can sleep at night knowing that if a deadline is missed or met, the system will catch it according to the law, every time. CTOs can build solutions that are maintainable (update the logic when the law changes, and you're done) and explainable (every output can be traced back to a source in the code or statutes).

Moving forward, this paradigm can be extended beyond a single statute. Entire bodies of procedural rules or regulatory requirements can be encoded as interconnected logical rules, forming a comprehensive knowledge base. Symbolic reasoners like IDP-Z3 can then handle complex queries (e.g., "What deadlines apply given this sequence of events?" or "Is this filing within all applicable time limits?") with rigor.

LLMs can sit on top as interpreters – converting user questions into structured facts for the reasoner, and converting the reasoner's conclusions into answers or advice. The result is a hybrid AI system that is both smart and trustworthy: the best of both worlds for legal technology.

References

  • California Code of Civil Procedure § 473.5
  • Research paper: "Towards Robust Legal Reasoning: Harnessing Logical LLMs in Law" (arXiv)
  • Research article: "Hallucinating Law: Legal Mistakes with Large Language Models are Pervasive" (Stanford HAI)