to_CNF

[Fernando Ferreira]

Hi all,

Im trying to convert a formula do CNF to get the diferent clauses of the formula.

Imagine this formula:

{ a in S :  (all s in S all t in S exists u )   a * s = a * u  <->   a * t = u * a    }

How doi insert the quantifyers "for all" and "exists" sympy.

I tryed something like prover9 format but with no luck.

Thanks in advance.

[Aaron Meurer]

We don't have ForAll or Exists objects yet. See
https://github.com/sympy/sympy/pull/7608.

Aaron Meurer

> --
> You received this message because you are subscribed to the Google Groups
> "sympy" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to sympy+un...@googlegroups.com.
> To post to this group, send email to sy...@googlegroups.com.
> Visit this group at https://groups.google.com/group/sympy.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/sympy/54e3cdb7-ce52-41d2-83c8-d2690c1f9bdb%40googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.