Re: logical/set theoretic programming

• To: mathgroup at smc.vnet.net
• Subject: [mg74120] Re: [mg74024] logical/set theoretic programming
• From: Christopher Arthur <caa0012 at unt.edu>
• Date: Mon, 12 Mar 2007 04:31:56 -0500 (EST)
• References: <200703061032.FAA02208@smc.vnet.net>

```My goal is in fact not to teach mathematica how to prove anything
clever.  All I really want to do is give it a list of logical
propositions, such as theorems and definitions in a known and specific
topic, and then use combinatorica or similiar project to show a graph
of the relationships among the concepts.  The main simplification that
i would like to make is to remove redundant implications from the
system.  For example if my system contains A=>B
B=>C
A=>C

then the last implication A=>C is superfluous and can be removed from
the graph.  I think most of the important propositions can be handled
on the logical level, but there are a few special ones that deal with
subsets.  But I'm coming to the conclusion that to descend into them is
more trouble than its worth.  Quoting Andrzej Kozlowski
<akoz at mimuw.edu.pl>:

> *This message was transferred with a trial version of CommuniGate(tm) Pro*
> 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
> 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
> 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
>>
>
>

Christopher Arthur
Student, Mathematics
University of North Texas

```

• Prev by Date: RE: plot of "marginal distributions" of scatter plot
• Next by Date: Re: plot of "marginal distributions" of scatter plot
• Previous by thread: Re: logical/set theoretic programming
• Next by thread: Re: Re: logical/set theoretic programming