Splitting (Propositional Logic)

Definition

Splitting (Propositional Logic)

Splitting is a recursive decision method for the satisfiability of a propositional formula: instead of evaluating a formula directly, it reduces the problem to simpler subproblems by branching on an atom.

For a formula and an atom occurring in , let and be the formulas obtained by replacing every occurrence of by the constant (verum) or (falsum), respectively.

Each branch removes , so repeating the step recursively builds a binary splitting tree whose leaves are constant formulas.

Lemma

Splitting over Atoms

Let be an atom, a formula, and an interpretation. Then

Under , replacing by the constant it takes leaves the truth value of unchanged.

Proof

Suppose . Then and have the same truth value under , so . Applying equivalent replacement with and replaces every occurrence of in by and yields .

Suppose . Then and have the same truth value under , so . Applying equivalent replacement with and yields .

Theorem

Splitting

Let be a formula and an atom. Then

Proof

If satisfies , then satisfies or not. If , the lemma gives , hence ; if , it gives . In either case the matching branch formula is satisfiable.

Assume is satisfiable: some . Since does not occur in , extend to with ; the value of is unchanged, so . Because , the lemma yields , hence . Symmetrically, a satisfying interpretation of extends with .