search

windsteiger / Theorema

Theorema: A System for Automated Reasoning (Theorem Proving) and Automated Theory Exploration based on Mathematica
GNU General Public License v3.0
71 stars 14 forks source link

Errors in connection with domain operators #32

Closed amaletzk closed 11 years ago

amaletzk commented 11 years ago

As soon as domain operators, like "D[Plus]" (in underscript notation!) are introduced, the context of other symbols in formulae that are evaluated afterwards is changed: Example: First evaluate "forall x: D[Plus][x, 1] == 2" (in underscript notation!) Then the formula F = "forall x in {1}: x+1 == 2" cannot be proved any more, even if all built-ins are activated (however, it can be computed and the result is "True"!). Reason: Internally, the symbols in F are, e.g., "Plus$TM" rather than "TheoremaLanguage Plus$TM" Possible solution: Replace "ToExpression[]" by "ReleaseHold[MakeExpression[]]" in the various definitions of function "MakeExpression" in file "Language/Syntax.m" that deal with underscript boxes.

Another error occurs if one writes, e.g., "D[Plus][1,2]" (in underscript notation!), because Mathematica evaluates "Plus[1,2]" when "ToExpression" is called on it (see above), and then the result is not an expression with 2 subexpressions any more, as needed.

windsteiger commented 11 years ago

We use MakeExpression instead of ToExpression, but no ReleaseHold in order to prevent any evaluation. MakeExpression gives HoldComplete[...], and therein we access the head symbol directly.

The problem with ToExpression seems to be that it involves evaluation. MakeExpression is part of the preprocessing and the ToExpression in it prematurely terminates the preprocessing. Therefore, the $Context and $ContextPath are not reset at the end of the preprocessing (closeEnvironment[]).