logical/set theoretic programming

*To*: mathgroup at smc.vnet.net*Subject*: [mg74024] logical/set theoretic programming*From*: Christopher Arthur <caa0012 at unt.edu>*Date*: Tue, 6 Mar 2007 05:32:35 -0500 (EST)

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

**Follow-Ups**:**Re: logical/set theoretic programming***From:*"Richard Palmer" <rhpalmer@gmail.com>

**Re: logical/set theoretic programming***From:*Andrzej Kozlowski <akoz@mimuw.edu.pl>

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

**Re: logical/set theoretic programming***From:*"Chris Chiasson" <chris@chiasson.name>