Мне интересно, может ли кто-нибудь сказать мне разницу между Z3 и coq? Мне кажется, что coq является помощником проверки, поскольку он требует, чтобы пользователь заполнил шаги доказательства, тогда как у Z3 этого требования нет. Но похоже, что coq также имеет тактику авто, которая похожа на то, что делает Z3? Или, может быть, способность поиска доказательств в coq не так сильна, как Z3?
Разница между Z3 и coq
Ответ 1
Coq - это интерактивный теоретический прорыв (он же помощник доказательства). Он предоставляет язык для написания математических определений, алгоритмов и теорем. Он также обеспечивает среду для производства проверенных машин. Coq использовался для формализации математических теорем и обеспечения семантики языков программирования. Сегодня мы можем найти много статей в POPL, которые использовали Coq. Некоторые утверждают, что в будущем системы, такие как Coq, будут широко использоваться математиками. В статье есть убедительный аргумент в пользу формальных доказательств в математике. Недавно Жорж Гонтье использовал Coq для создания обзорного доказательства четырехцветной теоремы. Coq имеет небольшое доверенное ядро и обеспечивает высокую степень уверенности.
Z3 - это решение SMT (выполнимость по модулю). Его язык - это много отсортированная логика + логики первого порядка, такая как арифметика, бит-векторы, типы данных, массивы и т.д. Этот язык не так выразителен, как тот, который используется в Coq. Z3 также не поддерживает поддержку проверки, например Coq. Z3 в основном используется при тестировании и проверке программного обеспечения. Он также может использоваться для решения проблем, проблем планирования, головоломок и т.д. Огромный упор делается на поиск моделей (т.е. Решений) для выполнимых формул. В статье описаны многие приложения Z3 в Microsoft и в других местах. Z3 по существу является автоматическим доказательством теоремы. В Z3 тактика используется для определения специфических для домена стратегий. То есть настраиваемые решатели для проблем в конкретной области приложения. Z3 может создавать сертификаты/сертификаты, которые могут быть независимо проверены. Однако создание доказательств не является основным направлением проекта Z3. Более того, многие модули не поддерживают доказательство производства и должны быть отключены, когда запрос на создание запросов запрашивается пользователем. Z3 также был интегрирован в вспомогательные инструменты, такие как Isabelle, а некоторые работают над интеграцией Z3 в Coq. Идея состоит в том, чтобы иметь лучшее из обоих миров: очень выразительный язык и очень хорошая автоматизация. Z3 также можно рассматривать как логический логический механизм, который может быть встроен в более крупные приложения. На самом деле, это касается всех приложений Z3. Конечные пользователи не используют Z3 напрямую. Он скрыт внутри таких инструментов, как Isabelle, Pex, VCC и т.д. новый интерфейс Python для Z3 пытается изменить это.