Added a method "fixSymmetry" to transform a RobinsonRefutation of a set of clauses C to a refutation of a set C' such that C' is C modulo applications of symmetry.
Added trivial projection to tautological clause to PCNF.
Added a case to treat "=" in SimpleFOLParser.
Added PrincipalFormulas trait to Paramodulation and changed unapply method.
Added some convenience constructors to RobinsonResolution calculus.



git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1818 85d21ef8-add0-11de-ae77-5bfb9c5a3f34