Special Cases
Satisfiability bijection
Bijection between models of
Ax
and
C
Common use: Skolemization, Vampire style splitting
Vacuous
No models of
Ax
Refutation of
Ax
or CNF(
Ax
)
Common use: Contradictory axioms in a FOF problem
Errors
