[−][src]Trait pocket_prover::Prove

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> { ... }
}

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.

ⓘThis example is not tested
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

fn count<F: Fn(Self) -> u64>(f: F) -> u64

A method to count true statements.

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

Loading content...

Provided methods

fn prove<F: Fn(Self) -> u64>(f: F) -> bool

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.

fn does_not_mean<F: Fn(Self) -> u64, G: Fn(Self) -> u64>(
    assumption: F,
    conclusion: G
) -> bool

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

fn means<F: Fn(Self) -> u64, G: Fn(Self) -> u64>(
    assumption: F,
    conclusion: G
) -> bool

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

fn eq<F: Fn(Self) -> u64, G: Fn(Self) -> u64>(a: F, b: G) -> bool

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

fn exc<F: Fn(Self) -> u64, G: Fn(Self) -> u64>(a: F, b: G) -> bool

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

fn imply<F: Fn(Self) -> u64, G: Fn(Self) -> u64>(a: F, b: G) -> bool

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

fn prob<F: Fn(Self) -> u64>(f: F) -> Option<f64>

Computes the logical probability P(f | rules).

fn prob_imply<A: Fn(Self) -> u64 + Copy, B: Fn(Self) -> u64>(
    a: A,
    b: B
) -> Option<f64>

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

Loading content...

Implementors

impl<T> Prove for T where
    T: Copy + Construct + ExtendRules, [src]

Loading content...