Вычислительная логика
 | Эта статья нуждается в дополнительных цитатах для проверки . ( апрель 2015 г. ) |
Вычислительная логика — это использование логики для выполнения вычислений или рассуждений о них . Она имеет такое же отношение к информатике и технике, как математическая логика относится к математике и как философская логика относится к философии . Это альтернативный термин для « логики в информатике ».
Вычислительная логика также стала ассоциироваться с логическим программированием , поскольку большая часть ранних работ в области логического программирования в начале 1970-х годов также проводилась на факультете вычислительной логики в Эдинбурге. В начале 1990-х годов он был повторно использован для описания работы над расширением логического программирования в рамках проекта фундаментальных исследований ЕС «Компулог» и связанной с ним Сети передового опыта. Кшиштоф Апт , который был координатором проекта фундаментальных исследований Compulog-II, повторно использовал и обобщил этот термин, когда в 2000 году основал организацию ACM Transactions on Computational Logic и стал ее первым главным редактором.
Термин «вычислительная логика» приобрел известность с основанием организации ACM Transactions on Computational Logic в 2000 году. [1] Однако этот термин был введен гораздо раньше Дж. А. Робинсоном в 1970 году. [2] Это выражение используется во втором абзаце со сноской, в которой утверждается, что «вычислительная логика» «определенно является лучшей фразой, чем «доказательство теорем», для отрасли искусственного интеллекта, которая занимается тем, как заставить машины эффективно выполнять выводы» .
В 1972 году отделение метаматематики Эдинбургского университета было переименовано в «кафедру вычислительной логики» Школы искусственного интеллекта. [3] Затем этот термин использовали Роберт С. Бойер и Дж. Стротер Мур , работавшие в Департаменте в начале 1970-х годов, для описания своей работы по проверке программ и автоматизированному рассуждению . Они также основали Computational Logic Inc.
См. также [ править ]
- Логическое программирование
- Автоматизированное доказательство теорем
- Теория типов
- Формальная проверка
Ссылки [ править ]
- ^ http://tocl.acm.org официальный сайт транзакций ACM по вычислительной логике
- ^ Робинсон, Дж. А. (1970). «Вычислительная логика: унификационные вычисления» . В Мельцере, Бернард; Мичи, Дональд (ред.). Материалы шестого ежегодного семинара по машинному интеллекту . Машинный интеллект. Том. 6. Издательство Эдинбургского университета (опубликовано в 1971 г.). стр. 63–72. ISBN 085224195X .
- ^ http://homepages.inf.ed.ac.uk/bundy/ профессора Алана Банди . Веб-сайт
Дальнейшее чтение [ править ]
- Дов М. Габбай ; Йорг Х. Зикманн; Джон Вудс, ред. (2014). Справочник по истории логики . Том. 9: Вычислительная логика. Эльзевир. ISBN 978-0-08-093067-1 .