pocket_prover 0.18.0

A fast, brute force, automatic theorem prover for first order logic
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14

use pocket_prover::*;

fn main() {
    println!("Path semantics: {}", measure(1, || prove!(&mut |a, b, c, d| {
        imply(
            and!(
                ps_core(a, b, c, d),
                imply(a, c),
                imply(b, d)
            ),
            imply(qual(a, b), qual(c, d))
        )
    })));
}