Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit a20d4ec9 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Metitarski, support for integer disabled, because inconsistency risks

parent 80714364
......@@ -42,24 +42,18 @@ transformation "encoding_smt"
*)
theory BuiltIn
(* support for integers disabled because may be inconsistent
meta "encoding : kept" type int
*)
meta "encoding : kept" type real
syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "no_index"
(*
meta "select_inst" "all"
meta "select_lskept" "all"
meta "select_lsinst" "all"
meta "select_kept" "all"
*)
end
import "discrimination.gen"
theory real.Real
meta "encoding : kept" type real
syntax function zero "0.0"
syntax function one "1.0"
......@@ -197,6 +191,7 @@ theory real.MinMax
remove prop Min_is_some
end
(* support for integers disabled because may be inconsistent
theory real.PowerInt
syntax function power "%1^%2"
......@@ -206,6 +201,7 @@ theory real.PowerInt
(* These follow from Metitarski's axioms. *)
end
*)
theory real.ExpLog
syntax function exp "exp(%1)"
......@@ -231,6 +227,7 @@ theory real.PowerReal
remove prop Pow_exp_log
end
(* support for integers disabled because may be inconsistent
theory int.Int
syntax function zero "0"
......@@ -268,3 +265,4 @@ theory int.Int
remove prop ZeroLessOne
end
*)
\ No newline at end of file
......@@ -42,12 +42,11 @@
shape="ainfix >=asqrV0c0.0F">
<proof
prover="0"
timelimit="60"
memlimit="1000"
edited="metitarski-P-sqr_pos_1.tptp"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.01"/>
</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