- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
- 22
- 23
- 24
- 25
- 26
- 27
- 28
- 29
- 30
- 31
- 32
- 33
- 34
- 35
- 36
- 37
- 38
- 39
- 40
- 41
- 42
- 43
- 44
- 45
- 46
- 47
- 48
- 49
- 50
- 51
- 52
- 53
- 54
- 55
- 56
- 57
- 58
- 59
- 60
- 61
- 62
- 63
- 64
- 65
- 66
(set-logic UF)
; https://smtlib.cs.uiowa.edu/logics.shtml
; UF for the extension allowing free sort and function symbols
(set-option :produce-proofs true)
(declare-sort M_list)
(declare-fun m_node (M_list M_list) M_list)
; один хер какой порядок, можно переписать (a, b) на (b, a)
(assert
(forall ( (a M_list) (b M_list) )
(=
(m_node a b)
(m_node b a)
)
)
)
; если есть (a (b c)) то можно переписать на (с (a b))
(assert
(forall ( (a M_list) (b M_list) (c M_list) )
(=
(m_node a (m_node b c) )
(m_node c (m_node a b) )
)
)
)
; Можно создавать или удалять повторы, (a a) <=> a
(assert
(forall ( (a M_list))
(=
(m_node a a)
a
)
)
)
; Чтоб узнать, выводима ли такая-то хернь
(declare-fun m_node_select (M_list M_list) Bool)
(assert
(forall ( (a M_list) (b M_list) )
(m_node_select
a (m_node a b)
)
)
)
; проверяем, можно ли сконструировать (a a) из (c ((b d) a))
(assert
(not (forall ( (a M_list) (b M_list) (c M_list) (d M_list) )
(m_node_select
(m_node a a)
(m_node c (m_node (m_node b d) a) )
)
))
)
(check-sat)
(get-proof)
j123123 01.03.2021 19:45 # 0
bormand 01.03.2021 19:49 # 0
j123123 01.03.2021 20:02 # 0
bormand 01.03.2021 20:07 # 0
А что делать, если они не осиливают? Какой-то способ вручную пнуть в нужном направлении есть?
j123123 01.03.2021 20:09 # 0
bormand 01.03.2021 20:22 # 0
Блин, я вот кстати х.з. как в петухе записать a и b -- неведомая хуйня одного сорта. Походу тут совсем другая логика юзается.
bormand 01.03.2021 21:24 # +2
j123123 13.03.2021 08:19 # 0
bormand 13.03.2021 10:19 # 0
j123123 13.03.2021 11:06 # 0
https://cs.stackexchange.com/a/80737
> Prop is meant for propositions. It is impredicative, meaning that you can instantiate polymorphic functions with polymorphic types. It also has proof irrelevance, meaning that if p1,p2:P then p1=p2. This allows terms that are only used for proof to be erased in any code generated by Coq.
> Set is meant for computation. It's predicative, and doesn't have proof irrelevance, which lets you do nice things like not assuming 1=2. The Set parts remain during code extraction.
Зачем тут нужна какая-то предикативность для этой питушни? Если непредикативно, то можно еще кодогенерировать это как-то там, убрав термы для доказательств.
Я вообще ненастоящий сварщик(пусть снаут прокомментирует).
bormand 13.03.2021 11:10 # 0
j123123 13.03.2021 11:22 # 0
bormand 13.03.2021 11:26 # +1
bormand 13.03.2021 11:40 # 0
И вот эта фраза "The Set parts remain during code extraction" становится очень полезной.
CHayT 13.03.2021 11:46 # 0
Будто я настоящий, лол. Set к ZFC и вычислимым множествам отношения не имеет, это просто название
самого низкого уровня в иерархии вселенных.
CHayT 01.03.2021 21:26 # +2
Питух умеет юзать что Z3, что CVC4 через coqhammer. Шах и мат, аметисты.
j123123 02.03.2021 01:16 # +1
Там вот https://groups.google.com/g/metamath/c/b9k2nWOWJ-A напимер пишут
> Yes. https://arxiv.org/abs/1412.8091 details a translation from OpenTheory to Metamath, and https://arxiv.org/abs/1910.10703 has a translation from Metamath -> MM0 -> Lean + HOL. You have to map every axiom and inference rule of the source system to a theorem of the target system, and since most of these systems have a similar idea about what math is this is usually possible, modulo some axiomatic strength mismatches, which can usually be addressed by adding (reasonable, idiomatic) axioms to the target system to make up the difference.
Desktop 02.03.2021 01:25 # 0
bormand 02.03.2021 01:35 # +3
Вы все ещё хотите работать в гугле?
Desktop 02.03.2021 01:36 # +1
MAKAKA 02.03.2021 01:43 # +1
Desktop 02.03.2021 01:44 # 0
У красноглазых они во все поля и грузятся из архивов мгновенно
Pozor
MAKAKA 02.03.2021 01:48 # 0
Понятное дело, что в 2021 нужно грузить все сообщения сразу, да еще и загзипованные (или за бротлинные даже)
Desktop 02.03.2021 01:53 # 0
MAKAKA 02.03.2021 01:56 # 0
Фидо
https://groups.google.com/g/fido7.ru.fidonet.today
Юзнет
https://groups.google.com/g/alt.unix
Fike 02.03.2021 02:47 # 0
устали поди за двадцать пять лет-то
bormand 02.03.2021 15:03 # 0
j123123 13.03.2021 08:28 # 0
CHayT 13.03.2021 11:35 # +1
j123123 13.03.2021 11:57 # 0
guest6 01.03.2021 23:03 # 0
bormand 01.03.2021 23:55 # 0
MAKAKA 01.03.2021 23:57 # 0
bormand 02.03.2021 00:00 # +2
Rooster 02.03.2021 09:02 # 0
bormand 02.03.2021 10:24 # +2
3oJIoTou_xyu 02.03.2021 13:05 # +1
Desktop 02.03.2021 13:23 # +1
3oJIoTou_xyu 02.03.2021 13:23 # +1
bormand 02.03.2021 13:30 # +1
3oJIoTou_xyu 02.03.2021 13:32 # +1
MAKAKA 02.03.2021 13:57 # 0
3oJIoTou_xyu 02.03.2021 14:05 # +1
bormand 02.03.2021 16:18 # 0
TOPT 02.03.2021 16:39 # 0
bormand 02.03.2021 16:39 # 0
TOPT 02.03.2021 16:45 # 0
Desktop 02.03.2021 13:33 # 0
па рэстаранам
MAKAKA 02.03.2021 13:44 # 0
Rooster 02.03.2021 15:57 # 0
bormand 02.03.2021 16:03 # +3
TOPT 02.03.2021 16:07 # +2
TOPT 02.03.2021 16:03 # 0
bormand 02.03.2021 16:13 # +1
Всё-таки цели у этих инструментов немного разные.
Rooster 02.03.2021 16:58 # 0
TOPT 02.03.2021 17:02 # 0
bormand 02.03.2021 17:06 # 0
А у пианино кусок механики от настоящего пианино.
Fike 02.03.2021 17:07 # 0
TOPT 02.03.2021 17:09 # 0
Fike 02.03.2021 17:10 # 0
TOPT 02.03.2021 17:14 # 0
bormand 02.03.2021 17:10 # 0
TOPT 02.03.2021 17:18 # 0
bormand 02.03.2021 17:25 # 0
Да ну... Медленно и неудобно же. А народ в реалтайме эти крутилки вертит, чтобы из потока не выходить.
Это как тебя заставить хоткеи мышкой прожимать.
MAKAKA 02.03.2021 13:45 # +1
Fike 02.03.2021 14:50 # +1
Desktop 02.03.2021 14:53 # +1
MAKAKA 01.03.2021 23:57 # 0
Desktop 02.03.2021 01:26 # 0
j123123 02.03.2021 15:40 # +3
http://smtlib.cs.uiowa.edu/language.shtml
Если некий язык в качестве синтаксиса испольует S-expression, это не делает его лиспом.
Desktop 02.03.2021 15:41 # +2