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
536f267e
Commit
536f267e
authored
Jan 03, 2017
by
MARCHE Claude
Browse files
example Genealogy: updated proofs to Isabelle 2016
parent
880be0fb
Changes
1
Hide whitespace changes
Inline
Side-by-side
examples/logic/genealogy/why3session.xml
View file @
536f267e
...
...
@@ -2,7 +2,6 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"Isabelle"
version=
"2015"
timelimit=
"5"
steplimit=
"1"
memlimit=
"4000"
/>
<prover
id=
"1"
name=
"CVC4"
version=
"1.2"
timelimit=
"60"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"2"
name=
"Zenon"
version=
"0.8.0"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"3"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"5"
steplimit=
"1"
memlimit=
"0"
/>
...
...
@@ -31,11 +30,11 @@
<prover
id=
"26"
name=
"Zenon Modulo"
version=
"0.4.1"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"27"
name=
"Coq"
version=
"8.4pl6"
timelimit=
"5"
steplimit=
"1"
memlimit=
"4000"
/>
<prover
id=
"28"
name=
"Z3"
version=
"4.4.1"
timelimit=
"5"
steplimit=
"1"
memlimit=
"4000"
/>
<prover
id=
"29"
name=
"Alt-Ergo"
version=
"1.30"
timelimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"29"
name=
"Alt-Ergo"
version=
"1.30"
timelimit=
"1"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"30"
name=
"Isabelle"
version=
"2016"
timelimit=
"5"
steplimit=
"1"
memlimit=
"4000"
/>
<file
name=
"../genealogy.why"
expanded=
"true"
>
<theory
name=
"Genealogy"
sum=
"35e1439432a79e05534b2c5cf39ad9dc"
expanded=
"true"
>
<goal
name=
"Child_is_son_or_daughter"
expanded=
"true"
>
<proof
prover=
"0"
edited=
"genealogy_Genealogy_Child_is_son_or_daughter_1.xml"
><result
status=
"valid"
time=
"6.55"
/></proof>
<goal
name=
"Child_is_son_or_daughter"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.00"
/></proof>
...
...
@@ -61,9 +60,9 @@
<proof
prover=
"27"
edited=
"genealogy_Genealogy_Child_is_son_or_daughter_1.v"
><result
status=
"valid"
time=
"0.80"
/></proof>
<proof
prover=
"28"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"29"
><result
status=
"valid"
time=
"0.00"
steps=
"10"
/></proof>
<proof
prover=
"30"
edited=
"genealogy_Genealogy_Child_is_son_or_daughter_1.xml"
><result
status=
"valid"
time=
"18.04"
/></proof>
</goal>
<goal
name=
"Sibling_sym"
expanded=
"true"
>
<proof
prover=
"0"
edited=
"genealogy_Genealogy_Sibling_sym_1.xml"
><result
status=
"valid"
time=
"6.09"
/></proof>
<goal
name=
"Sibling_sym"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.00"
/></proof>
...
...
@@ -89,9 +88,9 @@
<proof
prover=
"26"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"28"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"29"
><result
status=
"valid"
time=
"0.00"
steps=
"3"
/></proof>
<proof
prover=
"30"
edited=
"genealogy_Genealogy_Sibling_sym_1.xml"
><result
status=
"valid"
time=
"16.39"
/></proof>
</goal>
<goal
name=
"Sibling_is_brother_or_sister"
expanded=
"true"
>
<proof
prover=
"0"
edited=
"genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"
><result
status=
"valid"
time=
"6.19"
/></proof>
<goal
name=
"Sibling_is_brother_or_sister"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.00"
/></proof>
...
...
@@ -115,9 +114,9 @@
<proof
prover=
"26"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"28"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"29"
><result
status=
"valid"
time=
"0.00"
steps=
"10"
/></proof>
<proof
prover=
"30"
edited=
"genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"
><result
status=
"valid"
time=
"17.55"
/></proof>
</goal>
<goal
name=
"Grandparent_is_grandfather_or_grandmother"
expanded=
"true"
>
<proof
prover=
"0"
edited=
"genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"
><result
status=
"valid"
time=
"6.50"
/></proof>
<goal
name=
"Grandparent_is_grandfather_or_grandmother"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
/></proof>
...
...
@@ -142,6 +141,7 @@
<proof
prover=
"26"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"28"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"29"
><result
status=
"valid"
time=
"0.00"
steps=
"36"
/></proof>
<proof
prover=
"30"
edited=
"genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"
><result
status=
"valid"
time=
"18.55"
/></proof>
</goal>
<goal
name=
"Grandfather_male"
expanded=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
...
...
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