unicode_fol_kit.formulas_are_equivalent

unicode_fol_kit.formulas_are_equivalent(formula1, formula2, timeout=10000)

Return True iff formula1 and formula2 are logically equivalent.

Asks Z3 to refute ¬(φ ↔ ψ): the two formulas are equivalent exactly when that negation is unsatisfiable. The arguments are interchangeable (the check is symmetric). Returns False if Z3 finds a model of the negation (the formulas differ) or returns unknown within timeout milliseconds.

Parameters:

• formula1 (Node)

• formula2 (Node)

• timeout (int)

Return type:

bool