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
>> 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
>>>
>>
>>
>
>
>
> Christopher Arthur
> Student, Mathematics
> University of North Texas
- References:
- logical/set theoretic programming
- From: Christopher Arthur <caa0012@unt.edu>
- logical/set theoretic programming