Я планирую несколько экспериментов по символьному выполнению кода C, используя готовый SMT-решатель, и мне интересно, какой решатель использовать; глядя на например. участники конкурса SMT и, принимая только системы с открытым исходным кодом, сужают...

Пытаясь понять, что такое Coq, я оказался в ситуации, когда мне по сути нужно доказать, что a=b -> nat_compare a b = Eq . Я могу получить удобное начало, выполнив: Coq < Theorem foo: forall (a:nat) (b:nat), a=b->nat_compare a b=Eq. 1...

Что такое "шаблон типа частного" в Изабель? Я не нашел объяснений в Интернете.

Я пытаюсь написать тестовый код, чтобы проверить, действительно ли plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a доказывает a + b = b + a на натуральных числах, то есть код не подделывает их, используя типизированные отверстия,...

Я только начинаю играть с Z3 самостоятельно, и я подумал, что одним интересным экспериментом будет создание поля из 3 элементов. Поэтому я объявил свое поле S скалярным перечислением трех элементов, A, B, C, и начал постепенно добавлять аксиомы...

Я работаю над доказательством корректности компилятора в основах языка программирования и часами чесал в затылке, прежде чем сдаться и применить это решение, которое я нашел в сети (...

Я пытаюсь доказать следующую теорему после формализации лямбда-исчисления с индексами Дебройна и заменой в Coq. Theorem atom_equality : forall e : expression , forall x : nat, (beta_reduction (Var x) e) -> (e = Var x). и это определения...