[−][src]Trait pocket_prover::Prove
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
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.
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
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
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>
a: A,
b: B
) -> Option<f64>
Computes the logical probability P(b | a ∧ rules)
.
Implementors
impl<T> Prove for T where
T: Copy + Construct + ExtendRules,
[src]
T: Copy + Construct + ExtendRules,