[−][src]Module libprop_sat_solver::tableaux_solver

Propositional formula satisfiability solver using the Propositional Tableaux method.

Re-exports

pub use tableau::Tableau;

pub use theory::Theory;

tableau	A `Tableau` is a collection of `Theory`-ies. This corresponds to the entire propositional tableau tree, where each `Theory` is a branch (from the root node to each leaf).
theory	A `Theory` is a set of alternative `PropositionalFormula`s, which corresponds to a branch in a tableau tree.

Result of expansion using various rules.

is_satisfiable	Checks if the given propositional formula is satisfiable.
is_valid	Checks if a given propositional formula is valid.