Incomplete Models
Model finders' models interpret only symbols in formulae
If no
false
axiom select a
not-true
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
Model
Axiom
1
{ }
{~b}
E
1
