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

Donald W. Loveland (родился 26 декабря 1934 года в Рочестере, штат Нью - Йорк ) ^[1] является профессором в отставке из информатики в Университете Дьюка , который специализируется на искусственном интеллекте . ^[2] Он хорошо известен алгоритмом Дэвиса – Патнэма – Логеманна – Ловленда . ^[3]

Лавленд окончил Оберлин-колледж в 1956 году, получил степень магистра в Массачусетском технологическом институте в 1958 году и степень доктора философии. окончил Нью-Йоркский университет в 1964 году. В 1973 году он поступил на факультет компьютерных наук Университета Дьюка. Ранее он работал преподавателем на факультете математики Нью-Йоркского университета и Университета Карнеги-Меллона . ^{[1] [4] [5]}

Он получил премию Herbrand за выдающийся вклад в автоматизированное рассуждение в 2001 году. ^[5] Он является членом Ассоциации вычислительной техники (2000), ^[6] членом Ассоциации искусственного интеллекта (1993), ^[7] и член американской ассоциации содействия развитию науки (2019). ^[8]

Библиография [ править ]

Книги

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

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

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

См. Также [ править ]

• Исключение модели

Ссылки [ править ]

Внешние ссылки [ править ]

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