Похоже, Джордж Гонтье и его сотрудники закончили формализацию теоремы нечетного порядка . В своей более ранней работе над теоремой о четырех цветах Гонтье изобрел кучу новых алгоритмов (в основном, вариантов BDD и графовых алгоритмов), которые были особенно пригодны для формальной проверки....
Этот вопрос был перенесен из переполнения стека, потому что на него можно ответить в теоретической информатике стека обмена. Мигрировал 8 лет назад . Учитывая, что соответствие Карри-Говарда так широко распространено / расширено, есть ли разница между доказательствами и программами (или между...
Можно ли перевести булеву формулу B в эквивалентное соединение выражений Хорна? Статья в Википедии о HornSAT, похоже, подразумевает, что это так, но я не смог найти какую-либо ссылку. Обратите внимание, что я имею в виду не «за полиномиальное время», а скорее...
Считайте, что этот вопрос решен. Я не буду выбирать лучший ответ, поскольку все они внесли свой вклад в мое понимание темы. Я не уверен, какую пользу мы получаем, формально определяя семантику логики предикатов. Но я вижу ценность в формальном доказательстве. Я хочу сказать, что нам не нужна...
Я много читал о системах типов и тому подобное, и я примерно понимаю, почему они были введены (чтобы разрешить парадокс Рассела). Я также примерно понимаю их практическую значимость в языках программирования и системах доказательства. Однако я не совсем уверен, что мое интуитивное представление о...
ACSL (Ansi C Specification Language) - это спецификация для кода C, снабженная специальными комментариями, которая позволяет формально проверять код C. Я не рассматривал это, но я полагаю, что формальные методы, используемые в верификаторах ACSL , будут похожи на Hoare Logic. Однако для чисто...
В своем ответе на этот вопрос , Стефан Хименес указал мне на алгоритм нормализации полиномиальное время для доказательств в линейной логике. В доказательстве в статье Жирара используются сети доказательств, которые являются аспектом линейной логики, о которой я на самом деле не очень много знаю. Я...
Типы и языки программирования довольно сильно фокусируются на подтипах, но, насколько я могу судить, подтипы не кажутся особенно фундаментальными. Дает ли подтип что-то большее, чем зависимые типы? Работа с зависимыми типами должна быть более трудоемкой, поэтому я могу понять, почему подтипы могут...
Я хочу сделать первый SAT решатель. Я знаю соревнования SAT и конференцию SAT, и на эту тему очень много работ. Я стартер, перегруженный стартер. С чего мне начать? В конце концов я хочу продвинуть современное состояние. Мне нужен совет специалиста о том, как начать, чтобы я не тратил свое время на...
Из того, что я понимаю (что очень мало, поэтому, пожалуйста, поправьте меня, где я ошибаюсь!), Теория языков программирования часто связана с "интуиционистскими" доказательствами. В моей собственной интерпретации, подход требует, чтобы мы серьезно относились к последствиям вычислений для логики и...
Недавно я видел несколько статей об arxiv, которые ссылаются на систему доказательств под названием сумма квадратов. Может кто-нибудь объяснить, что такое доказательство суммы квадратов и почему такие доказательства важны / интересны? Как они связаны с другими алгебраическими системами...
В настоящее время я преподаю небольшой курс (четыре двухчасовых лекции на уровне магистратуры) по логическим методам в безопасности , хотя название « Формальные методы в безопасности» может быть более подходящим. В нем кратко рассматриваются следующие темы (с соответствующими логическими методами):...
Кто-нибудь знает ссылки, в которых четко прописана связь между алгоритмом объединения и гауссовым исключением? Меня особенно интересует связь между треугольными заменами и LU-разложениями. Уэйн Снайдер и Джин Галлиер упоминают эту аналогию в своей статье « Возвращение к объединению высшего порядка:...
Я читал, что изначально Черч предложил -calculus как часть своей статьи «Постулаты логики» (которая читается плотно). Но Клини доказал свою «систему» непоследовательной, после чего Черч извлек соответствующие вещи для своей работы по «эффективной вычислимости» и отказался от своей предыдущей...
Рассмотрим следующие рассуждения: Пусть обозначим сложность Колмогорова из строки . Теорема Чайтена о неполноте гласит, чтохК( х )K(x)K(x)Иксxx для любой последовательной и достаточно сильной формальной системы , существует постоянную (зависящую только от формальной системы и ее языка), что для...
Я видел (и слышал), что он утверждал, что безопасно добавить классическую аксиому исключенного среднего к Coq, но я не могу найти документ, подтверждающий это утверждение. Статьи, которые я вижу в списке в вики Coq о исключенной середине, показывают несоответствие с нечетким множеством....
Важной целью формальных методов является доказательство правильности систем, либо автоматизированными, либо управляемыми человеком средствами. Тем не менее, кажется, что даже если вы можете предоставить подтверждение правильности, вы НЕ МОЖЕТЕ гарантировать, что система не выйдет из строя....
Самостоятельная ссылка на проблему P / NP иногда подчеркивалась как барьер для ее разрешения, см., Например, статью Скотта Ааронсона, является ли P против NP формально независимой ? Одним из многих возможных решений P / NP будет демонстрация того, что проблема формально не зависит от ZFC или...
Недавно Дана Скотт предложила стохастическое лямбда-исчисление, попытку ввести вероятностные элементы в (нетипизированное) лямбда-исчисление на основе семантики, называемой графовой моделью. Вы можете найти его слайды в Интернете, например, здесь и его статью в журнале прикладной логики , том. 12...
Есть ли обзор алгоритмов вычисления интерполантов? Как насчет работ только по одному алгоритму? Случай я больше всего интересует = ¬ р ∧ д и С = д , а также ограничение , что интерполянт настолько мал , насколько это возможно. (Мне известна статья Макмиллана 2005 года , в которой описывается, как...