Services & ResourcesWolfram ForumsMathGroup Archive

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

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  
> 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

• Follow-Ups:
  • Re: Re: logical/set theoretic programming
    • From: János <janos.lobb@yale.edu>

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