Skip to main content

normalize_proof

Function normalize_proof 

Source
pub fn normalize_proof(proof: &Proof) -> Proof
Expand description

Normalize a proof by reordering axioms alphabetically and renumbering nodes.

This creates a canonical representation of the proof that is independent of the order in which axioms and inferences were added.

§Arguments

  • proof - The proof to normalize

§Returns

A normalized proof with axioms in alphabetical order

§Example

use oxiz_proof::proof::Proof;
use oxiz_proof::normalize::normalize_proof;

let mut proof = Proof::new();
proof.add_axiom("q");
proof.add_axiom("p");
proof.add_axiom("r");

let normalized = normalize_proof(&proof);
// Axioms will be in order: p, q, r