Making a Formula positive.

We define a program turning every formula A into a positive (i.e.: implication-free, and with negation on atomic formulas only) formula Pos[A], classically equivalent to it. In negative subformulas we switch disjunction and conjunction, existential and universal. We turn every subformula B⇒C or B→C into ¬B∨C if it is positive, into B∧¬C if it is negative.

In[68]:=

We start the program by the following clause:

In[76]:=

Some examples.

In[77]:=

Out[77]=

Out[78]=

In[79]:=

Out[79]=

Out[80]=

In[81]:=

Out[81]=

Out[82]=

In[83]:=

Out[83]=

Out[84]=

In[85]:=

Out[85]=

Out[86]=

In[87]:=

Out[87]=

Out[88]=

In[89]:=

Out[89]=

Out[90]=

Created by Mathematica  (October 17, 2006)