MathGroup Archive 2007

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

Search the Archive

Re: Re: logical/set theoretic programming

Have a look at the page:

and then click on the

"Downloadable programs for this page" link

to start with.


On Mar 12, 2007, at 5:31 AM, 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 =
> 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>:
>> *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

Trying to argue with a politician is like lifting up the head of a 
(S. Lem: His Master Voice)

  • Prev by Date: Re: Re: Re: Re: fastest way to add up a billion numbers
  • Next by Date: Re: logical/set theoretic programming
  • Previous by thread: Re: logical/set theoretic programming
  • Next by thread: Re: logical/set theoretic programming