[][src]Function libprop_sat_solver::tableaux_solver::is_valid

pub fn is_valid(formula: &PropositionalFormula) -> bool

Checks if a given propositional formula is valid.

This is done by checking that the contrapositive statement: "is -<formula> unsatisfiable?"