Необходимо зарегистрироваться, чтобы получить доступ к полным текстам статей и выпусков журналов!
- Название статьи
- ДОКАЗАТЕЛЬСТВО ТЕОРЕМ С ПОМОЩЬЮ КВАНТОВОГО ГЕНЕРАТОРА ТЕСТОВ
- Авторы
- Правильщиков Павел Алексеевич fca07@mail.ru, канд. техн. наук; ведущий научный сотрудник, ФГБУН "Институт проблем управления им. В. А. Трапезникова РАН", Москва, Россия
- В разделе
- ИНФОРМАЦИОННЫЕ ТЕХНОЛОГИИ В РЕШЕНИИ ЗАДАЧ ПРОИЗВОДСТВА
- Ключевые слова
- автоматическое доказательство теорем / квантовые компьютеры / квантовые ускорители / квантовые алгоритмы / проблема верификации программ / проблема формальной верификации проектов БИС / SAT-проблема
- Год
- 2015 номер журнала 3 Страницы 77 - 87
- Индекс УДК
- 517
- Код EDN
- Код DOI
- Тип статьи
- Научная статья
- Аннотация
- Рассмотрена проблема автоматического доказательства теорем с использованием такой модели вычислений, как квантовый генератор тестов (КГТ), описание которого и приводится. Предложено использовать квантовый ускоритель, моделью которого является КГТ, для автоматического доказательства теорем. Показано, что автоматизация доказательства теорем является важным и неотъемлемым элементом верификации современных БИС и создания программных комплексов, к надежности которых предъявляются повышенные требования. Утверждается, что автоматическое доказательство теорем может быть сведено к решению задачи выполнимости некоторого логического уравнения.
- Полный текст статьи
- Необходимо зарегистрироваться, чтобы получить доступ к полным текстам статей и выпусков журналов!
- Список цитируемой литературы
-
Пархоменко П. П., Правильщиков П. А. Диагностирование программного обеспечения // Автоматика и телемеханика. 1980. № 1. С. 103-121.
Андерсон Р. Доказательство правильности программ: Пер. с англ. - М.: Мир, 1982. - 168 с.
Pixley C. Formal Verification of Commercial Integrated Circuits // IEEE Design & Test of Computer. 2001. V. 18. No. 4. P. 4-5.
Правильщиков П. А. Проблема верификации БИС и ее решение путем использования "вычислительного решета" на основе закона сохранения перебора // Оборонный комплекс - научно-техническому прогрессу России. 2002. № 4. С. 45-61.
Ньюэлл А., Саймон Г., Шоу Дж. GPS-программа, моделирующая процесс человеческого мышления. В кн. "Вычислительные машины и мышление" // Под ред. Э. Фейгенбаума и Дж. Фельдмана, - М.: "МИР", 1967. - 464 с.
Поспелов Д. А. Фантазия или наука: на пути к искусственному интеллекту. - М.: Наука. Гл. Ред. Физико-математической литературы, 1982. - 224 с.
Правильщиков П. А. Закон сохранения перебора и естественный параллелизм D-алгоритмов для построения тестов и моделирования в технической диагностике // Автоматика и телемеханика. 2004. № 7. С. 156-199.
Правильщиков П. А. Квантовый параллелизм и новая модель вычислений / Тр. 12-го Всероссийского совещания по проблемам управления - ВСПУ-2014. - М.: Институт проблем управления им. Трапезникова РАН. 2014. С. 7319-7334. ISBN 978-5-91450-151-5. № госрегистрации: 0321401153.
Правильщиков П. А. Квантовый параллелизм и решение уравнений в задачах управления на базе новой модели вычислений / Тр. 12-го Всероссийского совещания по проблемам управления - ВСПУ-12. - М.: Институт проблем управления им. Трапезникова РАН. 2014. С. 7335-7351. ISBN 978-5-91450-151-5. № госрегистрации: 0321401153.
Менский М. Б. Квантовая механика: новые эксперименты, новые приложения и новые формулировки старых вопросов // Успехи физических наук. 2000. Т. 170. С. 631-648.
Валиев К. А., Кокин А. А. Квантовые компьютеры: надежды и реальность. - Москва-Ижевск: НИЦ «Регулярная и хаотическая динамика», 2002. - 320 с.
Богданов Ю. И., Кокин А. А., Лукичев В. Ф., Орликовский А. А., Семенихин И. А., Чернявский А. Ю. Квантовая механика и развитие информационных технологий / Тр. МСКФ-2011.
Roth J. P. Diagnosis of automata failures: a calculus and method // IBM Journal of Research and Development. 1966. No 7 (July). P. 18-32.
Turing A. M. On Computable Numbers, with an Application to Entscheidungsproblem // Proc. London Math Society, 42:230-265, 1936.
Хопкрофт Дж., Мотвани Р., Ульман Д. Введение в теорию автоматов, языков и вычислений (Introduction to Automata Theory, Languages, and Computation). - М.: «Вильямс», 2002. -528 с.
Топорков В. В. Модели распределенных вычислений. - М.: Физматлит, 2004. - 320 с.
Прескил Дж. Квантовая информация и квантовые вычисления. - Москва-Ижевск: ИКИ (НИЦ Регулярная и хаотическая динамика), 2008. - 464 с.
Нильсен М., Чанг И. Квантовые вычисления и квантовая информация: Пер. с англ.- М.: Мир, 2006. - 824 с.
Bennett C. H., DiVincenzo D. P. "Quantum computing: Towards an engineering era?" // Nature. 1995. V. 377. No 6548. P. 389-390.
Антес Г. Перспективы субатомных ИТ // Computerworld. 2006. № 37. P. 43-47.
Бортаковский А. С., Пантелеев А. В. Линейная алгебра в примерах и задачах. - М.: Высш. шк., 2010. - 591 с.
Перри Р. Элементарное введение в квантовые вычисления / Пер. с англ.: Учебное пособие / Р. Перри. - Долгопрудный: Издательский Дом «Интеллект», 2015. - 208 с.
Lanyon B. P., Barbieri M., Almeida M. P., Jennewein T., Ralph T. C., Resch K. J., Pryde G. J., O'Brien J. L., Gilchrist A., White A. G. Quantum computing using shortcuts through higher dimensions // Phys. Rev. Lett. 2008. Vol. 101. No. 2. P. 2-7.
Lanyon B. P., Barbieri M., Almeida M. P. and all. Simplifying quantum logic using higher-dimensional Hilbert spaces // Nature Physics. Vol. 5. No. 2. (2008). P. 134-140.
- Купить