proof checking for avatar

[abentkamp]

The checking of the split rule usually fails.

[c-cube]

It's actually hard to do because we'd need to check the equisatisfiability of the split clause with all the resulting clauses. (it's esa, because technically the boolean atoms are like new symbols). If you split a ∨ b into [a] or [b], a <= [a], b <= [b] it's only the conjunction of these that is provable from a ∨ b…

[abentkamp]

I thought we might want to interpret the clause a <= [a] as "a implies a", which is a tautology. Then the split would be easy. It's just that the merge in the end needs to know about the clause that was split.

Edit: Actually, the final merge isn't problematic either. We just need to translate ϕ <= [ψ] as ϕ ∨ ¬ ψ.