Resolution theorem proving
Resolution theorem proving
In[]:=
BooleanMinimize[(a||c)&&(b||!c)]
Out[]=
(a&&!c)||(b&&c)
In[]:=
FromDigits[Boole[BooleanTable[(a||c)&&(b||!c),{a,b,c}]],2]
Out[]=
216
In[]:=
RulePlot[CellularAutomaton[216]]
Out[]=
In[]:=
BooleanMinimize[Implies[(a||c)&&(b||!c),a||b]]
Out[]=
True
In[]:=
BooleanConvert[(a||c)&&(b||!c),"CNF"]
Out[]=
(a||c)&&(b||!c)
In[]:=
BooleanConvert[(a||c)&&(b||!c),"DNF"]
Out[]=
(a&&!c)||(b&&c)
Trying to deduce False from axioms && ¬proposition
Trying to deduce False from axioms && ¬proposition
