Введение
Питер Брюс Эндрюс (Peter Bruce Andrews) – американский математик, родившийся в 1937 году, и профессор математики, заслуженный профессор Университета Карнеги-Меллона в Питтсбурге, штат Пенсильвания, а также создатель математической логики Q0. Он получил степень доктора философии в Принстонском университете в 1964 году под руководством Алонзо Черча. В 2003 году он был удостоен премии Гербранда. Его исследовательская группа разработала автоматический теоремодоказатель TPS. Подсистема ETPS (Educational Theorem Proving System) в составе TPS используется для обучения студентов логике посредством интерактивного построения доказательств методом естественной дедукции.
Peter Bruce Andrews (born 1937) is an American mathematician and Professor of Mathematics, Emeritus at Carnegie Mellon University in Pittsburgh, Pennsylvania, and the creator of the mathematical logic Q0. He received his Ph. D. from Princeton University in 1964 under the tutelage of Alonzo Church. He received the Herbrand Award in 2003. His research group designed the TPS automated theorem prover. A subsystem ETPS (Educational Theorem Proving System) of TPS is used to help students learn logic by interactively constructing natural deduction proofs.
Публикации
Эндрюс, Питер Б. (1965). Теория трансфинитных типов с переменными типов. Издательская компания "Северная Голландия", Амстердам. Эндрюс, Питер Б. (1971). "Резолюция в теории типов". Журнал символической логики, 36, 414–432. Эндрюс, Питер Б. (1981). "Доказательство теорем посредством общих соответствий". J. Assoc. Comput. March, 28, № 2, 193–214. Эндрюс, Питер Б. (1986). Введение в математическую логику и теорию типов: к истине через доказательство. Computer Science and Applied Mathematics. Academic Press, Inc., Орландо, Флорида. Эндрюс, Питер Б. (1989). "О связях и логике высшего порядка". J. Automat. Reason., 5, № 3, 257–291. Эндрюс, Питер Б.; Бишоп, Мэтью; Иссар, Сунил; Несмит, Дэн; Пфеннинг, Франк; Си, Хунвэй (1996). "TPS: система доказательства теорем для классической теории типов". J. Automat. Reason., 16, № 3, 321–353. Эндрюс, Питер Б. (2002). Введение в математическую логику и теорию типов: к истине через доказательство. Второе издание. Applied Logic Series, 27. Kluwer Academic Publishers, Дордрехт.