Logic Module: Quantified and/or Predicate Logic?
184 views
Skip to first unread message
Cullen Seaton
Mar 22, 2012, 4:38:27 PM3/22/12
to sy...@googlegroups.com
Hello,
I'm a third year undergraduate at the University of Chicago studying Mathematics. I read through the logic module documentation and it seems like sympy is currently limited to sentential logic. How much (if any) support is there for more advanced systems like Quantified Predicate Logic? I would be interested in expanding the logic module to include Quantifiers, predicate logic, modal logic etc. Is there anyone with whom I can speak about what kinds of logic and functions you would be interested in including? Thank you,
Cullen Seaton
University of Chicago
Class of 2013
Joachim Durchholz
Mar 22, 2012, 5:22:34 PM3/22/12
to sy...@googlegroups.com
Am 22.03.2012 21:38, schrieb Cullen Seaton:
> I read through the logic module documentation and it seems
> like sympy is currently limited to sentential logic. How much (if any)
> support is there for more advanced systems like Quantified Predicate Logic?
> I would be interested in expanding the logic module to include Quantifiers,
> predicate logic, modal logic etc. Is there anyone with whom I can speak
> about what kinds of logic and functions you would be interested in
> including? Thank you,
> I read through the logic module documentation and it seems
> like sympy is currently limited to sentential logic. How much (if any)
> support is there for more advanced systems like Quantified Predicate Logic?
> I would be interested in expanding the logic module to include Quantifiers,
> predicate logic, modal logic etc. Is there anyone with whom I can speak
> about what kinds of logic and functions you would be interested in
> including? Thank you,
I know a bit about predicate logic, and have some limited background
about proof theory (plus some odds and ends about temporal logic but
nothing solid there).
That means I can provide a second opinion about feasibility and similar
questions.
I haven't done any actual symbolic processing that uses formal logic, so
I have no real ideas about what would fit best for SymPy.
I think one of the first decisions would be whether we'd rather see
existing support completed or new features added.
Saptarshi Mandal
Mar 23, 2012, 3:19:01 AM3/23/12
to sympy
Hi,
> I'm a third year undergraduate at the University of Chicago studying
> Mathematics. I read through the logic module documentation and it seems
> like sympy is currently limited to sentential logic. How much (if any)
> support is there for more advanced systems like Quantified Predicate Logic?
Since you read the code, you should know that there is currently no
support
beyond propositional logic. There is a dpll SAT solver implemented and
that's
about it. The logic stuff is handled by Christian Muise, my mentor for
GSoC
2011 and an all round nice guy. I contributed a few small patches as
well.
The idea is to develop it further, add support for higher order logic,
BDDs
and get it into a state so that we can do mechanical theorem proving
with it
(this is obviously a long term vision). I think the ideas page also
mentions
non classical logic like fuzzy logic.
> I would be interested in expanding the logic module to include Quantifiers,
> predicate logic, modal logic etc. Is there anyone with whom I can speak
I am not sure how useful modal logic will be. They have very little
use in
axiomatizing mathematical statements.
> I'm a third year undergraduate at the University of Chicago studying
> Mathematics. I read through the logic module documentation and it seems
> like sympy is currently limited to sentential logic. How much (if any)
> support is there for more advanced systems like Quantified Predicate Logic?
support
beyond propositional logic. There is a dpll SAT solver implemented and
that's
about it. The logic stuff is handled by Christian Muise, my mentor for
GSoC
2011 and an all round nice guy. I contributed a few small patches as
well.
The idea is to develop it further, add support for higher order logic,
BDDs
and get it into a state so that we can do mechanical theorem proving
with it
(this is obviously a long term vision). I think the ideas page also
mentions
non classical logic like fuzzy logic.
> I would be interested in expanding the logic module to include Quantifiers,
> predicate logic, modal logic etc. Is there anyone with whom I can speak
use in
axiomatizing mathematical statements.
Cullen Seaton
Mar 23, 2012, 11:27:34 AM3/23/12
to sympy
Alright, then in the interest of working towards proving theorems, it
seems like an appropriate starting place might be to implement
predicates (something of the form l(x, y) that reads as "x has
property l with respect to y") and then begin working on adding
quantifiers. After all the absolute logic is in place, I would be be
interested in working more on logics with multiple truth values (which
I am admittedly a little less familiar with). I would also like to
begin by adding functions that can perform logical deduction. Does
this seem like an appropriate amount of work for the summer? Best
regards,
-Cullen
seems like an appropriate starting place might be to implement
predicates (something of the form l(x, y) that reads as "x has
property l with respect to y") and then begin working on adding
quantifiers. After all the absolute logic is in place, I would be be
interested in working more on logics with multiple truth values (which
I am admittedly a little less familiar with). I would also like to
begin by adding functions that can perform logical deduction. Does
this seem like an appropriate amount of work for the summer? Best
regards,
-Cullen
Christian Muise
Mar 23, 2012, 11:41:24 AM3/23/12
to sy...@googlegroups.com
Predicate:
Logical deduction:
And I wouldn't be so sure that modal logic isn't of interest. There are many forms that are still of quite a high interest (LTL being a prime example).
Cheers,
Christian
--
You received this message because you are subscribed to the Google Groups "sympy" group.
To post to this group, send email to sy...@googlegroups.com.
To unsubscribe from this group, send email to sympy+un...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/sympy?hl=en.
Damien Desfontaines
Mar 23, 2012, 11:39:19 AM3/23/12
to sy...@googlegroups.com
2012/3/23 Cullen Seaton <cullen...@gmail.com>:
> Alright, then in the interest of working towards proving theorems, it seems
> like an appropriate starting place might be to implement predicates (something
> of the form l(x, y) that reads as "x has property l with respect to y") and
> then begin working on adding quantifiers. After all the absolute logic is in
> place, I would be be interested in working more on logics with multiple truth
> values (which I am admittedly a little less familiar with). I would also like
> to begin by adding functions that can perform logical deduction. Does this
> seem like an appropriate amount of work for the summer? Best regards,
> -Cullen
> Alright, then in the interest of working towards proving theorems, it seems
> like an appropriate starting place might be to implement predicates (something
> of the form l(x, y) that reads as "x has property l with respect to y") and
> then begin working on adding quantifiers. After all the absolute logic is in
> place, I would be be interested in working more on logics with multiple truth
> values (which I am admittedly a little less familiar with). I would also like
> to begin by adding functions that can perform logical deduction. Does this
> seem like an appropriate amount of work for the summer? Best regards,
> -Cullen
A theorem verifyer and/or automatic prover seems to be a lot of work, in my
opinion : entire teams of researchers are needed to implement such systems, like
Coq or Isabelle. Maybe you should consider making thoses systems interact with
SymPy instead of re-coding everything ?
Damien
Christian Muise
Mar 23, 2012, 12:04:02 PM3/23/12
to sy...@googlegroups.com
Aye, wrapping should be an obvious target (you could start by wrapping a SAT solver to replace the prototype implementation currently in there). If there's any simple theorem proving technique that could be implemented, it's good to have something fully written in SymPy as shipping other solves with the library isn't recommended.
Joachim Durchholz
Mar 23, 2012, 2:40:40 PM3/23/12
to sy...@googlegroups.com
Am 23.03.2012 17:04, schrieb Christian Muise:
> Aye, wrapping should be an obvious target (you could start by wrapping a
> SAT solver to replace the prototype implementation currently in there). If
> there's any simple theorem proving technique that could be implemented,
> it's good to have something fully written in SymPy as shipping other solves
> with the library isn't recommended.
> Aye, wrapping should be an obvious target (you could start by wrapping a
> SAT solver to replace the prototype implementation currently in there). If
> there's any simple theorem proving technique that could be implemented,
> it's good to have something fully written in SymPy as shipping other solves
> with the library isn't recommended.
I'd start by defining some concrete use cases that this should support.
Preferrably some that aren't covered by Coq etc. - we don't want to
compete with established theorem provers, that's not SymPy's mission.
Cullen Seaton
Mar 24, 2012, 5:25:46 PM3/24/12
to sympy
You'll have to forgive me, I'm still a bit of novice programmer (an
enthusiastic novice), but can someone briefly explain what you all
mean by "wrapping"? I quite agree that building a fully functional
mechanical theorem prover is far from a feasible summer project. I
guess I'm more interested in developing more basic functionality that
could serve as a basis for moving in that direction. If replacing the
SAT solver (I assume you're referring to the one in logic/
inference.py) is a priority, that's something I'd love to work on.
Thank's, Christian, for pointing me to the Predicate class in
assumptions/assume.py. Best,
-Cullen
enthusiastic novice), but can someone briefly explain what you all
mean by "wrapping"? I quite agree that building a fully functional
mechanical theorem prover is far from a feasible summer project. I
guess I'm more interested in developing more basic functionality that
could serve as a basis for moving in that direction. If replacing the
SAT solver (I assume you're referring to the one in logic/
inference.py) is a priority, that's something I'd love to work on.
Thank's, Christian, for pointing me to the Predicate class in
assumptions/assume.py. Best,
-Cullen
Sergiu Ivanov
Mar 24, 2012, 5:31:19 PM3/24/12
to sy...@googlegroups.com
On Sat, Mar 24, 2012 at 11:25 PM, Cullen Seaton <cullen...@gmail.com> wrote:
> You'll have to forgive me, I'm still a bit of novice programmer (an
> enthusiastic novice), but can someone briefly explain what you all
> mean by "wrapping"?
>
> You'll have to forgive me, I'm still a bit of novice programmer (an
> enthusiastic novice), but can someone briefly explain what you all
> mean by "wrapping"?
>
> On Mar 23, 1:40 pm, Joachim Durchholz <j...@durchholz.org> wrote:
>> Am 23.03.2012 17:04, schrieb Christian Muise:
>>
>> > Aye, wrapping should be an obvious target (you could start by wrapping a
>> > SAT solver to replace the prototype implementation currently in there).
>> Am 23.03.2012 17:04, schrieb Christian Muise:
>>
>> > Aye, wrapping should be an obvious target (you could start by wrapping a
>> > SAT solver to replace the prototype implementation currently in there).
As I read it in this context, "to wrap" means to create a set of SymPy
classes/functions which will redirect any request to compute something
to the already existing SAT solver.
Sergiu
Christian Muise
Mar 24, 2012, 6:18:52 PM3/24/12
to sy...@googlegroups.com
Actually in this context I was using "wrap" to refer to an interface that would call an already existing solver (SAT solver or theorem prover).
Cullen Seaton
Mar 25, 2012, 9:05:03 AM3/25/12
to sympy
Ok, so we're talking about using an already existent proof engine like
Coq rather than trying to build one from scratch. Are you still
interested in improving the other bits of the logic module? I would
still like to work on things like multivalued and/or modal logics.
On Mar 24, 5:18 pm, Christian Muise <christian.mu...@gmail.com> wrote:
> Actually in this context I was using "wrap" to refer to an interface that
> would call an already existing solver (SAT solver or theorem prover).
>
> On Saturday, March 24, 2012, Sergiu Ivanov <unlimitedscol...@gmail.com>
> wrote:
>
>
>
> > On Sat, Mar 24, 2012 at 11:25 PM, Cullen Seaton <cullensea...@gmail.com>
Coq rather than trying to build one from scratch. Are you still
interested in improving the other bits of the logic module? I would
still like to work on things like multivalued and/or modal logics.
On Mar 24, 5:18 pm, Christian Muise <christian.mu...@gmail.com> wrote:
> Actually in this context I was using "wrap" to refer to an interface that
> would call an already existing solver (SAT solver or theorem prover).
>
> wrote:
>
>
>
> > On Sat, Mar 24, 2012 at 11:25 PM, Cullen Seaton <cullensea...@gmail.com>
Matthew Rocklin
Mar 30, 2012, 10:59:11 AM3/30/12
to sy...@googlegroups.com
Perhaps there's work that can be done to improve the current assumptions system? Are there any major TODOs for that project?
There is some current work at PR 1162 https://github.com/sympy/sympy/pull/1162
I was charmed by the idea of adding interval arithmetic to assumptions. It seems to have a number of uses. This is an idea brought up recently by Nathan Alison (who, I think, is no longer applying to GSoC). https://groups.google.com/d/topic/sympy/z9EtemLewBA/discussion . This is only tangentially related to the topic of improving Logic but might be of interest.
Reply all
Reply to author
Forward
0 new messages