Inadequate Models
Model might not be found even if one exists ... totally incomplete
Evaluation might not be possible in incomplete models
Evaluation in a model might timeout
If no
false
or
not-true
axiom, select a
counter satisfiable
axiom
C =
b
E
1
=
a | b
E
2
=
b => a
E
3
=
(~a & (b | c)) | (a & ~b & ~c)
E
4
=
b | (a <=> c)
Negated conjecture =
~b
Selected set
Model
False
N-T
CSA
1
{ }
{~b}
-
-
E
1
2
{
E
1
}
{a, ~b}
-
-
E
3
3
{
E
1
, E
3
}
{a, ~b, ~c}
E
4
4
{
E
1
, E
3
, E
4
}
-
-
-
-
The converse of the basic process
Establishing satisfiability may be easier than finding a model
