- 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)
Follow us!
А что делать, если они не осиливают? Какой-то способ вручную пнуть в нужном направлении есть?
Блин, я вот кстати х.з. как в петухе записать a и b -- неведомая хуйня одного сорта. Походу тут совсем другая логика юзается.
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.
Зачем тут нужна какая-то предикативность для этой питушни? Если непредикативно, то можно еще кодогенерировать это как-то там, убрав термы для доказательств.
Я вообще ненастоящий сварщик(пусть снаут прокомментирует).
И вот эта фраза "The Set parts remain during code extraction" становится очень полезной.
Будто я настоящий, лол. Set к ZFC и вычислимым множествам отношения не имеет, это просто название
самого низкого уровня в иерархии вселенных.
Питух умеет юзать что Z3, что CVC4 через coqhammer. Шах и мат, аметисты.
Там вот 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.
Вы все ещё хотите работать в гугле?
У красноглазых они во все поля и грузятся из архивов мгновенно
Pozor
Понятное дело, что в 2021 нужно грузить все сообщения сразу, да еще и загзипованные (или за бротлинные даже)
Фидо
https://groups.google.com/g/fido7.ru.fidonet.today
Юзнет
https://groups.google.com/g/alt.unix
устали поди за двадцать пять лет-то
па рэстаранам
Всё-таки цели у этих инструментов немного разные.
А у пианино кусок механики от настоящего пианино.
Да ну... Медленно и неудобно же. А народ в реалтайме эти крутилки вертит, чтобы из потока не выходить.
Это как тебя заставить хоткеи мышкой прожимать.
http://smtlib.cs.uiowa.edu/language.shtml
Если некий язык в качестве синтаксиса испольует S-expression, это не делает его лиспом.