Struct ProofTrace 

pub struct ProofTrace {
    pub steps: Vec<ProofStep>,
    pub root: u32,
    pub naf_dependent: bool,
    pub cwa_false: bool,
}

Complete proof trace: steps array + root index.

Fields

steps: Vec<ProofStep>

root: u32

naf_dependent: bool

True if any step in this trace used negation-as-failure (CWA assumption). Under open-world semantics, NAF-dependent conclusions would be Unknown. Populated by nibli-reason at trace construction; serialized over the wire.

cwa_false: bool

True if the verdict is a CLOSED-WORLD FALSE: not derivable from the KB (the closed-world assumption), as opposed to a numeric/arithmetic FALSE that was genuinely DECIDED (e.g. 5 dunli 3). A closed-world FALSE is the dual of naf_dependent — under open-world semantics it would be Unknown, not a proof of the negation. Computed by nibli-reason from the verdict (it needs to distinguish FALSE from Unknown, both of which have a non-holding root), so unlike naf_dependent it cannot be recomputed from the steps alone.

Implementations

impl ProofTrace

pub fn has_naf_dependency(&self) -> bool

Returns true if any step in this proof trace used negation-as-failure. A Negation step with holds: true means the inner formula was unprovable and NAF flipped it to True — this is the CWA assumption in action. Under open-world semantics, the same conclusion would be Unknown.

Trait Implementations

impl Clone for ProofTrace

fn clone(&self) -> ProofTrace

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ProofTrace

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for ProofTrace

fn deserialize<__D>( __deserializer: __D, ) -> Result<ProofTrace, <__D as Deserializer<'de>>::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for ProofTrace

fn eq(&self, other: &ProofTrace) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl Serialize for ProofTrace

fn serialize<__S>( &self, __serializer: __S, ) -> Result<<__S as Serializer>::Ok, <__S as Serializer>::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for ProofTrace