Ограниченные положения Хорна

Предложения Хорна с ограничениями (CHC) представляют собой фрагмент логики первого порядка , применимый для проверки и синтеза программ . Предложения Хорна с ограничениями можно рассматривать как форму программирования логики с ограничениями . ^[1]

Определение [ править ]

Ограниченное предложение Хорна представляет собой формулу вида

$\phi \land P_{1}(\mathbf {x} _{1})\land \ldots \land P_{n}(\mathbf {x_{n}} )\to P(\mathbf {x} )$

где $\phi$ является ограничением в некоторой теории первого порядка, $P_{i}$ являются предикатами, а $\mathbf {x} _{i}$ являются универсально-квантифицированными переменными.

Разрешимость [ править ]

Выполнимость ограниченных предложений Хорна с ограничениями из линейной целочисленной арифметики неразрешима . ^[2]

Решатели [ править ]

Существует несколько автоматических решателей для CHC, ^[3] включая двигатель SPACER от Z3 . ^[4]

CHC-COMP — это ежегодный конкурс решателей CHC. ^[5] CHC-COMP проводится ежегодно с 2018 года.

Приложения [ править ]

Ограниченные предложения Хорна — удобный язык для описания проблем при верификации программ. ^[6] Верификатор SeaHorn для LLVM представляет условия проверки в виде ограниченных предложений Horn: ^[7] как и верификатор JayHorn для Java . ^[8]

Ссылки [ править ]

^ Анжелис, Эмануэле Де; Фиораванти, Фабио; Галлахер, Джон П.; Эрменегильдо, Мануэль В.; Петторосси, Альберто; Пройетти, Маурицио (ноябрь 2022 г.). «Анализ и преобразование ограниченных предложений Хорна для проверки программы» . Теория и практика логического программирования . 22 (6): 974–1042. arXiv : 2108.00739 . дои : 10.1017/S1471068421000211 . ISSN 1471-0684 . S2CID 236777105 . CHC синтаксически и семантически такие же, как программы логики ограничений.
^ Кокс, Джим; Макалун, Кен; Треткофф, Кэрол (1 июня 1992 г.). «Вычислительная сложность и логические языки программирования с ограничениями» . Анналы математики и искусственного интеллекта . 5 (2): 163–189. дои : 10.1007/BF01543475 . ISSN 1573-7470 . S2CID 666608 .
^ Блича, Мартин; Бритиков, Константин; Шарыгина, Наташа (2023). Энея, Константин; Лал, Акаш (ред.). Решатель рогов големов . Конспекты лекций по информатике. Чам: Springer Nature, Швейцария. стр. 209–223. дои : 10.1007/978-3-031-37703-7_10 . ISBN 978-3-031-37703-7 . {{cite book}}: |journal= игнорируется ( помогите )
^ Гурфинкель, Арье (2022). Шохам, Шарон; Визель, Якир (ред.). Верификация программы с использованием ограниченных предложений Horn (приглашенный доклад) . Конспекты лекций по информатике. Том. 13371. Чам: Springer International Publishing. стр. 19–29. дои : 10.1007/978-3-031-13185-1_2 . ISBN 978-3-031-13185-1 . {{cite book}}: |journal= игнорируется ( помогите )
^ Федюкович, Григорий; Рюммер, Филипп (10 сентября 2021 г.). «Отчет о соревновании: CHC-COMP-21». Электронные труды по теоретической информатике . 344 : 91–108. arXiv : 2109.04635v1 . дои : 10.4204/EPTCS.344.7 . S2CID 221132231 .
^ Бьёрнер, Николай; Гурфинкель, Арье; Макмиллан, Кен; Рыбальченко Андрей (2015), Беклемишев Лев Д.; Бласс, Андреас; Дершовиц, Нахум; Финкбайнер, Бернд (ред.), «Решатели предложений Хорна для проверки программ» , «Области логики и вычислений II: очерки, посвященные Юрию Гуревичу по случаю его 75-летия» , конспекты лекций по информатике, Cham: Springer International Publishing, стр. . 24–51, номер домена : 10.1007/978-3-319-23534-9_2 , ISBN. 978-3-319-23534-9 , получено 7 декабря 2023 г.
^ Гурфинкель, Арье; Кахсай, Темесген; Комуравелли, Анвеш; Навас, Хорхе А. (2015). Кренинг, Дэниел; Пасэряну, Корина С. (ред.). Система проверки SeaHorn . Конспекты лекций по информатике. Чам: Международное издательство Springer. стр. 343–361. дои : 10.1007/978-3-319-21690-4_20 . ISBN 978-3-319-21690-4 . {{cite book}}: |journal= игнорируется ( помогите )
^ Кахсай, Темесген; Рюммер, Филипп; Санчес, Уаскар; Шеф, Мартин (2016). Чаудхури, Сварат; Фарзан, Азаде (ред.). JayHorn: платформа для проверки Java-программ . Конспекты лекций по информатике. Чам: Международное издательство Springer. стр. 352–358. дои : 10.1007/978-3-319-41528-4_19 . ISBN 978-3-319-41528-4 . {{cite book}}: |journal= игнорируется ( помогите )

[1] Анжелис, Эмануэле Де; Фиораванти, Фабио; Галлахер, Джон П.; Эрменегильдо, Мануэль В.; Петторосси, Альберто; Пройетти, Маурицио (ноябрь 2022 г.). «Анализ и преобразование ограниченных предложений Хорна для проверки программы» . Теория и практика логического программирования . 22 (6): 974–1042. arXiv : 2108.00739 . дои : 10.1017/S1471068421000211 . ISSN 1471-0684 . S2CID 236777105 . CHC синтаксически и семантически такие же, как программы логики ограничений.

[2] Кокс, Джим; Макалун, Кен; Треткофф, Кэрол (1 июня 1992 г.). «Вычислительная сложность и логические языки программирования с ограничениями» . Анналы математики и искусственного интеллекта . 5 (2): 163–189. дои : 10.1007/BF01543475 . ISSN 1573-7470 . S2CID 666608 .

[3] Блича, Мартин; Бритиков, Константин; Шарыгина, Наташа (2023). Энея, Константин; Лал, Акаш (ред.). Решатель рогов големов . Конспекты лекций по информатике. Чам: Springer Nature, Швейцария. стр. 209–223. дои : 10.1007/978-3-031-37703-7_10 . ISBN 978-3-031-37703-7 . {{cite book}}: |journal= игнорируется ( помогите )

[4] Гурфинкель, Арье (2022). Шохам, Шарон; Визель, Якир (ред.). Верификация программы с использованием ограниченных предложений Horn (приглашенный доклад) . Конспекты лекций по информатике. Том. 13371. Чам: Springer International Publishing. стр. 19–29. дои : 10.1007/978-3-031-13185-1_2 . ISBN 978-3-031-13185-1 . {{cite book}}: |journal= игнорируется ( помогите )

[5] Федюкович, Григорий; Рюммер, Филипп (10 сентября 2021 г.). «Отчет о соревновании: CHC-COMP-21». Электронные труды по теоретической информатике . 344 : 91–108. arXiv : 2109.04635v1 . дои : 10.4204/EPTCS.344.7 . S2CID 221132231 .

[6] Бьёрнер, Николай; Гурфинкель, Арье; Макмиллан, Кен; Рыбальченко Андрей (2015), Беклемишев Лев Д.; Бласс, Андреас; Дершовиц, Нахум; Финкбайнер, Бернд (ред.), «Решатели предложений Хорна для проверки программ» , «Области логики и вычислений II: очерки, посвященные Юрию Гуревичу по случаю его 75-летия» , конспекты лекций по информатике, Cham: Springer International Publishing, стр. . 24–51, номер домена : 10.1007/978-3-319-23534-9_2 , ISBN. 978-3-319-23534-9 , получено 7 декабря 2023 г.

[7] Гурфинкель, Арье; Кахсай, Темесген; Комуравелли, Анвеш; Навас, Хорхе А. (2015). Кренинг, Дэниел; Пасэряну, Корина С. (ред.). Система проверки SeaHorn . Конспекты лекций по информатике. Чам: Международное издательство Springer. стр. 343–361. дои : 10.1007/978-3-319-21690-4_20 . ISBN 978-3-319-21690-4 . {{cite book}}: |journal= игнорируется ( помогите )

[8] Кахсай, Темесген; Рюммер, Филипп; Санчес, Уаскар; Шеф, Мартин (2016). Чаудхури, Сварат; Фарзан, Азаде (ред.). JayHorn: платформа для проверки Java-программ . Конспекты лекций по информатике. Чам: Международное издательство Springer. стр. 352–358. дои : 10.1007/978-3-319-41528-4_19 . ISBN 978-3-319-41528-4 . {{cite book}}: |journal= игнорируется ( помогите )

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]