[Берклиевский семинар] Бенджамин Браст-Макки | Программная семантика

Название: Программная семантика
Аннотация: В этом докладе представлена ​​программная методология, использующая разработанное мной программное обеспечение для проверки моделей, позволяющее быстро создавать прототипы семантических теорий.
Я начну с представления стандартной методологии в философской логике, чтобы выделить ряд недостатков, которые обусловили необходимость программной методологии. Затем я представлю средство проверки моделей, которое использует решатель SMT Z3 для исключения конечных контрмоделей заданного пользователем размера, предоставляя доказательства того, что логическое следствие не имеет контрмоделей, если на самом деле их нет. Реализация программной семантики с помощью средства проверки моделей расширяет стандартную методологию, упрощая процесс исследования и создания прототипов новых семантических теорий.
Помимо облегчения изучения сложных семантических теорий, средство проверки моделей предоставляет ресурсы для загрузки семантических теорий в TheoryLib для облегчения сотрудничества. Программные семантические теории также являются модульными, что позволяет легко комбинировать и сравнивать их, позволяя пользователям изучать взаимодействия в языках со многими операторами. Более того, вычислимость семантической теории обеспечивает объективную меру, которую можно сопоставить с другими теоретическими достоинствами.
Хотя средство проверки моделей является универсальным инструментом для работы в семантике, его применение в гипертенсиональной семантике особенно естественно, учитывая возросшую сложность этих семантических систем. Вместо недостатка я буду характеризовать хорошо обоснованные формы теоретической сложности как признак зрелости семантики как дисциплины. Именно в поддержку как будущего развития, так и доступности семантики средство проверки моделей призвано внести свой вклад. Доклад завершится краткой демонстрацией, чтобы сделать рабочий процесс более наглядным.
Дата: 17.06.2025

https://topos.institute/events/berkel...