Function validate 

pub fn validate<Unbound: Ord + Clone, Bound: Ord + Clone>(
    rules: &[Rule<Unbound, Bound>],
    proof: &[RuleApplication<Bound>],
) -> Result<Valid<Bound>, Invalid>

Check is a proof is well-formed according to a ruleset. Returns the set of assumptions used by the proof and the set of statements those assumptions imply. If all the assumptions are true, and then all the implied claims are true under the provided ruleset.

Validating a proof checks whether the proof is valid, but not whether implied claims are true. Additional steps need to be performed to ensure the proof is true. You can use the following statement to check soundness:

forall assumed, implied, rules, proof:
  if Ok(Valid { assumed, implied }) = validate(rules, proof)
  and all assumed are true
  and all rules are true
  then all implied are true

use rify::{
    prove, validate, Valid,
    Entity::{Bound, Unbound},
    Rule, RuleApplication,
};

// (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome)
let awesome_score_axiom = Rule::create(
    vec![
        // if someone is awesome
        [Unbound("a"), Bound("is"), Bound("awesome"), Bound("default_graph")],
        // and they have some score
        [Unbound("a"), Bound("score"), Unbound("s"), Bound("default_graph")],
    ],
    vec![
        // then they must have an awesome score
        [Unbound("a"), Bound("score"), Bound("awesome"), Bound("default_graph")]
    ],
)?;

let proof = vec![
    // (you is awesome) ∧ (you score unspecified) -> (you score awesome)
    RuleApplication {
        rule_index: 0,
        instantiations: vec!["you", "unspecified"]
    }
];

let Valid { assumed, implied } = validate::<&str, &str>(
    &[awesome_score_axiom],
    &proof,
).map_err(|e| format!("{:?}", e))?;

// Now we know that under the given rules, if all quads in `assumed` are true, then all
// quads in `implied` are also true.