Module proof_verifier 

Proof Verifier

Verifies serialized proof trees by re-checking each node’s rule application. Uses memoization to avoid re-verifying shared sub-proofs, and detects cycles via an in-progress tracking set during DFS traversal.

Examples

use ipfrs_tensorlogic::proof_verifier::{ProofNode, ProofVerifier, RuleSpec};

let mut verifier = ProofVerifier::new();

// Register an axiom rule (arity = 0, no premises required)
verifier.register_rule(RuleSpec {
    rule_id: "axiom".to_string(),
    head_pattern: "fact:".to_string(),
    arity: 0,
});

// A single axiom node
let nodes = vec![ProofNode {
    node_id: 1,
    rule_id: "axiom".to_string(),
    goal: "fact:alice-is-human".to_string(),
    premise_ids: vec![],
    depth: 0,
}];

let result = verifier.verify(&nodes);
assert!(result.is_valid());
assert_eq!(result.nodes_checked, 1);

Structs

ProofNode

A single node in a serialized proof tree.

ProofVerifier

Verifies serialized proof trees by re-checking each node’s rule application.

RuleSpec

Specification of an inference rule used to validate proof nodes.

VerificationResult

Summary of a completed proof verification pass.

Enums

VerificationError

Errors produced during proof verification.