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
>

```

• Prev by Date: Re: Transformation rules - explain please
• Next by Date: Re: PN junction Simulation with Mathematica
• Previous by thread: Re: Re: logical/set theoretic programming
• Next by thread: Re: logical/set theoretic programming