First Order Logic #7608

sd-biswas · 2014-06-18T19:08:25Z

asmeurer · 2014-06-18T19:12:12Z

sympy/logic/FOL.py

+        self._func = func
+        self._args = tuple(args)
+
+    def _sympystr(self, *args, **kwargs):


The second argument should be the printer, I think. You should use it to recursively print the arguments.

All the printers here are purely for my personal convenience at this moment. All of the printer code will go into the respective file soon.

asmeurer · 2014-06-18T19:13:03Z

I think you'll need to override _hashable_content along with __eq__. Python 3 make also make you override __hash__, which you should just pass to the superclass using super.

asmeurer · 2014-06-18T19:14:06Z

sympy/logic/FOL.py

+    >>> from sympy.logic.FOL import Predicate
+    >>> Knows = Predicate('Knows')
+    >>> Knows('John', 'Jack')
+    Knows(John, Jack)


Are 'John' and 'Jack' implicitly converted to Symbol('John') and Symbol('Jack')?

No. The are intended to be constants.

The problem is that SymPy objects don't really play with with non-SymPy objects such as strings as part of their expression tree. In this case, I would just only use Symbol everywhere, since that is the standard way to have a 'name' in SymPy.

asmeurer · 2014-06-18T19:19:10Z

I think it would be cleaner to just use symbols in place of strings. Most actual usage will be with symbols, I think. It's just a matter of using symbols in the doctests.

asmeurer · 2014-07-16T19:07:17Z

sympy/logic/FOL.py

+        self._name = name
+
+    def __call__(self, *args):
+        return self.apply()(self, *args)


There should be some apply on this class, even if it just raises NotImplementedError.

asmeurer · 2014-07-16T19:08:30Z

The class structure here is still a little confusing to me. Can you add a docstring to each class that just explains what it is for, especially the abstract base classes. It also should be made clear for each class if it is designed to be used on its own or if it is only a designed to be subclassed.

asmeurer · 2014-07-22T18:40:23Z

I don't think it's a good idea to have multiple to_cnf functions. I would just have the one function, and use dispatching to have it do the right thing on different kinds of objects (i.e., have to_cnf call _eval_to_cnf on the object if it has that method, and then implement that on the logic and first order logic classes).

asmeurer · 2014-07-22T18:42:17Z

sympy/logic/FOL.py

+    return expr.func(*args)
+
+
+def standardize(expr):


You should probably add a keyword argument to pass in a custom iterator of symbols.

Similar to the symbols argument to cse().

asmeurer · 2014-08-08T00:56:56Z

I am going to put a checklist at the top of the pull request, so that we can keep track of what needs to be done.

asmeurer · 2014-08-08T01:02:11Z

sympy/logic/FOL.py

+            raise ValueError("Use a constant instead of %s()" % func)
+        args = [arg if isinstance(arg, (Boolean, Symbol))
+                    else Constant(arg) for arg in args]
+        self._func = func


Is this at all related to self.func (which will be the class, Applied)?

The issue with using a property is that it leads to confusion to people reading the code from here, as you can see from this comment of mine.

asmeurer · 2014-08-12T16:22:35Z

I was hoping for more than just "abstract base class" in the docstrings of the abstract base classes. For someone coming to this module for the first time, it can be quite unclear what all the abstract classes are supposed to represent. It would be helpful to give a higher level idea of why they are there.

asmeurer · 2014-08-12T16:25:28Z

I think the Python 3 test failures are coming from using strings instead of SymPy objects in the doctests.

sd-biswas · 2014-08-12T17:01:38Z

I'll work on better documentation.
Simply calling to_snf followed by to_cnf/to_dnf (in boolalg) should give the user the required CNF/ DNF. to_snf returns an expression with no quantifiers (existentially bound variables are replaced by skolem functions and all other variables are considered to be universally quantified). Following this, any boolalg function can be called on this expression. The major requirement for CNF is for resolution, and the resolution method takes care of all this.
I will fix it in some time.

asmeurer · 2014-08-12T17:05:02Z

Simply calling to_snf followed by to_cnf/to_dnf (in boolalg) should give the user the required CNF/ DNF. to_snf returns an expression with no quantifiers (existentially bound variables are replaced by skolem functions and all other variables are considered to be universally quantified). Following this, any boolalg function can be called on this expression. The major requirement for CNF is for resolution, and the resolution method takes care of all this.

Good. I like this better. CNF and DNF should be only about propositional logic, and should treat quantifiers basic terms.

sd-biswas · 2014-09-09T22:34:17Z

Oh, that should fix the problem then. The Predicate in FOL represents the most generic predicate possible. So subclassing other things from it makes sense. If the name of Predicate (in assumptions) is changed to AssumptionsPredicate I'll have to make changes throughout assumptions to reflect the same. A quick grep shows that currently assumptions, core/tests and solvers/inequalities use this name. Do you know of anything that needs to be changed?
I think we should not make boolalg (BooleanFunction) dependent on FOL, simply from the perspective of logical separation. As far as possible we should keep the code for FOL limited to its file.

asmeurer · 2014-09-09T22:37:23Z

It shouldn't be used in many places. Also, if someone has code that uses Predicate and they don't update it to use AssumptionsPredicate the worst that will happen is that it won't print with the Q any more, right?
But is BooleanUndefinedFunction useful outside of FOL?

sd-biswas · 2014-09-09T22:40:46Z

The AssumptionsPredicate has these extra methods: add_handler, remove_handler, sort_key, eval.
BooleanUndefinedFunction has no use outside FOL

asmeurer · 2014-09-09T23:01:29Z

add_handler and remove_handler are assumptions specific. The sort_key should stay on the Predicate object. I don't know what eval is, but it sounds like something that should stay on Predicate as well.

Remind me again what a BooleanUndefinedFunction represents. It's just a function f(X) except unlike Function('f') from the core, it is assumed to take on boolean values, right?

asmeurer · 2014-09-13T20:39:41Z

@SDB1323 will you be able to finish this in the next week? Otherwise, it will need to be pushed to the next release.

sd-biswas · 2014-09-13T20:48:26Z

Yes, it should be ready by the next weekend.

sd-biswas · 2014-09-19T22:59:20Z

@asmeurer Please have a look at sd-biswas#1. Please confirm that this is what you want to be done finally. Additionally I need a little help from you because something is screwing up in ask once I do this.

asmeurer · 2014-09-21T21:16:13Z

I'm removing the milestone. If you finish this, please let me know and we can still get it in, but I don't want to block the release on it.

sd-biswas · 2014-09-21T21:19:56Z

Okay, sure. I am on this at the moment. I have modified the FOL classes to mimic the original Assumption classes. But that is creating errors in my code, so fixing that at the moment.

peterwittek · 2017-01-26T16:40:12Z

Is there any progress with this? Thanks.

ghost · 2018-01-19T17:48:44Z

I'm also interested in this, it appears to be halted now. Is there currently any plans for first-order logic in the future?

sd-biswas · 2018-01-19T18:44:44Z

@naiveaiguy Please speak to the maintainers. I have been away for a very long time and don't know the current state of things here. If there is still interest in having FOL then I can help you with modifying and/or rewriting this code.

@skirpichev

Mechanistic port of sympy/sympy#7608 for Diofant by @skirpichev.

@skirpichev

Mechanistic port of sympy/sympy#7608 for Diofant by @skirpichev.

@skirpichev