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>
- Re: Re: logical/set theoretic programming
- References:
- logical/set theoretic programming
- From: Christopher Arthur <caa0012@unt.edu>
- logical/set theoretic programming