Services & Resources / Wolfram Forums
-----
 /
MathGroup Archive
2004
*January
*February
*March
*April
*May
*June
*July
*August
*September
*October
*November
*December
*Archive Index
*Ask about this page
*Print this page
*Give us feedback
*Sign up for the Wolfram Insider

MathGroup Archive 2004

[Date Index] [Thread Index] [Author Index]

Search the Archive

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


  • Prev by Date: Re: How input stacked characters with vertical bar
  • Next by Date: Re: Re: Mathematica language issues
  • Previous by thread: Re: Re: Redefining the minus operator
  • Next by thread: Re: Re: Redefining the minus operator