stalmarck 0.1.0

A crate implementing Stålmarck's method for efficiently proving propositional logic formulas and verifying logical validity.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

//! Proves a distributive law valid and prints the solver counters.

use stalmarck::{Config, Formula, ProofResult, Solver};

fn main() {
    let (a, b, c) = (Formula::var("a"), Formula::var("b"), Formula::var("c"));
    // (a ∧ b) ∨ (a ∧ c) → a ∧ (b ∨ c) needs one Dilemma level.
    let f = ((a.clone() & b.clone()) | (a.clone() & c.clone()))
        .implies(a & (b | c));

    for depth in 0..=1 {
        let solver =
            Solver::new(Config { max_depth: depth, ..Config::default() });
        let report = solver.prove(&f);
        let verdict = match &report.result {
            ProofResult::Valid => "valid".to_string(),
            ProofResult::Invalid(m) => format!("invalid, counter-model {m:?}"),
            ProofResult::Unknown(u) => format!("unknown ({u:?})"),
        };
        println!("depth {depth}: {f} is {verdict}");
        println!("  {:?}", report.stats);
    }
}