Я сам изучаю Автоматизированное доказательство теорем / SMT-решатели / Помощники по проверке и выкладываю серию вопросов о процессе, начинающемся здесь. Обратите внимание, что эти темы нелегко усваиваются без знания (математической) логики. Если у вас есть проблемы с основными терминами,...
Рассмотрим индуктивный тип, который имеет некоторые рекурсивные вхождения во вложенном, но строго положительном месте. Например, деревья с конечным ветвлением с узлами, использующими общую структуру данных списка для хранения дочерних элементов. Inductive LTree : Set := Node : list LTree ->...
Я сам изучаю Автоматизированное доказательство теорем / SMT-решатели / Помощники по проверке и выкладываю серию вопросов о процессе, начинающемся здесь . Какие релевантные автоматические доказатели теорем? Я нашел обзор доказателей теорем Это все еще актуально? Какие из них все еще очень активны,...
Я сам изучаю Автоматизированное доказательство теорем / SMT-решатели / Помощники по проверке и выкладываю серию вопросов о процессе, начиная здесь . Я продолжаю читать об Алгоритме Объединения . Что это такое и почему это так важно для двигателей вывода ? Почему это так важно для информатики?...
Кто-нибудь когда-либо писал систему (программное обеспечение или подробное объяснение на бумаге с простыми примерами), которая генерирует компьютерные программы? Я ввожу и он создает программу, которая перечисляет простые числа меньше 10. P r i m e ( x ) просто определяется как 1 < x ∧ ∄ Aпг я м...
Я сам изучаю Автоматизированное доказательство теорем / SMT-решатели / Помощники по проверке и выкладываю серию вопросов о процессе, начиная здесь . Почему автоматические средства проверки теорем, то есть ACL2 , и решатели SMT не нуждаются в помощи человека, в то время как помощники по...
Я самообучающийся помощник по доказательствам и решил начать с некоторых базовых доказательств и продолжить работу. Поскольку доказательства основаны на других доказательствах и поэтому образуют иерархию, существует ли хранилище иерархии доказательств? Я знаю, что могу выбрать конкретного помощника...
В комментарии к Learning F #: Какие книги, использующие другие языки программирования, можно перевести на F # для изучения функциональных концепций? Макарий заявил: Обратите внимание, что подход «CPS» нанес большой вред производительности в SML / NJ. Его модель физической оценки нарушает слишком...
Фон Я обучаю помощи, Coq, самостоятельно. До сих пор я закончил читать Coq Ива Берто в спешке . Теперь моя цель состоит в том, чтобы доказать некоторые базовые результаты, касающиеся натуральных чисел, что завершается так называемым алгоритмом деления. Однако я столкнулся с некоторыми препятствиями...
Учитывая это: Язык с очень выразительными системами типов (например, Idris ) также может иметь механизмы выхода, такие как интерфейсы сторонних функций / unsafePerformIO. Существуют помощники по проверке, которые можно использовать для доказательства некоторых свойств программы, написанной на...