Signed Formula

logic

Definition

Signed Formula

A signed formula is a pair $(S,A)$ where $S\in \{t,f\}$ is a sign and $A$ is a formula. The sign $t$ indicates that $A$ is true; the sign $f$ indicates that $A$ is false.

Signed formulas are used in the semantic tableau method to track truth-value assignments during the decomposition of complex formulas.

Signs

Signs

• $t$ — the formula is true
• $f$ — the formula is false

A signed formula $t:A$ asserts that $A$ holds under some interpretation. A signed formula $f:A$ asserts that $A$ does not hold.