Module tableaux_solver

Propositional formula satisfiability solver using the Propositional Tableaux method.

Re-exports

pub use tableau::Tableau;

pub use theory::Theory;

Modules

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 PropositionalFormulas, which corresponds to a branch in a tableau tree.

Enums

ExpansionKind

Result of expansion using various rules.

Functions

is_satisfiable

Checks if the given propositional formula is satisfiable.

is_valid

Checks if a given propositional formula is valid.