Trait pocket_prover::Prove

source · [−]
pub trait Prove: Sized + Copy {
    fn count<F: Fn(Self) -> u64>(f: F) -> u64;

    fn prove<F: Fn(Self) -> u64>(f: F) -> bool { ... }
    fn does_not_mean<F: Fn(Self) -> u64, G: Fn(Self) -> u64>(
        assumption: F,
        conclusion: G
    ) -> bool { ... }
    fn means<F: Fn(Self) -> u64, G: Fn(Self) -> u64>(
        assumption: F,
        conclusion: G
    ) -> bool { ... }
    fn eq<F: Fn(Self) -> u64, G: Fn(Self) -> u64>(a: F, b: G) -> bool { ... }
    fn exc<F: Fn(Self) -> u64, G: Fn(Self) -> u64>(a: F, b: G) -> bool { ... }
    fn imply<F: Fn(Self) -> u64, G: Fn(Self) -> u64>(a: F, b: G) -> bool { ... }
    fn prob<F: Fn(Self) -> u64>(f: F) -> Option<f64> { ... }
    fn prob_imply<A: Fn(Self) -> u64 + Copy, B: Fn(Self) -> u64>(
        a: A,
        b: B
    ) -> Option<f64> { ... }
}
Expand description

Implemented by provable systems of logic.

This trait is used by other crates in the PocketProver ecosystem named pocket_prover-<name>.

A common pattern is create logical systems that can be combined into new systems. For example, a base system Foo is extended by Bar<Foo>. However, Bar<()> might be used independently reasoning only about its own rules.

ⓘ
pub struct Foo<T = ()> {
    pub bar: T,
    pub a: u64,
    pub b: u64,
    pub c: u64,
}

impl ::std::ops::Deref for Foo<Bar> {
    type Target = Bar;
    fn deref(&self) -> &Bar {&self.bar}
}

impl Prove for Foo { ... }
impl Prove for Foo<Bar> { ... }

Pro tip: Use the Construct and ExtendRules trait to auto impl this trait. For base logical systems, implement the BaseSystem trait to auto impl this trait.

Required Methods

A method to count true statements.

Counts imply(<system>, f) since this permits deriving all other methods automatically.

Provided Methods

A method to prove a statement according to the rules.

The default method counts true cases and might be overridden for better performance. One can compute the number of true cases faster by using 1 << bits.

According to the rules, the assumption does not lead to the conclusion, but neither does it lead to the opposite conclusion.

According to the rules, the conclusion follows from the assumptions, but the assumptions can not be used to get the opposite conclusion.

Proves that according to the rules, two statements are equivalent.

Proves that according to the rules, two statements are exclusive.

Proves that according to the rules, the first statement implies the other.

Computes the logical probability P(f | rules).

Computes the logical probability P(b | a ∧ rules).

Implementors