Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
e97308ee
Commit
e97308ee
authored
Mar 24, 2015
by
MARCHE Claude
Browse files
removed axiom generating a wrong proof by metitarski
parent
7369b0a2
Changes
4
Hide whitespace changes
Inline
Side-by-side
examples/tests-provers/metitarski.why
View file @
e97308ee
...
...
@@ -45,3 +45,16 @@ theory P3
end
theory Power
use import real.RealInfix
use import real.PowerReal
goal G: false
goal G1: forall x:real. x >. 2.0 -> (pow x 3.0) *. 2.0 >. 20.0
goal G2: forall x:real. x >. 2.0 -> x >. 5.0
end
examples/tests-provers/metitarski/why3session.xml
View file @
e97308ee
...
...
@@ -3,6 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"MetiTarski"
version=
"2.2"
timelimit=
"60"
memlimit=
"4000"
/>
<prover
id=
"1"
name=
"MetiTarski"
version=
"2.4"
timelimit=
"5"
memlimit=
"1000"
/>
<file
name=
"../metitarski.why"
expanded=
"true"
>
<theory
name=
"P"
sum=
"1d04567a049f848cb57260f3bbd2cdfa"
expanded=
"true"
>
<goal
name=
"x_mul_x_pos"
expanded=
"true"
>
...
...
@@ -31,5 +32,16 @@
<proof
prover=
"0"
memlimit=
"1000"
><result
status=
"unknown"
time=
"3.24"
/></proof>
</goal>
</theory>
<theory
name=
"Power"
sum=
"f1807c022587c3770e4e7984d0a322b9"
expanded=
"true"
>
<goal
name=
"G"
expanded=
"true"
>
<proof
prover=
"1"
><result
status=
"unknown"
time=
"0.17"
/></proof>
</goal>
<goal
name=
"G1"
expanded=
"true"
>
<proof
prover=
"1"
><result
status=
"unknown"
time=
"0.19"
/></proof>
</goal>
<goal
name=
"G2"
expanded=
"true"
>
<proof
prover=
"1"
edited=
"metitarski-Power-G2_1.tptp"
><result
status=
"unknown"
time=
"0.20"
/></proof>
</goal>
</theory>
</file>
</why3session>
examples/tests-provers/metitarski/why3shapes.gz
View file @
e97308ee
No preview for this file type
theories/real.why
View file @
e97308ee
...
...
@@ -252,8 +252,10 @@ theory PowerReal
function pow real real : real
(*
axiom Pow_zero_y:
forall y:real. y > 0.0 -> pow 0.0 y = 0.0
*)
axiom Pow_x_zero:
forall x:real. x <> 0.0 -> pow x 0.0 = 1.0
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment