Язык TouIST для логики высказываний и дискретной математики. В помощь преподавателям и студентам
Аннотация
В работе рассматриваются вопросы логической формализации и решения задач с использованием автоматических систем проверки выполнимости. Предлагается автоматический транслятор TouIST, который позволяет генерировать логические формулы на основе простого полуформального описания проблемы. С его помощью оказывается возможным моделировать множество статических и динамических комбинаторных задач. Подчеркивается полезность системы в качестве вспомогательного средства для сопровождения курса логики и дискретной математики. Дополнительную выгоду пользователи смогут извлечь благодаря постоянному совершенствованию SAT, QBF и SMT-систем проверки выполнимости применительно к эффективному решению конкретных логических и комбинаторных проблем, таких, как планирование задач в области искусственного интеллекта.
Литература
B. Buss and J. Nordstr¨om, “Proof Complexity and SAT Solving,” in Handbook of Satisfiability, 2nd ed., A. Biere et al., eds, Amsterdam: IOS Press, 2021, ch. 7, pp. 233–350; doi: 10.3233/FAIA200990
G. S. Tseitin, “On the Complexity of Derivation in Propositional Calculus,” in Automation of Reasoning: 2: Classical Papers on Computational Logic 1967–1970, Berlin, Heidelberg: Springer, 1983, pp. 466–483; doi: 10.1007/978-3-642-81955-1_28
Z. Luo and S. Soloviev, “Dependent Event Types,” in Proc. of Logic, Language, Information, and Computation - 24th Int. Workshop, WoLLIC 2017, London, UK, July 18-21, 2017, pp. 216–228; doi: 10.1007/978-3-662-55386-2_15
J. Barwise, “Scenes and other situations,” Journal of Philosophy, vol. 78, no. 7, pp. 369–397, 1981; doi: 10.2307/2026481
D. Kroening and O. Strichman, Decision Procedures — An Algorithmic Point of View, 2nd Ed., Berlin: Springer, 2016; doi: 10.1007/978-3-662-50497-0
A. Biere, “Resolve and Expand,” in Proc. of the 7th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT’04), Vancouver, BC, Canada, May 10–13, 2004, 2005, pp. 59–70.
H. A. Kautz and B. Selman, “Planning as Satisfiability,” in Proc. of the 10th European Conference on Artificial Intelligence, ECAI-92, Vienna, Austria, August 3–7, 1992, pp. 359–363.
J. Rintanen, “Asymptotically Optimal Encodings of Conformant Planning in QBF,” in Proc. of the Twenty-Second AAAI Conference on Artificial Intelligence, July 22–26, 2007, Vancouver, British Columbia, Canada,, 2007, pp. 1045–1050.
J. Rintanen, “Discretization of Temporal Models with Application to Planning with SMT,” in Proc. of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA., 2015, pp. 3349–3355.
J. Shin and E. Davis, “Processes and continuous change in a SAT-based planner,” Artificial Intelligence, vol. 166, no. 1–2, pp. 194–253, 2005; doi: 10.1016/j.artint.2005.04.001
F. Maris and P. Regnier, “TLP-GP: New Results on Temporally-Expressive Planning Benchmarks,” in ˊProc. of the 20th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2008), November 3–5, Dayton, Ohio, USA, 2008, vol. 1, pp. 507–514; doi: 10.1109/ICTAI.2008.90
O. Gasquet, D. Longin, F. Mari, P. Regnier, and M. Valais, “Compact Tree Encodings for Planning as QBF,” Inteligencia Artificial (Ibero-American Journal of Artificial Intelligence), vol. 21(62), pp. 103–114, 2018; doi: 10.4114/intartif.vol21iss62pp103-113
Материал публикуется под лицензией:
