-
Notifications
You must be signed in to change notification settings - Fork 4
/
README.metitarski
170 lines (131 loc) · 6.76 KB
/
README.metitarski
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
KeYmaera-MetiTarski interface README
§1 GENERAL INFORMATION
MetiTarski is a theorem prover developed at the University of Cambridge which
is specifically "designed to prove theorems involving real-valued special
functions such as log, exp, sin, cos and sqrt. In particular, it is designed
to prove universally quantified inequalities involving such functions".
For more details, see
http:https://www.cl.cam.ac.uk/~lp15/papers/Arith/
KeYmaera provides an interface to MetiTarski, much as it does for other
back-end solvers such as QEPCAD and Reduce.
§2 INSTALLATION
For information about installing MetiTarski on your system, please see
http:https://www.cl.cam.ac.uk/~lp15/papers/Arith/download.html
An alternative way to obrain the latest source code is Google Code:
https://code.google.com/p/metitarski/
N.B. In case of compatibility issues in the release version, it is advisable
to checkout the latest snapshot from Google Code.
In order to use KeYmaera with MetiTarski, it is required that the path for
both the MetiTarski binary and the Axioms directory be set in KeYmaera tool
paths, e.g.
Binary: /opt/metit-2.0/metit
Axioms: /opt/metit-2.0/tptp
§3 USAGE
The primary use case is the handling of solutions to ordinary differential
equations. After calling ODESolve on the system dynamics in KeYmaera, the
system produces a closed form solution (if one can be obtained) which will
frequently feature transcendental terms.
MetiTarski can be used as a solver for non-polynomial real arithmetic, i.e.
it will *attempt* to determine whether a given first-order sentence involving
transcendental terms is true or not, and if so - it will close the proof
branch, otherwise it will leave the query intact.
N.B. Unlike CAD-based methods employed for polynomials, MetiTarski cannot
be used directly to synthesize constraints on system parameters. It
will treat free variable occurrences as implicitly *universally*
quantified and will either produce a proof that a given sentence is a
theorem, or will fail to find any proof (which does *not* mean that the
sentence is false).
Other use cases include transcendental terms in the system dynamics or
constraints to state/parameter space.
N.B. It is often prudent to use a simplifier shipped with a computer algebra
system (e.g. Mathematica) before calling MetiTarski on the problem, as
this will tend to eliminate some unnecessary complexities, albeit at
the expense of soundness guarantees.
Any .key file which is intended to be used with MetiTarski has to include a
functions block declaring *all* the special function symbols that will occur
during the proof; below are some examples:
TRIGONOMETRIC
\functions {
\external R E;
\external R Exp(R);
\external R Sin(R);
\external R Cos(R);
\external R Tan(R);
}
INVERSE TRIGONOMETRIC
\functions{
\external R ArcTan(R);
\external R ArcCos(R);
\external R ArcSin(R);
\external R Sin(R);
\external R Cos(R);
\external R Tan(R);
\external R Exp(R);
\external R Log(R);
\external R E;
}
HYPERBOLIC
\functions{
\external R E;
\external R Exp(R);
\external R Cosh(R);
\external R Sinh(R);
\external R Tanh(R);
\external R Log(R);
}
INVERSE HYPERBOLIC
\functions{
\external R ArcCosh(R);
\external R ArcSinh(R);
\external R ArcTanh(R);
}
MIN, MAX, ABS
\functions{
\external R Min(R,R);
\external R Max(R,R);
\external R Abs(R);
}
PI
\functions{
\external Pi;
}
The KeYmaera interface gives access to all the command-line options offered
by MetiTarski. To change the default settings, navigate to the MetiTarski
options pane (as for other solvers) and select the options manually.
N.B. A copy of the problems sent to MetiTarski will be stored under a unique
.tptp file in the default temporary storage directory. These can be
accessed and inspected/run manually from the command line.
When choosing variable names for your KeYmaera problems, please assume that
variable identifiers are equal modulo their case as MetiTarski is *not* case
sensitive. It is generally safer to be explicit, e.g. using variable names
't' and 'tau', rather than 't' and 'T'.
WARNING: Please make sure that none of the variable identifiers is 'E', as
this symbol is reserved as a Mathematica shortcut for Exp[], the
exponential function.
§4 EXAMPLES
An example of a .key problem with transcendental dynamics
\functions {
\external R E;
\external R Exp(R);
\external R Sin(R);
\external R Cos(R);
\external R Tan(R);
R a;
}
\programVariables {
R x1, x2;
}
\problem {
((x1^2 +x1*x2 +4*(x2^2))<=a) & a>=0 & a < 0.69929971 ->
\[ {
x1' = x2,
x2' = -Sin(x1) + (81/100)*Cos(x1)*Sin(x1)-(x2/5)&
((x1^2 +x1*x2 +4*(x2^2)) <= 0.69929971)
} \]
((x1^2 +x1*x2 +4*(x2^2)) <= a )
}
Further examples and proofs using MetiTarski are provided with KeYmaera's
examples in examples/hybrid/transcendental.
§5 BUGS
Please contact the interface maintainer < s0805753 -át- sms.ed.ac.uk >
in the event of software malfunction or to request changes/features.