Re: Redefining the minus operator
- To: mathgroup at smc.vnet.net
- Subject: [mg53027] Re: Redefining the minus operator
- From: Paul Abbott <paul at physics.uwa.edu.au>
- Date: Mon, 20 Dec 2004 06:34:56 -0500 (EST)
- Organization: The University of Western Australia
- References: <cmkkn6$j99$1@smc.vnet.net> <200411080813.DAA07948@smc.vnet.net> <cp3shr$969$1@smc.vnet.net>
- Sender: owner-wri-mathgroup at wolfram.com
In article <cp3shr$969$1 at smc.vnet.net>, Ben Kovitz <bkovitz at acm.org> wrote: > Here's what I'm trying to do: derive theorems mechanically in > Mathematica. I'd like to be able to take, say, a trig theorem and a > few arithmetic theorems (like a + a == 2a), and see what other theorems > those generate. Hopefully I could also make a visualization of the > graph of logical implication and equivalence relations. > > For this purpose, I need to turn off *all* of Mathematica's > simplification code, and invoke just the pattern-matching code. I'd > also like the results to look nice, but you've shown me that it's far > simpler to just define a PLUS function and not even bother trying to > talk Mathematica out of its normal interpretation of +. > > I'm thinking of making an ever-growing list of theorems and just taking > Cases or another pattern-matching function on it. A potential problem > with this is just that it could get slow. I don't think DispatchTable > would be of much use, since the list produced is static, and my list of > theorems will grow and grow. I would recommend that you have a look at Theorema http://www.risc.uni-linz.ac.at/people/buchberg/theorema_project.html and also the work by Ronald Monson <Ronald.Monson at vu.edu.au>, formerly at The University of Western Australia but now at Victoria University in Melbourne. Cheers, Paul -- Paul Abbott Phone: +61 8 6488 2734 School of Physics, M013 Fax: +61 8 6488 1014 The University of Western Australia (CRICOS Provider No 00126G) 35 Stirling Highway Crawley WA 6009 mailto:paul at physics.uwa.edu.au AUSTRALIA http://physics.uwa.edu.au/~paul
- Follow-Ups:
- Re: Re: Redefining the minus operator
- From: Ben Kovitz <bkovitz@acm.org>
- Re: Re: Redefining the minus operator