Peter B. Andrews

(2012, Manchester)
Nama dalam bahasa asli	(en) Peter Bruce Andrews
Biografi
Kelahiran	1r November 1937 Kota New York
Kematian	21 April 2025 (87 tahun) Burlington
Data pribadi
Pendidikan	Universitas Princeton - Doktor (–1964)
Kegiatan
Penasihat doktoral	Alonzo Church
Spesialisasi	Logika matematika dan matematika
Pekerjaan	matematikawan, dosen, filsuf, logician (en)
Bekerja di	Universitas Carnegie Mellon
Murid	Donald H. Taranto (mul)
Karya kreatif
Murid doktoral	Frank Pfenning (mul) , Michael Kohlhase (mul) , Matthew Clive Bishop (mul) , Sunil Issar (mul) , Edward Russell Fisher, Jr. (mul) , Dale Allen Miller (en) dan Chad E. Brown (en)
Penghargaan (2003)  Herbrand Award (en)

Peter Bruce Andrews (1 November 1937 – 21 April 2025) adalah seorang matematikawan asal Amerika Serikat yang dikenal luas karena kontribusinya dalam bidang logika formal dan teori pemrograman. Ia merupakan pencipta logika matematika Q0, sebuah sistem logika tipe tinggi yang menjadi dasar penting bagi penelitian dalam teori pembuktian, semantik formal, dan pengembangan perangkat lunak berbasis logika. Selain prestasinya dalam logika matematika, Andrews juga menerima hak paten untuk sebuah perban inovatif yang dirancang khusus untuk penanganan luka kritis, menunjukkan minatnya yang meluas di luar bidang akademik murni.^[1]

Selama kariernya, Andrews menjabat di berbagai institusi akademik terkemuka dan menulis sejumlah publikasi ilmiah yang memengaruhi perkembangan logika matematika kontemporer. Karyanya, terutama dalam pengembangan Q0, sering dikaitkan dengan upaya untuk menggabungkan ketelitian formal matematika dengan aplikasi praktis dalam ilmu komputer dan teknologi medis. Prestasinya mencerminkan kombinasi unik antara penelitian teoretis yang mendalam dan inovasi yang berdampak pada dunia nyata.^[1]

Sistem Pembuktian Teorema

Dalam bidang penelitian logika matematika, kelompok riset yang dipimpin oleh Peter Bruce Andrews merancang TPS (Theorem Proving System), sebuah sistem pembuktian teorema otomatis yang mampu menangani logika orde pertama maupun logika orde tinggi.^[2] Sistem ini dirancang untuk memungkinkan peneliti dan mahasiswa membangun pembuktian formal secara otomatis maupun interaktif. Sebagai bagian dari TPS, terdapat subsistem ETPS (Educational Theorem Proving System) yang digunakan khusus untuk membantu mahasiswa mempelajari logika dengan cara membangun bukti deduksi alami secara interaktif, sehingga mendukung pembelajaran konseptual dan praktik dalam logika formal. Kode sumber TPS kini tersedia secara publik melalui Internet Archive, memungkinkan akses dan studi lanjutan bagi para peneliti dan pendidik di bidang logika matematika.^[3]

Publikasi

Dalam ranah publikasi akademik, Peter B. Andrews dikenal luas melalui karya-karya yang berfokus pada logika matematika dan teori tipe. Daftar lengkap publikasinya tersedia pada halaman web pribadinya.^[4] Beberapa publikasi terpilih antara lain:Andrews, Peter B. (1965). A Transfinite Type Theory with Type Variables. North Holland Publishing Company, Amsterdam. Buku ini membahas teori tipe transfinita dengan variabel tipe, yang menjadi landasan awal dalam pengembangan logika tipe.

Andrews, Peter B. (1971). "Resolution in type theory". Journal of Symbolic Logic 36, 414–432. Artikel ini mengeksplorasi metode resolusi dalam konteks teori tipe, memperluas teknik pembuktian otomatis.

Andrews, Peter B. (1981). "Theorem proving via general matings". J. Assoc. Comput. March. 28, no. 2, 193–214. Karya ini memperkenalkan pendekatan pembuktian teorema melalui “general matings” yang berkontribusi pada sistem pembuktian otomatis.

Andrews, Peter B. (1986). An introduction to mathematical logic and type theory: to truth through proof. Computer Science and Applied Mathematics. ISBN 978-0-1205-8535-9. Academic Press, Inc., Orlando, FL. Buku ini merupakan pengantar komprehensif tentang logika matematika dan teori tipe, menekankan metode pembuktian formal.

Andrews, Peter B. (1989). "On connections and higher-order logic". J. Automat. Reason. 5, no. 3, 257–291. Artikel ini membahas hubungan antara koneksi logis dan logika orde tinggi, memberikan kontribusi penting pada teori pembuktian.

Andrews, Peter B.; Bishop, Matthew; Issar, Sunil; Nesmith, Dan; Pfenning, Frank; Xi, Hongwei (1996). "TPS: a theorem-proving system for classical type theory". J. Automat. Reason. 16, no. 3, 321–353. Karya ini menjelaskan sistem TPS yang dikembangkan oleh timnya, termasuk arsitektur dan penerapannya dalam pembuktian teorema klasik.

Andrews, Peter B. (2002). An introduction to mathematical logic and type theory: to truth through proof, edisi kedua. Applied Logic Series, 27. ISBN 978-1-4020-0763-7. Kluwer Academic Publishers, Dordrecht. Edisi kedua ini memperbarui dan memperluas materi dari edisi pertama, menekankan pembuktian formal dan aplikasi logika tipe dalam matematika kontemporer.

Publikasi-publikasi tersebut mencerminkan kontribusi signifikan Andrews dalam bidang logika matematika, terutama dalam pengembangan teori tipe dan sistem pembuktian otomatis, yang terus menjadi rujukan penting bagi peneliti dan akademisi di seluruh dunia.

Referensi

1. 1 2 , Andrews, Peter B., "Bandage which enables examining or treating a wound without removing the adhesive" 
2. ↑ "TPS and ETPS Homepage". gtps.math.cmu.edu. Diakses tanggal 2025-11-08.
3. ↑ Peter Bruce Andrews (2016), theorem_proving_system_peter_bruce_andrews.tar, diakses tanggal 2025-11-08
4. ↑ http://gtps.math.cmu.edu/andrews.html