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

Фрагмент логики первого порядка

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

Определение

Ограниченное предложение Хорна — это формула вида

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

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

Разрешимость

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

Решатели

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

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

Приложения

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

Ссылки

^ Angelis, Emanuele De; Fioravanti, Fabio; Gallagher, John P.; Hermenegildo, Manuel V.; Pettorossi, Alberto; Proietti, Maurizio (ноябрь 2022 г.). «Анализ и преобразование ограниченных предложений Хорна для проверки программ». Теория и практика логического программирования . 22 (6): 974–1042 . arXiv : 2108.00739 . doi : 10.1017/S1471068421000211 . ISSN 1471-0684. S2CID 236777105. CHC синтаксически и семантически совпадают с программами логики ограничений.
^ Кокс, Джим; МакАлун, Кен; Треткофф, Кэрол (1992-06-01). «Вычислительная сложность и языки программирования логики ограничений». Annals of Mathematics and Artificial Intelligence . 5 (2): 163– 189. doi :10.1007/BF01543475. ISSN 1573-7470. S2CID 666608.
^ Blicha, Martin; Britikov, Konstantin; Sharygina, Natasha (2023). "The Golem Horn Solver". В Enea, Constantin; Lal, Akash (ред.). Computer Aided Verification . Lecture Notes in Computer Science. Cham: Springer Nature Switzerland. стр. 209–223 . doi :10.1007/978-3-031-37703-7_10. ISBN 978-3-031-37703-7.
^ Гурфинкель, Ари (2022). «Проверка программ с ограниченными предложениями Хорна (приглашенная статья)». В Шохам, Шарон; Визель, Якир (ред.). Компьютерная проверка . Конспект лекций по информатике. Том 13371. Чам: Springer International Publishing. стр. 19– 29. doi : 10.1007/978-3-031-13185-1_2. ISBN 978-3-031-13185-1.
^ Федюкович, Григорий; Рюммер, Филипп (2021-09-10). «Отчет о конкурсе: CHC-COMP-21». Электронные труды по теоретической информатике . 344 : 91–108 . arXiv : 2109.04635v1 . doi : 10.4204/EPTCS.344.7. S2CID 221132231.
^ Бьёрнер, Николай; Гурфинкель, Ари; Макмиллан, Кен; Рыбальченко, Андрей (2015), Беклемишев, Лев Д.; Бласс, Андреас; Дершовиц, Нахум; Финкбайнер, Бернд (ред.), «Решатели уравнений Хорна для проверки программ», Поля логики и вычислений II: Эссе, посвященные Юрию Гуревичу по случаю его 75-летия , Конспект лекций по информатике, Cham: Springer International Publishing, стр. 24–51 , doi :10.1007/978-3-319-23534-9_2, ISBN 978-3-319-23534-9, получено 2023-12-07
^ Гурфинкель, Ари; Кахсай, Темесген; Комуравелли, Анвеш; Навас, Хорхе А. (2015). «The SeaHorn Verification Framework». В Kroening, Daniel; Păsăreanu, Corina S. (ред.). Computer Aided Verification . Lecture Notes in Computer Science. Cham: Springer International Publishing. стр. 343–361 . doi :10.1007/978-3-319-21690-4_20. ISBN 978-3-319-21690-4.
^ Кахсай, Темесген; Рюммер, Филипп; Санчес, Уаскар; Шеф, Мартин (2016). «JayHorn: платформа для проверки программ Java». В Чаудхури, Сварат; Фарзан, Азаде (ред.). Компьютерная проверка . Конспекты лекций по информатике. Чам: Международное издательство Springer. стр. 352–358 . doi : 10.1007/978-3-319-41528-4_19. ISBN 978-3-319-41528-4.

[1] Angelis, Emanuele De; Fioravanti, Fabio; Gallagher, John P.; Hermenegildo, Manuel V.; Pettorossi, Alberto; Proietti, Maurizio (ноябрь 2022 г.). «Анализ и преобразование ограниченных предложений Хорна для проверки программ». Теория и практика логического программирования . 22 (6): 974–1042 . arXiv : 2108.00739 . doi : 10.1017/S1471068421000211 . ISSN 1471-0684. S2CID 236777105. CHC синтаксически и семантически совпадают с программами логики ограничений.

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

[3] Blicha, Martin; Britikov, Konstantin; Sharygina, Natasha (2023). "The Golem Horn Solver". В Enea, Constantin; Lal, Akash (ред.). Computer Aided Verification . Lecture Notes in Computer Science. Cham: Springer Nature Switzerland. стр. 209–223 . doi :10.1007/978-3-031-37703-7_10. ISBN 978-3-031-37703-7.

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

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

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

[7] Гурфинкель, Ари; Кахсай, Темесген; Комуравелли, Анвеш; Навас, Хорхе А. (2015). «The SeaHorn Verification Framework». В Kroening, Daniel; Păsăreanu, Corina S. (ред.). Computer Aided Verification . Lecture Notes in Computer Science. Cham: Springer International Publishing. стр. 343–361 . doi :10.1007/978-3-319-21690-4_20. ISBN 978-3-319-21690-4.

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