#матлог #учёба #спецсеминар #не_мехмат #МИАН #ТД

Семинар отдела математической логики МИАН, Logic Online Seminar (www.mathnet.ru/rus/conf876), понедельник 28 сентября 16:00 MSK (UTC+3), ауд. 313 МИАН + Kontur Talk

28.09.2026 Мати Рейнович Пентус (мехмат МГУ):
Сети доказательства для мультипликативной некоммутативной линейной логики без констант (очный доклад)

Рассматривается бесконстантный мультипликативный фрагмент некоммутативной линейной логики. Для этого фрагмента известен критерий выводимости в терминах сетей доказательства с областями. Такую сеть доказательства можно определить как биективный ациклический каркас доказательства. Каркасом доказательства (proof structure) является плоский граф, образованный деревом разбора формулы и аксиомными рёбрами, а сеть доказательства (proof net) — это каркас доказательства, удовлетворяющий дополнительным аксиомам.

Мы покажем, что каждый биективный каркас доказательства, содержащий цикл, обязательно содержит цикл специального регулярного вида. Отсюда следует более удобный критерий выводимости: формула выводима тогда и только тогда, когда для неё существует биективный каркас доказательства, где нет циклов этого специального вида.