Module wfs 

Well-Founded Semantics for non-monotone probabilistic programs.

WFS handles programs with cycles through negation using three-valued logic:

• True: definitely derivable
• False: definitely not derivable
• Undefined: in cycle, neither provable nor refutable

Algorithm Overview

The WFS alternating fixed-point algorithm works as follows:

1. Initialize: All atoms start as undefined
2. Loop until fixed point: a. Unfounded set computation: Find atoms that cannot be supported
   • An atom is unfounded if every rule that derives it either:
     • Has a body literal that is known false, or
     • Depends positively on an unfounded atom b. Mark unfounded atoms as false c. Consequence derivation: Find atoms that must be true
   • An atom is a consequence if some rule has:
     • All positive body literals true
     • All negative body literals false d. Mark consequences as true
3. Remaining atoms stay undefined

Gradient Treatment

• True atoms: Normal probability and gradient computation
• False atoms: Probability = 0, gradient = 0
• Undefined atoms: Probability = 0, gradient = 0 (conservative)

This matches ProbLog’s behavior for non-stratified programs.

Integration

WFS is invoked during provenance extraction when a non-monotone SCC is detected. It receives ground rules (after variable substitution) and returns the well-founded model with provenance formulas for true atoms.

Structs

WfsAtom

Ground atom representation for WFS

WfsConfig

Configuration for Well-Founded Semantics evaluation.

WfsContext

Context for WFS evaluation

WfsResult

Result of WFS evaluation for an SCC

WfsRule

A ground rule for WFS evaluation

Enums

TruthValue

Three-valued truth value for WFS

WfsLiteral

A ground literal in a rule body

Functions

evaluate_wfs_rules

Evaluate a non-monotone SCC using Well-Founded Semantics.

evaluate_wfs_with_rules

Evaluate WFS with provided ground rules.