Re: logical/set theoretic programming
- To: mathgroup at smc.vnet.net
- Subject: [mg74139] Re: [mg74024] logical/set theoretic programming
- From: Andrzej Kozlowski <akoz at mimuw.edu.pl>
- Date: Mon, 12 Mar 2007 22:05:24 -0500 (EST)
- References: <200703061032.FAA02208@smc.vnet.net>
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 >
- References:
- logical/set theoretic programming
- From: Christopher Arthur <caa0012@unt.edu>
- logical/set theoretic programming