Commit 75efd6d9 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Metitarski: Remove files *-constant.ax from prelude, as they cause timeouts.

parent f98a2a85
......@@ -147,7 +147,7 @@ theory real.Trigonometry
prelude "include('Axioms/arctan-lower.ax')."
prelude "include('Axioms/arctan-upper.ax')."
syntax function atan "arctan(%1)"
syntax function atan "arctan(%1)"
syntax function tan "tan(%1)"
prelude "include('Axioms/cos.ax')."
......@@ -160,10 +160,13 @@ theory real.Trigonometry
remove prop Cos_0
remove prop Sin_0
(* The following files "greatly increase the search space" and thus
cause failures. Do not include them! *)
(*
prelude "include('Axioms/cos-constant.ax')."
prelude "include('Axioms/sin-constant.ax')."
*)
(* These follow from Metitarski's auxiliary axioms. *)
remove prop Cos_le_one
remove prop Sin_le_one
end
......
......@@ -27,11 +27,12 @@ theory P3
use import real.Real
use import real.Trigonometry
(* unprovable without cos-constant.ax, which causes failures for more interesting goals *)
goal cos_bound :
forall x:real. -1.0 <= cos x <= 1.0
goal cos_bound_harder :
forall x:real. 0.0 <= x <= 0.1 -> 0.1 <= cos x <= 1.0
forall x:real. -0.7 <= x <= 0.7 -> 0.7 <= cos x <= 1.0
end
......@@ -13,7 +13,7 @@
name="P"
locfile="../metitarski.why"
loclnum="1" loccnumb="7" loccnume="8"
verified="false"
verified="true"
expanded="true">
<goal
name="x_mul_x_pos"
......@@ -37,17 +37,81 @@
locfile="../metitarski.why"
loclnum="10" loccnumb="7" loccnume="14"
sum="14c5e18ceaa4ec73959d4db9a1295376"
proved="false"
proved="true"
expanded="true"
shape="ainfix &gt;=asqrV0c0.0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
<theory
name="P2"
locfile="../metitarski.why"
loclnum="15" loccnumb="7" loccnume="9"
verified="true"
expanded="true">
<goal
name="sqr_pos"
locfile="../metitarski.why"
loclnum="20" loccnumb="7" loccnume="14"
sum="222051b3fa2e2f7946541037ee172109"
proved="true"
expanded="true"
shape="ainfix &gt;=asqrV0c0.0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
edited="metitarski-P-sqr_pos_1.tptp"
obsolete="false"
archived="false">
<result status="unknown" time="0.24"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
<theory
name="P3"
locfile="../metitarski.why"
loclnum="25" loccnumb="7" loccnume="9"
verified="false"
expanded="true">
<goal
name="cos_bound"
locfile="../metitarski.why"
loclnum="30" loccnumb="7" loccnume="16"
sum="1279f956936a79ace638c17c4f31378d"
proved="false"
expanded="true"
shape="ainfix &lt;=acosV0c1.0Aainfix &lt;=aprefix -c1.0acosV0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="2.34"/>
</proof>
</goal>
<goal
name="cos_bound_harder"
locfile="../metitarski.why"
loclnum="33" loccnumb="7" loccnume="23"
sum="9e730acb71ecc7a8fb46ef19c84a57db"
proved="true"
expanded="true"
shape="ainfix &lt;=acosV0c1.0Aainfix &lt;=c0.7acosV0Iainfix &lt;=V0c0.7Aainfix &lt;=aprefix -c0.7V0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.21"/>
</proof>
</goal>
</theory>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment