Re: Re: logical/set theoretic programming
- To: mathgroup at smc.vnet.net
- Subject: [mg74148] Re: [mg74120] Re: [mg74024] logical/set theoretic programming
- From: János <janos.lobb at yale.edu>
- Date: Mon, 12 Mar 2007 22:10:17 -0500 (EST)
- References: <200703061032.FAA02208@smc.vnet.net> <200703120931.EAA26948@smc.vnet.net>
Have a look at the page: http://www.wolframscience.com/nksonline/page-1176b-text and then click on the "Downloadable programs for this page" link to start with. J=E1nos 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 = 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 ---------------------------------------------- Trying to argue with a politician is like lifting up the head of a corpse. (S. Lem: His Master Voice)
- References:
- logical/set theoretic programming
- From: Christopher Arthur <caa0012@unt.edu>
- Re: logical/set theoretic programming
- From: Christopher Arthur <caa0012@unt.edu>
- logical/set theoretic programming