|
ahirn@37877
|
1 |
\chapter{\isac s tactics}
|
|
ahirn@37877
|
2 |
|
|
ahirn@37877
|
3 |
\begin{description}
|
|
ahirn@37877
|
4 |
\item{\bf Init\_Proof\_Hid (dialogmode, formalization, specification)} transfers the arguments to the math engine, the latter two in order to solve the example automatically. The tactic is not intended to be used by the student; it generates a proof tree with an empty model.
|
|
ahirn@37877
|
5 |
\item{\bf Init\_Proof} generates a proof tree with an empty model.
|
|
ahirn@37877
|
6 |
\item{\bf Model\_Problem problem} determines a problemtype (eventually found in the hierarchy) to be used for modeling.
|
|
ahirn@37877
|
7 |
\item{\bf Add\_Given, Add\_Find, Add\_Relation formula} inputs a formula to the respective field in a model (necessary as long as there is no facility for the user to input formula directly, and not only select the respective tactic plus formula from a list).
|
|
ahirn@37877
|
8 |
\item{\bf Specify\_Theory theory, Specify\_Problem problem, Specify\_Method method} specifies the respective element of the knowledgebase.
|
|
ahirn@37877
|
9 |
\item{\bf Refine\_Problem problem} searches for a matching problem in the hierarchy below 'problem'.
|
|
ahirn@37877
|
10 |
\item{\bf Apply\_Method method} finishes the model and specification phase and starts the solve phase.
|
|
ahirn@37877
|
11 |
\item{\bf Free\_Solve} initiates the solve phase without guidance by a method.
|
|
ahirn@37877
|
12 |
\item{\bf Rewrite theorem} applies 'theorem' to the current formula and transforms it accordingly (if possible -- otherwise error).
|
|
ahirn@37877
|
13 |
\item{\bf Rewrite\_Asm theorem} is the same tactic as 'Rewrite', but stores an eventual assumption of the theorem (instead of evaluating the assumption, i.e. the condition)
|
|
ahirn@37877
|
14 |
\item{\bf Rewrite\_Set ruleset} similar to 'Rewrite', but applies a whole set of theorems ('ruleset').
|
|
ahirn@37877
|
15 |
\item{\bf Rewrite\_Inst (substitution, theorem), Rewrite\_Set\_Inst (substitution, ruleset)} similar to the respective tactics, but substitute a constant (e.g. a bound variable) in 'theorem' before application.
|
|
ahirn@37877
|
16 |
\item{\bf Calculate operation} calculates the result of numerals w.r.t. 'operation' (plus, minus, times, cancel, pow, sqrt) within the current formula.
|
|
ahirn@37877
|
17 |
\item{\bf Substitute substitution} applies 'substitution' to the current formula and transforms it accordingly.
|
|
ahirn@37877
|
18 |
\item{\bf Take formula} starts a new sequence of calculations on 'formula' within an already ongoing calculation.
|
|
ahirn@37877
|
19 |
\item{\bf Subproblem (theory, problem)} initiates a subproblem within a calculation.
|
|
ahirn@37877
|
20 |
\item{\bf Function formula} calls a function, where 'formula' contains the function name, e.g. 'Function (solve $1+2x+3x^2=0\;\;\;x$)'. In this case the modelling and specification phases are suppressed by default, i.e. the solving phase of this subproblem starts immediately.
|
|
ahirn@37877
|
21 |
\item{\bf Split\_And, Conclude\_And, Split\_Or, Conclude\_Or, Begin\_Trans, End\_Trans, Begin\_Sequ, End\_Sequ, Split\_Intersect, End\_Intersect} concern the construction of particular branches of the prooftree; usually suppressed by the dialog guide.
|
|
ahirn@37877
|
22 |
\item{\bf Check\_elementwise assumptions} w.r.t. the current formula which comprises elements in a list.
|
|
ahirn@37877
|
23 |
\item{\bf Or\_to\_List} transforms a conjunction of equations to a list of equations (a questionable tactic in equation solving).
|
|
ahirn@37877
|
24 |
\item{\bf Check\_postcond:} check the current formula w.r.t. the postcondition on finishing the resepctive (sub)problem.
|
|
ahirn@37877
|
25 |
\item{\bf End\_Proof} finishes a proof and delivers a result only if 'Check\_postcond' has been successful before.
|
|
ahirn@37877
|
26 |
\end{description} |