Skip to content
Commit de13f421 authored by Christoph Schwering's avatar Christoph Schwering
Browse files

Removed Grounder::PlusSplitNames().

The reasoning behind PlusSplitNames() was the following:

// When a term t only occurs in the form of literals (t = n), (t = x), or
// their duals and negations, then splitting does not necessitate an
// additional name. However, when t is an argument of another term or when
// it occurs in literals of the form (t = t') or its dual or negation, then
// we might need a name for every split.
// Note that in general we really need k plus names. For instance,
// (c = d) is not valid. To see that for k >= 2, splitting needs to consider
// at least 2 <= k names, not just one.

Now that such literals (t = t') do not occur in normalised
formulas anymore, PlusSplitNames() is not necessary anymore.

Removing PlusSplitNames() preserves soundness because such literals
cannot be proven anyway: they don't occur in any setup and we don't
"substitute away" any split terms (as is done in the original semantics
during splitting and as did our ResolveDeterminedTerms()).
(There's one exception of such literals that can be proved: (t = t) is
trivially valid and recognised as such.)
parent e9e90ef9
Loading
Loading
Loading
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment