[Date Index] [Thread Index] [Author Index]

Re: logical/set theoretic programming

• To: mathgroup at smc.vnet.net
• Subject: [mg74139] Re: [mg74024] logical/set theoretic programming
• From: Andrzej Kozlowski <akoz at mimuw.edu.pl>
• Date: Mon, 12 Mar 2007 22:05:24 -0500 (EST)
• References: <200703061032.FAA02208@smc.vnet.net>

You won't be able to make much use of most of the built in functions  
you mention in your post, that is Element, Exists, Reduce,Refine  
since they are already defined and intended for a different purpose .  
You could make some use of Simplify if you construct your own  
TransformationRules, but doing that would not have any obvious  
advantage over defining your own function called, say,  
LogicalSimplify or something like that. You might also be able to  
make some use of Implies and LogicExpand because they can be used to  
perform certain elementary deductions belonging to "propositional  
logic", an example being:

LogicalExpand[Implies[Or[a,b]&&Not[b],a]]

True

where a and b are abstract sentences. Of course what you want to do  
is much harder, in fact to do what you seem to want to do is to  
implement first order logic, which will be quite hard and is not  
implemented in Mathematica, though there may be some packages that do  
that. What is implemented din Mathematica  is quantifier elimination  
for first order formulas in the language of ordered fields with  
parameters in the real numbers, which is what  the built-in functions  
Exists, ForAll and Resolve are for, but that won't be of any use in  
your stated task.
So, my point is that you really have to program everything form  
scratch yourself, unless you can find a suitable package. It's quite  
easy to use patterns and rules to make Mathematica decide a few basic  
cases, like the one you mention, but for something more sophisticated  
it would be easier to learn Prolog.

Andrzej Kozlowski


On 6 Mar 2007, at 11:32, Christopher Arthur wrote:

> Hello, any suggestions on how to program set theory?
> Suppose that I have a notation set up well, and I have a set of rules
> of implication.  The next step is to teach mathemania how to  
> compute...
> For example, I define a notation for AbstractComplement[X,A], and I
> want to associate it with it the rule
> Implies[Subset[A,X]&&Element[x,A],!Element[x,AbstractComplement[X,A]].
> In other words, a point can't be in a subset and its complement.  My
> feeling is that alone this rule should be enough to decide the
> falsehood of a statement such as
> Subset[B,W]&&Exists[y,Element[y,B]&&Element[y,AbstractComplement[W,B]]
>
> where in this case i've purposefully changed the variables because i
> don't want to tie the rule to any particular symbols.  How can we set
> up Simplify,Reduce,Refine or something similar to decide on this rule?
> Especially, without having to make the rule explicit in the expression
> to simplify. Christopher Arthur
> Student, Mathematics
> University of North Texas
>

• References:
  • logical/set theoretic programming
    • From: Christopher Arthur <caa0012@unt.edu>