drivers/metitarski.drv

   1 (* Why driver for MetiTarski *)
   2 (* main author: Piotr Trojanek <piotr.trojanek@gmail.com> *)
   3
   4 (* TODO:
   5  * real.FromInt
   6  * real.Truncate
   7  * real.PowerInt    (incomplete)
   8  * real.Hyperbolic
   9  * real.Polar       (should work as is)
  10  *)
  11
  12 printer "metitarski"
  13 filename "%f-%t-%g.tptp"
  14
  15 valid   "^SZS status Theorem"
  16 valid   "^SZS status Unsatisfiable"
  17 unknown "^SZS status CounterSatisfiable" ""
  18 unknown "^SZS status Satisfiable" ""
  19 timeout "^SZS status Timeout"
  20 unknown "^SZS status GaveUp" ""
  21 fail    "^SZS status Error" ""
  22
  23 time "why3cpulimit time : %s s"
  24
  25 (* to be improved *)
  26
  27 transformation "inline_trivial"
  28 transformation "eliminate_builtin"
  29 transformation "inline_all"
  30 transformation "eliminate_definition"
  31 transformation "eliminate_inductive"
  32 transformation "eliminate_algebraic"
  33 transformation "eliminate_literal"
  34 transformation "eliminate_if"
  35 transformation "eliminate_epsilon"
  36 transformation "eliminate_let"
  37 transformation "eliminate_negative_constants" (* due to integers, see below *)
  38
  39 transformation "simplify_formula"
  40 transformation "simplify_unknown_lsymbols"
  41 transformation "simplify_trivial_quantification"
  42 transformation "introduce_premises"
  43 transformation "instantiate_predicate"
  44 transformation "abstract_unknown_lsymbols"
  45
  46 transformation "discriminate"
  47 transformation "encoding_tptp"
  48
  49 theory BuiltIn
  50 (* support for integers disabled because may be inconsistent
  51   meta "encoding:kept" type int
  52 *)
  53   meta "encoding:base" type real
  54   syntax predicate (=)  "(%1 = %2)"
  55   meta "eliminate_algebraic" "no_index"
  56 end
  57
  58 import "discrimination.gen"
  59
  60 theory real.Real
  61
  62   syntax function zero "0.0"
  63   syntax function one  "1.0"
  64
  65   syntax function (+)  "(%1 + %2)"
  66   syntax function (-)  "(%1 - %2)"
  67   syntax function (-_) "(-%1)"
  68   syntax function (*)  "(%1 * %2)"
  69   syntax function (/)  "(%1 / %2)"
  70   syntax function inv  "(1/ %1)"
  71
  72   syntax predicate (<=) "(%1 <= %2)"
  73   syntax predicate (<)  "(%1 < %2)"
  74   syntax predicate (>=) "(%1 >= %2)"
  75   syntax predicate (>)  "(%1 > %2)"
  76
  77   meta "inline:no" predicate (<=)
  78   meta "inline:no" predicate (>=)
  79   meta "inline:no" predicate (>)
  80
  81   (* These follow from Metitarski's axioms. *)
  82   remove prop MulComm.Comm
  83   remove prop MulAssoc.Assoc
  84   remove prop Unit_def_l
  85   remove prop Unit_def_r
  86   remove prop Inv_def_l
  87   remove prop Inv_def_r
  88   remove prop Assoc
  89   remove prop Mul_distr_l
  90   remove prop Mul_distr_r
  91   remove prop Comm
  92   remove prop Unitary
  93   remove prop Inverse
  94   remove prop Refl
  95   remove prop Trans
  96   remove prop Antisymm
  97   remove prop Total
  98   remove prop NonTrivialRing
  99   remove prop CompatOrderAdd
 100   remove prop ZeroLessOne
 101
 102   remove prop add_div
 103   remove prop sub_div
 104   remove prop neg_div
 105   remove prop assoc_mul_div
 106   remove prop assoc_div_mul
 107   remove prop assoc_div_div
 108   remove prop CompatOrderMult
 109 end
 110
 111 prelude "%%% this is a prelude for Metitarski"
 112 prelude "include('Axioms/general.ax')."
 113
 114 theory real.Abs
 115   prelude "%%% this is a prelude for Metitarski absolute value"
 116
 117   syntax function abs "abs(%1)"
 118
 119   prelude "include('Axioms/abs.ax')."
 120   prelude "include('Axioms/abs2.ax')."
 121
 122   (* These follow from Metitarski's axioms. *)
 123   remove prop Abs_le
 124   remove prop Abs_pos
 125   remove prop Abs_sum
 126   remove prop Abs_prod
 127   remove prop triangular_inequality
 128 end
 129
 130 theory real.Square
 131   prelude "%%% this is a prelude for Metitarski square"
 132
 133   prelude "include('Axioms/sqrt-general.ax')."
 134
 135   syntax function sqr  "(%1)^2"
 136   syntax function sqrt "sqrt(%1)"
 137
 138   (* This follows from Metitarski's general axioms. *)
 139   remove prop Sqrt_positive
 140   remove prop Sqrt_le
 141 end
 142
 143 theory real.Trigonometry
 144   prelude "%%% this is a prelude for Metitarski trigonometry"
 145   remove allprops
 146
 147   prelude "include('Axioms/pi.ax')."
 148
 149   syntax function atan "arctan(%1)"
 150   syntax function tan  "tan(%1)"
 151
 152   prelude "include('Axioms/tan.ax')."
 153   prelude "include('Axioms/arctan-lower.ax')."
 154   prelude "include('Axioms/arctan-upper.ax')."
 155
 156   syntax function cos  "cos(%1)"
 157   syntax function sin  "sin(%1)"
 158
 159   prelude "include('Axioms/cos.ax')."
 160   prelude "include('Axioms/sin.ax')."
 161
 162   (* The following files "greatly increase the search space" and thus
 163      cause failures. Do not include them! *)
 164   (*
 165   prelude "include('Axioms/cos-constant.ax')."
 166   prelude "include('Axioms/sin-constant.ax')."
 167   *)
 168
 169 end
 170
 171 theory real.MinMax
 172   prelude "%%% this is a prelude for Metitarski min-max"
 173
 174   prelude "include('Axioms/minmax.ax')."
 175
 176   syntax function min "min(%1,%2)"
 177   syntax function max "max(%1,%2)"
 178
 179   remove prop Max_l
 180   remove prop Min_r
 181   remove prop Max_comm
 182   remove prop Min_comm
 183   remove prop Max_assoc
 184   remove prop Min_assoc
 185 end
 186
 187 (* support for integers disabled because may be inconsistent
 188 theory real.PowerInt
 189   syntax function power "%1^%2"
 190
 191   prelude "%%% this is a prelude for Metitarski power function"
 192
 193   prelude "include('Axioms/pow.ax')."
 194
 195   (* These follow from Metitarski's axioms. *)
 196 end
 197 *)
 198
 199 theory real.ExpLog
 200   syntax function exp "exp(%1)"
 201   syntax function log "ln(%1)"
 202
 203   prelude "%%% this is a prelude for Metitarski exp/log"
 204
 205   prelude "include('Axioms/exp-general.ax')."
 206   prelude "include('Axioms/ln-general.ax')."
 207
 208   (* These follow from Metitarski's axioms. *)
 209   remove prop Log_one
 210   remove prop Exp_zero
 211 end
 212
 213 theory real.PowerReal
 214   syntax function pow "pow(%1,%2)"
 215
 216   prelude "include('Axioms/pow.ax')."
 217
 218   (* These follow from Metitarski's axioms. *)
 219   remove prop Pow_def
 220   remove prop Pow_one_y
 221 end
 222
 223 (* support for integers disabled because may be inconsistent
 224 theory int.Int
 225
 226   syntax function zero "0"
 227   syntax function one  "1"
 228
 229   syntax function (+)  "(%1 + %2)"
 230   syntax function (-)  "(%1 - %2)"
 231   syntax function (*)  "(%1 * %2)"
 232   syntax function (-_) "(-%1)"
 233
 234   syntax predicate (<=) "(%1 <= %2)"
 235   syntax predicate (<)  "(%1 < %2)"
 236   syntax predicate (>=) "(%1 >= %2)"
 237   syntax predicate (>)  "(%1 > %2)"
 238
 239   (* These follow from Metitarski's axioms. *)
 240   remove prop MulComm.Comm
 241   remove prop MulAssoc.Assoc
 242   remove prop Unit_def_l
 243   remove prop Unit_def_r
 244   remove prop Inv_def_l
 245   remove prop Inv_def_r
 246   remove prop Assoc
 247   remove prop Mul_distr_l
 248   remove prop Mul_distr_r
 249   remove prop Comm
 250   remove prop Unitary
 251   remove prop Refl
 252   remove prop Trans
 253   remove prop Antisymm
 254   remove prop Total
 255   remove prop NonTrivialRing
 256   remove prop CompatOrderAdd
 257   remove prop CompatOrderMult
 258   remove prop ZeroLessOne
 259
 260 end
 261 *)