[GSOC] Interested in an application related to formal logic and set theory?

[Peter Davies]

I'm a gsoc applicant, who's particularly interested in formal logics
and set theory. I'd be quite interested in working on those sorts of
areas over the summer. It says on the ideas page about logic and set
theory, "This task is heavily tied to the assumptions system.". Does
this mean that coding in this area should wait for revision of the
assumption module? In what sort of way would logic/set theory code be
using the assumptions system?



Peter,

[Ronan Lamy]

Actually, it's rather the other way round: the (new-style) assumption
system depends heavily on logic. So making sure that improvements to
logic translate into improvements to assumptions is an important goal.

[Peter Davies]

> Actually, it's rather the other way round: the (new-style) assumption
> system depends heavily on logic. So making sure that improvements to
> logic translate into improvements to assumptions is an important goal.

My understanding so far is:
* core/logic.py, core/facts.py, core/assumptions.py is the old
assumptions system.
* assumptions/* is the new assumptions system.

Would a GSOC proposal along the following lines make sense?
* Improve logic/boolalg.py to include Predicate logic, fuzzy logic and
useful functionality for manipulating them
* Use statements in predicate logic as the external format for
assumptions and rules. Such as
** forall x. real(x) => positive(x)
** forall x. nonnegative(x) <=> positive(x+1)
** forall x. nonnegative(x) <=> Abs(x) = x (I'm dubious about this one
since it's effectively expressing a rewrite rule)
* Implement a deduction system that can be the backend to Q.ask() (how
exactly we do this depends on what sort of rules we allow)

Peter,

[Christian Muise]

Would a GSOC proposal along the following lines make sense?
* Improve logic/boolalg.py to include Predicate logic, fuzzy logic and
useful functionality for manipulating them

  See the other thread on predicates in Sympy -- they already exist to some extent.

 

* Use statements in predicate logic as the external format for
assumptions and rules. Such as
** forall x. real(x) => positive(x)
** forall x. nonnegative(x) <=> positive(x+1)
** forall x. nonnegative(x) <=> Abs(x) = x (I'm dubious about this one
since it's effectively expressing a rewrite rule)

  These examples are already covered -- everything is assumed to be universally quantified, and the assumption system handles things of the sort you're proposing there.

 

* Implement a deduction system that can be the backend to Q.ask() (how
exactly we do this depends on what sort of rules we allow)

  Again, this is already mostly complete. The deduction is done using the prototype SAT solver, but is waiting to be hooked up with the changes currently being worked on for the assumptions subsystem (see https://github.com/sympy/sympy/pull/1162 ).

  Cheers