# fa.bianp.net

The logic module is slowly becoming useful. This week I managed to get some basic inference in propositional logic working. This should be enough for the assumption sysmtem (although having first-order inference would be cool). You can pull from my branch: `` git pull http://fa.bianp.net/git/sympy.git logic`` Here are some examples of what it can do: First, importing and defining our symbols

```In : A, B, C = symbols('ABC')
In : from sympy.logic import *
```

It works with Symbols just as you would expect

```In : And(A, B)
Out: And(A, B)
```

It applies De Morgan Rules automatically

```In : Not(Or(A, B))
Out: And(Not(A), Not(B))
```

converts to conjuntive normal form (CNF)

```In : to_cnf(Implies(A, And(B, C)))
Out: And(Or(B, Not(A)), Or(C, Not(A)))
```

Some basic inference:

```In : pl_true( Or(A, B), {A : True})  # what can we say about Or(A, B) if A is True ?
Out: True

In : pl_true ( And(A, B), {B: False}) # what is And(A, B) if B is False
Out: False
```

To be discussed: - I'm not sure if we should override &&, || on Symbol so that we can do A && B instead of And(A, B). If would make the code cleaner, but also I don't want to bloat Symbol any more. What do you think ? I'm very proud of this in the sense that it is a nice clean module that will hopefully serve as the foundation of the new assumption system.

Mastodon