Журналы
Email: Пароль: Войти Регистрация
E-mail: Dominique.Longin@irit.fr

Научный сотрудник Тулузского научно-исследовательского института информатики.

Статьи автора:

В работе рассматриваются вопросы логической формализации и решения задач с использованием автоматических систем проверки выполнимости. Предлагается автоматический транслятор TouIST, который позволяет генерировать логические формулы на основе простого полуформального описания проблемы. С его помощью оказывается возможным моделировать множество статических и динамических комбинаторных задач. Подчеркивается полезность системы в качестве вспомогательного средства для сопровождения курса логики и дискретной математики. Дополнительную выгоду пользователи смогут извлечь благодаря постоянному совершенствованию SAT, QBF и SMT-систем проверки выполнимости применительно к эффективному решению конкретных логических и комбинаторных проблем, таких, как планирование задач в области искусственного интеллекта. С. 13-25. (на англ.)

This work deals with logical formalization and problem solving using automated solvers. We present the automatic translator TouIST that provides a simple language to generate logical formulas from a problem description. Our tool allows us to model many static or dynamic combinatorial problems. All this can be very helpful as a teaching support for logics and discrete mathematics. Users will benefit from the regular improvements of SAT, QBF or SMT solvers in order to solve concrete logical and combinatorial problems efficiently, e.g., different classes of planning tasks in Artificial Intelligence.

Ключевые слова: системы проверки выполнимости, логика высказываний, логики высших порядков, дискретная математика, удобный пользовательский интерфейс.
Keywords: SAT solvers, propositional logic, higher order logic, discrete mathematics, user-friendly interface.
Для пополнения баланса выберите страну, оператора и отправьте СМС с кодом на указанный номер. Отправив одну смс, вы получаете доступ к одной статье.
Закрыть