- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
(* basic power axiom
safe_comp_power x y =
case
(x = 0) and (y <> 0) -> 1
(x = 1) -> x
((x <> 0) and (y >= 0)) or ((x = 0) and (y > 0)) -> x * (safe_comp_power x (y - 1))
*)
logic safe_comp_pow : int, int -> int
axiom safe_comp_pow_int_A_1 : forall x : int. (x <> 0) -> safe_comp_pow(x, 0) = 1
axiom safe_comp_pow_int_A_2 : forall x : int. safe_comp_pow(x, 1) = x
axiom safe_comp_pow_int_A_3 : forall x,y : int. ((x <> 0) and (y >= 0)) or ((x = 0) and (y > 0)) -> safe_comp_pow(x, y) = x*(safe_comp_pow(x,y-1))
goal g_1 :
forall a,n : int.
a <> 0 -> n >= 0 ->
safe_comp_pow(a,n+1) = safe_comp_pow(a,n)*a
j123123 22.03.2016 16:39 # 0
kipar 22.03.2016 22:16 # 0
> int, int -> int
Ясно.
kurwa 22.03.2016 22:35 # 0
guest 22.03.2016 22:54 # +1
Годкод.ру это же лучший ресурс, круче чем РСДН
guest 22.03.2016 22:54 # +2
j123123 23.03.2016 05:07 # 0
j123123 23.03.2016 00:47 # 0
j123123 23.03.2016 00:59 # 0
3_14dar 23.03.2016 19:43 # −1
roman-kashitsyn 23.03.2016 09:33 # +1
j123123 23.03.2016 11:16 # 0
roman-kashitsyn 23.03.2016 13:46 # 0
roman-kashitsyn 23.03.2016 09:47 # 0
> (x <> 0) and (y >= 0)
Там точно включительно должно быть? С первой аксиомой пересечение получается. Решатель по порядку аксиомы пробует?
j123123 23.03.2016 11:15 # 0
или так:
roman-kashitsyn 23.03.2016 13:45 # 0
(y > 0) and (x >= 0)
kegdan 23.03.2016 13:50 # 0
y>0
j123123 23.03.2016 15:57 # 0
Потому что если подставить сюда x = 0 и y = 1 то оно проходит по условию (x = 0) and (y > 0) и исходя из этой аксиомы должно быть верно что safe_comp_pow(0, 1) = x*(safe_comp_pow(0,1-1))
Получается 0^0 - нельзя.
j123123 23.03.2016 16:47 # 0
доказательство того, что x*x = safe_comp_pow(x, 2):
j123123 23.03.2016 11:29 # 0
Там если собрать через opam этот alt-ergo то можно врубить логгирование, какие аксиомы и как он пытается
применять. Порядок объявления аксиом не важен