Re: logical/set theoretic programming

• To: mathgroup at smc.vnet.net
• Subject: [mg74147] Re: [mg74024] logical/set theoretic programming
• From: Andrzej Kozlowski <akoz at mimuw.edu.pl>
• Date: Mon, 12 Mar 2007 22:09:44 -0500 (EST)
• References: <200703061032.FAA02208@smc.vnet.net> <D653C710-17C0-426B-82D6-008C44D52942@mimuw.edu.pl> <20070311191027.yp5psi9k170g40kc@eaglemail.unt.edu>

```As I wrote earlier, Mathematica can deal with propositional logic to
some extent, so for example, in your case you cqan do;

LogicalExpand[Implies[A, C] && Implies[B, C] &&
Implies[A, C]]

C || ( !A &&  !B)

The answer has no redundancy and is equivalent to

LogicalExpand[Implies[A, C] && Implies[B, C]]

C || ( !A &&  !B)

but it now contains no explicit Implies and there is no automatic way
to convert logical expressions involving Or, And etc.  into ones
involving Implies. If, however, you wrote all your formulas using
boolean operations Or, And, Xor and Not, then, at the purely
propositional level, LogicalExpand should remove any redundancies.

Andrzej Kozlowski

On 12 Mar 2007, at 01:10, Christopher Arthur wrote:

> 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
>> 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
>> 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: Re: logical/set theoretic programming
• Next by Date: Re: How to rotate AxesLabel ?
• Previous by thread: Re: logical/set theoretic programming
• Next by thread: Re: logical/set theoretic programming