Дональд В. Лавленд

Дональд В. Лавленд
Рожденный	( 1934-12-26 ) 26 декабря 1934 г. Рочестер, Нью-Йорк
Альма-матер	Нью-Йоркский университет
Известный	Алгоритм ДПЛЛ
Награды	Премия Эрбрана 2001 г.
Научная карьера
Поля	Информатика
Учреждения	Университет Дьюка
Диссертация	Рекурсивно случайные последовательности   (1964)
Докторские консультанты	Питер Унгар, Мартин Дэвид Дэвис
Докторанты	Оуэн Астрахан , Сьюзэн Герхарт

Дональд В. Лавленд (родился 26 декабря 1934 года в Рочестере, Нью-Йорк ) профессор — почетный информатики , Университета Дьюка специализирующийся на искусственном интеллекте . Он хорошо известен благодаря алгоритму Дэвиса-Патнэма-Логемана-Лавленда .

Лавленд окончил Оберлин-колледж в 1956 году, получил степень магистра Массачусетского технологического института в 1958 году и докторскую степень. из Нью-Йоркского университета в 1964 году. Он поступил на факультет компьютерных наук Университета Дьюка в 1973 году. Ранее он работал преподавателем на факультете математики в Нью-Йоркском университете и Университете Карнеги-Меллона .

В 2001 году он получил премию Эрбрана за выдающийся вклад в автоматизированное мышление. Он является членом Ассоциации вычислительной техники (2000 г.). член Ассоциации искусственного интеллекта (1993 г.), и член Американской ассоциации содействия развитию науки (2019 г.).

Библиография

Книги

• Автоматизированное доказательство теорем: логическая основа . Издательство Северной Голландии. 1978. doi : 10.1016/c2009-0-12705-8 . hdl : 2445/109943 . ISBN  978-0-7204-2500-0 .
• 6-я конференция по автоматизированному дедукции . Конспекты лекций по информатике. Том. 138. (Редактор) Спрингер-Верлаг, Лондон. 1982. doi : 10.1007/BFb0000048 . ISBN  978-3-540-11558-8 . S2CID   33583364 .
• Автоматизированное доказательство теорем: спустя 25 лет . Современная математика. Том. 29. (совместно с В.В. Бледсо) American Mathematical Soc. 1984. doi : 10.1090/conm/029 . ISBN  978-0-8218-5027-5 .
• Три взгляда на логику: математика, философия и информатика . (совместно с Р. Ходелом и С.Г. Стерреттом) Издательство Принстонского университета. 26 января 2014 г. ISBN  978-1-4008-4875-1 .

Избранные статьи

• Дэвис, Мартин; Логеманн, Джордж; Лавленд, Дональд (1 июля 1962 г.). «Машинная программа для доказательства теорем». Коммуникации АКМ . 5 (7): 394–397. дои : 10.1145/368273.368557 . hdl : 2027/mdp.39015095248095 . S2CID   15866917 .
• Лавленд, Дональд (1966). «Новая интерпретация концепции случайной последовательности фон Мизеса». Журнал математической логики и основ математики . 12 (1): 279–294. дои : 10.1002/malq.19660120124 .
• Лавленд, Дональд В. (1 апреля 1968 г.). «Доказательство механических теорем методом исключения моделей» . Журнал АКМ . 15 (2): 236–251. дои : 10.1145/321450.321456 . S2CID   18377884 .
• Лавленд, Д.В. (1969). «Упрощенный формат процедуры доказательства теоремы об исключении модели». Автоматизация рассуждений . стр. 233–248. CiteSeerX   10.1.1.1017.8248 . дои : 10.1007/978-3-642-81955-1_14 . ISBN  978-3-642-81957-5 .
• Лавленд, DW (декабрь 1969 г.). «Вариант колмогоровской концепции сложности» . Информация и контроль . 15 (6): 510–526. дои : 10.1016/S0019-9958(69)90538-5 .
• Лавленд, Д.В. (1970). «Линейный формат разрешения». Симпозиум по автоматической демонстрации . Конспект лекций по математике. Том. 125. стр. 147–162. дои : 10.1007/BFb0060630 . ISBN  978-3-540-04914-2 . ISSN   0075-8434 . S2CID   121021241 .
• Лавленд, DW (1 апреля 1972 г.). «Объединяющий взгляд на некоторые линейные процедуры Эрбрана» . Журнал АКМ . 19 (2): 366–384. дои : 10.1145/321694.321706 . S2CID   14244283 .
• Флейзиг, С.; Лавленд, Д.; Смайли, АК; Ярмуш, Д.Л. (1 января 1974 г.). «Реализация процедуры доказательства исключения модели» . Журнал АКМ . 21 (1): 124–139. дои : 10.1145/321796.321807 . S2CID   15686713 .

См. также

• Удаление модели

Внешние ссылки

• Список публикаций на DBLP