Pointer untuk aplikasi logika CS

Saya seorang mahasiswa pascasarjana dalam matematika dengan latar belakang yang kuat dalam logika. Saya telah mengambil kursus pascasarjana selama setahun di bidang logika bersama-sama dengan program pascasarjana tentang teori model terbatas dan satu lagi tentang teori memaksa dan menetapkan. Sebagian besar teks CS tampaknya hanya mengasumsikan latar belakang yang sangat sederhana dalam logika, yang sebagian besar mencakup dasar-dasar logika proposisional dan logika tingkat pertama.

Saya ingin mendapatkan beberapa petunjuk tentang ke mana harus pergi untuk aplikasi CS di mana bahan yang lebih berat dari logika digunakan. Salah satu minat saya adalah teori tipe dan metode formal secara umum. Adakah yang bisa menyarankan beberapa bacaan bagus melewati buku-buku pengantar tentang pengecekan model dan bahasa pemrograman?

Saya meninjau secara singkat beberapa area di sini, mencoba untuk fokus pada ide-ide yang akan menarik bagi seseorang dengan latar belakang logika matematika tingkat lanjut.

Teori Model Hingga

Pembatasan paling sederhana dari teori model klasik dari sudut pandang ilmu komputer adalah mempelajari struktur di atas alam semesta yang terbatas. Struktur ini terjadi dalam bentuk basis data relasional, grafik, dan objek kombinatorial lainnya yang muncul di mana-mana dalam ilmu komputer. Pengamatan pertama adalah bahwa beberapa teorema dasar teori model orde pertama gagal ketika dibatasi untuk model terbatas. Ini termasuk teorema kekompakan, teorema kelengkapan Godel, dan konstruksi ultraproduk. Trakhtenbrot menunjukkan bahwa tidak seperti logika orde pertama klasik, kepuasan atas model terbatas tidak dapat diputuskan.

Alat mendasar di area ini adalah lokalitas Hanf, lokalitas Gaifman, dan berbagai variasi pada game Ehrenfeucht-Fraisse. Topik yang dipelajari meliputi logika infinitary, logika penghitungan, logika titik tetap, dll. Selalu dengan fokus pada model yang terbatas. Ada pekerjaan yang berfokus pada ekspresivitas dalam fragmen variabel terbatas dari logika tingkat pertama dan logika ini memiliki karakterisasi melalui permainan kerikil. Arahan lain dari penyelidikan adalah untuk mengidentifikasi sifat-sifat logika klasik yang selamat dari pembatasan model terbatas. Hasil baru-baru ini ke arah itu dari Rossman menunjukkan bahwa teorema pelestarian homomorfisme tertentu masih memegang model yang terbatas.

1. Teori Model Hingga , Ebbinghaus dan Kegagalan
2. Elemen Teori Model Hingga , Libkin
3. Tentang strategi kemenangan dalam permainan Ehrenfeucht-Fraisse , Arora dan Fagin, 1997.
4. Teorema pelestarian homomorfisme , Rossman

Proposisional -kalkulus$\mu$

Garis kerja dari akhir 60-an menunjukkan bahwa banyak sifat program dapat diekspresikan dalam ekstensi dari logika proposisional yang mendukung alasan tentang titik tetap. Modalus kalkulus adalah salah satu logika yang dikembangkan pada periode ini yang telah menemukan berbagai aplikasi dalam metode formal otomatis. Banyak metode formal terhubung ke logika temporal, atau logika gaya-Hoare dan banyak dari ini dapat dilihat dari segi μ -kalkulus. Bahkan, saya telah mendengarnya mengatakan bahwa μ- calculus adalah bahasa assembly dari logika temporal.$\mu$$\mu$$\mu$

Dalam makalahnya yang memperkenalkan -calculus, Kozen memberikan aksioma dan hanya membuktikannya terdengar dan lengkap untuk fragmen logika yang terbatas. Bukti kelengkapan adalah salah satu masalah terbuka besar dalam ilmu komputer logis sampai Walukiewicz memberikan bukti (berdasarkan automata tak terbatas). Teori model μ- kalkulus memiliki banyak hasil yang kaya. Mirip dengan teorema van Benthem untuk logika modal, Janin dan Walukiewicz membuktikan bahwa μ- kalkulus secara ekuivalen dengan fragmen invarian bisimulasi dari logika urutan kedua monadik. The $\mu$$\mu$$\mu$$\mu$-kalkulus juga telah ditandai dalam hal permainan paritas dan automata atas pohon tak terbatas. Masalah kepuasan untuk logika ini adalah EXPTIME lengkap dan Emerson dan Jutla menunjukkan bahwa logika memiliki properti model kecil. Bradfield menunjukkan bahwa hierarki pergantian -kalkulus adalah ketat, sementara Berwanger menunjukkan bahwa hierarki variabel juga ketat. Alat klasik penting yang digunakan dalam bidang ini adalah teorema Rabin dan teorema determinasi Martin.$\mu$

1. Hasil pada μ proposisional$\mu$ kalkulus , Kozen, 1983
2. Dasar-dasar $\mu$ -calculus Arnold dan Niwinski, 2001
3. Kelengkapan Aksiomatis Kozen tentang Proposisi $\mu$ -Calculus , Walukiewicz 1995
4. Logika modal dan $\mu$ -calculi , Bradfield and Stirling, 2001
5. Hirarki alternatif modal mu-kalkulus sangat ketat , Bradfield, 1996
6. Hirarki variabel dari kalkulus mu sangat ketat , Berwanger, E. Grädel, dan G. Lenzi, 2005

Logika Temporal Linier

Logika temporal linier diadopsi dari logika filosofis ke dalam ilmu komputer untuk alasan tentang perilaku program komputer. Itu dianggap logika yang baik karena bisa mengekspresikan properti seperti invarian (tidak adanya kesalahan) dan pemutusan. Teori pembuktian logika temporal dikembangkan oleh Manna dan Pnueli (dan lainnya, kemudian) dalam artikel dan buku mereka. Pengecekan model dan masalah kepuasan untuk LTL keduanya dapat diselesaikan dalam hal automata dibandingkan kata-kata yang tak terbatas.

Pnueli juga membuktikan resuls mendasar tentang LTL dalam makalah aslinya yang memperkenalkan logika untuk alasan tentang program. Vardi dan Wolper memberikan kompilasi formula LTL yang jauh lebih sederhana ke dalam Buchi automata. Koneksi ke logika temporal telah menyebabkan studi yang intens dari algoritma untuk secara efisien memperoleh automata dari LTL, dan untuk penentuan dan pelengkap Buchi automata. Teorema Kamp menunjukkan bahwa LTL dengan modalitas karena secara dan sampai eksplisit setara dengan logika orde pertama monadik dengan relasi urutan. Ada pekerjaan yang sedang berlangsung memperluas hasil ini ke logika atas pesanan linier yang padat dan interval waktu. Etessami dan Wilke mengembangkan variasi game Ehrenfeucht-Fraisse untuk LTL dan menggunakannya untuk menunjukkan bahwa hierarki sampai ketat. Lini pekerjaan lain adalah memperluas LTL untuk menyatakan sewenang-wenang$\omega$$\mu$$\mu$

1. Logika temporal program , Pnueli 1977
2. Dari Gereja dan Sebelum ke PSL , Vardi, 2008
3. Pendekatan automata-theoretic untuk logika temporal linier , Vardi dan Wolper, 1986
4. Logika Temporal Sistem Reaktif dan Bersamaan: Spesifikasi , Manna dan Pnueli
5. Sebuah hierarki Hingga dan aplikasi lain dari game Ehrenfeucht-Fraïssé untuk logika temporal , Etessami dan Wilke, 2000

Logika Komputasi-Pohon

$\mu$

Masalah pengecekan model untuk CTL pada struktur hingga adalah dalam waktu polinomial. Masalah pengecekan model untuk CTL * selesai EXPTIME. Aksiomaasi CTL * adalah masalah terbuka yang menantang yang akhirnya diselesaikan oleh Reynolds 2001. Analog dari teorema van Benthem untuk logika modal dan teorema Kamp untuk LTL diberikan untuk CTL * oleh teorema Hafer dan Thomas yang menunjukkan bahwa CTL * sesuai dengan sebuah fragmen logika urutan kedua monadik di atas pohon biner. Karakterisasi selanjutnya oleh Hirschfeld dan Rabinovich adalah bahwa CTL * secara ekuivalen dengan fragmen MSO dengan bisimulasi-invarian dengan kuantifikasi jalur.

1. "Kadang-kadang" dan "tidak pernah" ditinjau kembali: pada percabangan versus logika temporal waktu linier , Emerson dan Halpern, 1986
2. Tentang Kekuatan Ekspresif CTL , Moller, Rabinovich, 1999
3. Logika komputasi pohon CTL * dan quantifier jalur dalam teori monadik dari pohon biner , Hafer dan Thomas, 1987
4. Axiomatization dari Logika Pohon Komputasi Lengkap , Reynolds, 2001

Bahasa Kata Tak Terbatas

$\omega$ -languages, yang adalah bahasa di mana kata-kata didefinisikan sebagai fungsi dari nomor alami untuk alfabet yang terbatas. Komunitas telah mempelajari sifat-sifat bahasa reguler di atas kata-kata tak terbatas dan mengembangkan beberapa hasil analog dengan kasus kata hingga. Ada beberapa kejutan yang muncul, jadi kita tidak bisa begitu saja mengangkat hasil kata hingga ke kasus kata tak terbatas.

$\omega$$\omega$$\omega$kata-kata. Selain itu, dengan menggunakan topologi dasar, mereka menunjukkan bahwa setiap properti waktu-linier dapat dinyatakan sebagai persimpangan properti keselamatan dan properti. Hasil ini memiliki konsekuensi praktis yang signifikan karena ini berarti bahwa alih-alih membangun pemeriksa properti yang kompleks, ia cukup untuk membangun pemeriksa keamanan dan keselamatan. Pengurangan lebih lanjut menunjukkan bahwa itu cukup untuk membangun pemeriksa invarian dan pemeriksa penghentian. Karakterisasi safety-liveness diperluas ke pohon oleh Manolios dan Trefler dan baru-baru ini untuk serangkaian jejak, dalam kerangka hyperproperties, oleh Clarkson dan Schneider.

1. Kata Tak Terbatas: Automata, Semigroup, Logika dan Game , Perrin dan Pin, 2004
2. $\omega$
3. $\omega$
4. Pada kongruensi sintaksis untuk ω — bahasa , Maler dan Staiger, 1993

Automata pada Kata Tak Terbatas

Di mana ada bahasa, ilmuwan komputer akan memiliki automata. Masukkan teori automata melalui kata-kata tak terbatas dan pohon tak terbatas. Sangat menyedihkan bahwa walaupun automata atas kata-kata tak terbatas muncul dalam dua tahun automata pada kata-kata yang terbatas, topik mendasar ini jarang dicakup dalam kurikulum ilmu komputer standar. Automata atas kata-kata dan pohon yang tak terbatas memberikan pendekatan yang sangat kuat untuk membuktikan kepastian kepuasan bagi keluarga logika yang sangat kaya.

$\omega$

1. Decidability dari Teori Orde Kedua dan Automata on Infinite Trees , Rabin, 1969
2. Automata pada objek tak terbatas , Thomas, 1988
3. Automata: Dari Logika ke Algoritma , Vardi, 2007

Game Tanpa Batas

Permainan logis dan tak terbatas adalah bidang penelitian aktif. Teori-teori permainan muncul dalam ilmu komputer di semua tempat dalam dualitas antara non-determinisme dan paralelisme (pergantian), program dan lingkungannya, kuantifikasi universal dan eksistensial, modalitas kotak dan berlian, dll. Permainan ternyata menjadi cara yang bagus untuk mempelajari properti dari berbagai jenis logika non-klasik yang tercantum di atas.

Seperti halnya kriteria penerimaan untuk automata, kami memiliki kondisi kemenangan yang berbeda untuk permainan dan banyak yang dapat ditunjukkan setara. Karena Anda bertanya tentang hasil klasik, teorema Borel Determinacy dan Gale-Stewart sering terletak secara diam-diam di latar belakang beberapa model permainan yang kami pelajari. Salah satu pertanyaan mendesak dari zaman kita adalah tentang kompleksitas menyelesaikan permainan paritas. Jurdzinski memberikan algoritma peningkatan strategi dan menunjukkan bahwa menentukan pemenang ada di persimpangan kelas kompleksitas UP dan coUP. Kompleksitas yang tepat dari algoritma Jurdzinski terbuka sampai Friedmann memberikannya batas bawah eksponensial pada tahun 2009.

1. Memutuskan pemenang dalam permainan paritas adalah di UP ∩ co-UP , Jurdzinski, 1998
2. Game untuk μ-calculus , Niwinski dan Walukiewicz, 1996
3. Batas Bawah Eksponensial untuk Algoritma Peningkatan Strategi Permainan Paritas seperti yang Kita Ketahui , Friedmann, 2009

Edmund M. Clarke, Orna Grumberg, Doron A. Peled: Memeriksa Model . MIT Press 1999, adalah buku yang bagus (untuk saya) tentang pengecekan model.

Glynn Winskel: Semantik Resmi Bahasa Pemrograman: pengantar . MIT Press 1994, adalah salah satu buku teks standar tentang bahasa pemrograman.

Mordechai Ben-Ari: Logika matematika untuk ilmu komputer . Springer 2001, mungkin itu yang Anda cari.

Teori basis data adalah bidang yang luas yang menyediakan banyak aplikasi logika. Kompleksitas deskriptif dan teori model hingga adalah bidang yang terkait erat. Sejauh yang saya tahu, semua bidang ini cenderung menggunakan gaya logika aljabar (mengikuti jejak Birkhoff dan Tarski) daripada teori bukti. Namun, beberapa karya Peter Buneman , Leonid Libkin , Wenfei Fan , Susan Davidson , Limsoon Wong , Atsushi Ohori , dan peneliti lain yang bekerja di UPenn pada 1980-an, 90-an, memang berupaya menyatukan teori dan database bahasa pemrograman. Ini tampaknya membutuhkan kenyamanan dengan kedua gaya logika. Hal yang sama berlaku untuk pekerjaan yang lebih baru oleh James Cheney dan Philip Wadler .

Dalam hal referensi spesifik, buku teks standar tersedia online untuk referensi yang mudah:

• Serge Abiteboul, Richard Hull, Victor Vianu. Yayasan Databases , 1995. http://webdam.inria.fr/Alice/

Sayangnya saya tidak tahu buku teks atau survei umum terkini yang mencakup bidang yang bergerak cepat ini. Saya telah menemukan dua survei yang lebih tua berguna. Pertama,

• Jan Van den Bussche, Aplikasi Ide Alfred Tarski dalam Database Theory , CSL 2001. doi: 10.1007 / 3-540-44802-0_2

menunjukkan cara menghubungkan titik-titik antara Tarski dan subbidang tertentu, basis data pembatas. Kedua,

• Victor Vianu, Basis Data dan Teori Model Hingga , Kompleksitas Deskriptif, dan Model Hingga: Prosiding Workshop DIMACS, 1996. http://leo.saclay.inria.fr/publifiles/gemo/GemoReport-107.ps.gz

pitches (1996-style) teori database untuk teori model hingga, dan dalam proses menyoroti banyak aplikasi logika yang menarik dalam database. Untuk pekerjaan yang lebih baru (seperti teori XML, sumber, model streaming, atau basis data grafik) membaca makalah penelitian yang sangat dikutip adalah pendekatan yang masuk akal.

Michael Huth dan Mark Ryan: Logika dalam ilmu komputer , Cambridge University Press, 2004.

Saya sangat merekomendasikan buku ini sebagai pengantar umum tentang bagaimana logika berperan dalam ilmu komputer.

Penggunaan utama logika dalam CS adalah logika program, juga disebut logika Hoare.

$2 \in \sqrt(\pi^{17})$

Situasi serupa diperoleh dalam studi logika modal yang (menyederhanakan sedikit lagi) tidak seekspresi logika urutan pertama, tetapi apa yang bisa mereka ungkapkan, mereka ekspresikan dengan formula dan bukti yang lebih pendek.

Mengidentifikasi fragmen yang sesuai dari ZFC tidak sulit untuk bahasa pemrograman sederhana, tetapi menjadi lebih cepat menantang karena bahasa pemrograman memperoleh lebih banyak fitur. Beberapa tahun terakhir telah melihat kemajuan besar dalam upaya ini.

Makalah Dasar Aksiomatik untuk Pemrograman Komputer oleh T. Hoare sering dianggap sebagai studi yang mempelajari logika program dengan sungguh-sungguh, mudah dibaca, dan mungkin cara yang baik untuk mulai menjelajah ke lapangan. Logika yang sama dipelajari secara lebih rinci dalam buku Winskel "Formal Semantics of Programming Languages" yang disebutkan oleh @vb le.

Teori tipe dapat dilihat dalam cahaya yang serupa. Titik penjualan utama dari tipe-teori adalah identifikasi bukti dengan program (murni fungsional), yang mengarah ke konsep ekonomi yang hebat dan otomatisasi yang kuat (dalam bentuk inferensi tipe dan pembuktian teorema interaktif). Harga untuk teori jenis menjadi cara yang elegan untuk mengorganisir bukti adalah bahwa itu tampaknya tidak bekerja dengan baik dengan bahasa pemrograman yang tidak murni fungsional.

Teks modern dan menyeluruh yang memperkenalkan logika program dengan cara berteori tipe-teoretis adalah Software Foundations oleh Pierce et al. Ini akan membawa Anda tepat di dekat (a) penelitian terdepan dalam verifikasi program dan, sebagai buku teks, mungkin memberikan sekilas tentang bagaimana ilmu komputer dan matematika akan diajarkan di masa depan.

Setelah logika program dikembangkan untuk suatu bahasa, langkah selanjutnya adalah otomatisasi, atau otomatisasi parsial: membuat bukti untuk program non-sepele adalah padat karya, dan kami ingin mesin melakukan sebanyak mungkin dari itu. Banyak penelitian saat ini dalam metode formal yang harus dilakukan dengan otomatisasi tersebut.

Ada tradisi logika yang sangat kuat dalam ilmu komputer. Masalah yang kita pelajari dan estetika komunitas logika komputasi tidak identik dengan komunitas logika matematika. Anda benar bahwa perkembangan signifikan dalam teori model, meta-teori logika orde pertama dan teori himpunan tidak umum digunakan dalam logika komputasi. Seseorang dapat dengan sukses meneliti log komputasi tanpa melihat atau menggunakan ultrafilters, analisis non-standar, pemaksaan, teorema Paris-Harrington, dan sejumlah konsep menarik lainnya yang dianggap penting dalam logika klasik.

Sama seperti seseorang menerapkan ide-ide matematika untuk mempelajari logika serta ide-ide logis untuk mempelajari matematika, kami menerapkan logika untuk mempelajari ilmu komputer dan juga menerapkan perspektif komputasi untuk mempelajari logika. Fokus yang berbeda ini memiliki konsekuensi yang agak dramatis untuk jenis hasil yang penting bagi kami.

Berikut ini kutipan dari John Baez tentang logika dan ilmu komputer. Saya tidak memiliki pandangan yang persis sama karena saya tidak terlalu terbiasa dengan logika matematika tingkat lanjut.

Ketika saya masih sarjana, saya cukup tertarik pada logika dan dasar-dasar matematika --- saya selalu mencari konsep yang paling mengejutkan yang bisa saya dapatkan, dan teorema Goedel, teorema Loewenheim-Skolem, dan seterusnya di atas sana dengan mekanika kuantum dan relativitas umum sejauh yang saya ketahui. [...] Saya ingat merasakan pada saat itu bahwa logika telah menjadi kurang revolusioner daripada di dalamnya pada bagian awal abad ini. Tampak bagi saya bahwa logika telah menjadi cabang matematika seperti yang lainnya, mempelajari sifat-sifat tidak jelas dari model aksioma Zermelo-Fraenkel, daripada mempertanyakan asumsi dasar yang tersirat dalam aksioma-aksioma tersebut dan berani mengejar pendekatan baru yang berbeda. [...]

Bagaimanapun, sekarang sudah cukup jelas bagi saya bahwa saya belum membaca hal yang benar. Saya pikir Rota telah mengatakan bahwa karya yang sangat menarik dalam logika sekarang berada di bawah nama "ilmu komputer ', [...] - Minggu 40, Temuan Minggu Ini, John Baez

Logika dalam ilmu komputer adalah bidang yang luas dan berkembang pesat. Saya menemukan bahwa setiap perspektif logika klasik dapat dimodifikasi untuk mendapatkan beberapa perspektif pada logika komputasi. Entri Wikipedia tentang logika matematika membagi bidang menjadi teori himpunan, teori model, teori bukti dan teori rekursi. Anda dapat secara esensial mengambil area-area ini dan menambahkan rasa komputasi ke dalamnya dan memperoleh sub-bidang logika komputasi.

Model Theory Kami suka mempelajari teori model logika non-klasik dan model non-klasik dari logika klasik. Maksud saya, kita mempelajari modal, temporal dan logika sub-struktural, dan bahwa kita mempelajari logika di atas pohon, kata-kata, dan model terbatas, sebagai lawan dari model klasik seperti aljabar. Dua masalah mendasar adalah kepuasan dan pengecekan model. Keduanya memiliki signifikansi praktis dan teoritis yang sangat besar. Sebaliknya, masalah-masalah ini kurang penting dalam logika klasik.

Teori bukti Kami mempelajari kompleksitas dan efisiensi yang dengannya kami dapat menghasilkan bukti dalam sistem bukti klasik, serta mengembangkan sistem bukti non-klasik baru yang sensitif terhadap pertimbangan kompleksitas dan efisiensi. Pengurangan otomatis mempelajari generasi bukti yang didukung mesin, berbicara luas. Prosesnya mungkin melibatkan interaksi manusia atau sepenuhnya otomatis. Ada banyak pekerjaan dalam mengembangkan prosedur keputusan untuk teori-teori logis. Kompleksitas bukti berfokus pada ukuran bukti dan kompleksitas komputasi untuk menghasilkan bukti. Ada garis pekerjaan yang menarik terkait program untuk bukti, yang menggabungkan dengan pekerjaan turun dari logika linier untuk mengembangkan sistem bukti, dan akibatnya bahasa pemrograman, yang peka terhadap sumber daya.

Teori rekursi Teori rekursi kami adalah teori kompleksitas. Daripada mempelajari apa yang dapat dihitung, kita mempelajari seberapa efisien kita dapat menghitung. Ada banyak analogi teori rekursi dalam teori kompleksitas, tetapi hasil dan pemisahan teori rekursi tidak selalu berlaku untuk analogi teoretis kompleksitas mereka. Alih-alih set yang dapat dihitung dan hierarki aritmatika, kami memiliki waktu polinomial, hierarki waktu polinomial, dan ruang polinomial yang melampirkan hierarki. Alih-alih kuantifikasi terbatas dalam hierarki aritmatika, kami memiliki kepuasan dan rumus Boolean yang terukur serta kuantifikasi terbatas dari rumus Boolean.

Artikel survei

Tentang Efektivitas Logika yang Tidak Biasa dalam Ilmu Komputer

adalah titik awal yang baik untuk mendapatkan pandangan logika komputasi yang sangat tinggi. Saya akan membuat daftar beberapa bidang ilmu komputer yang berorientasi logis. Saya berharap orang lain akan mengedit jawaban ini dan menambah daftar itu di sini, dan mungkin menambahkan tautan ke jawaban di halaman ini.

1. Teori model terbatas
2. Kompleksitas bukti
3. Deduksi Algoritma (prosedur keputusan untuk teori logis)
4. Logika program
5. Logika dinamis
6. Linear Temporal logic dan variannya
7. Logika Pohon Komputasi dan variannya
8. Logika epistemik
9. Teori basis data
10. Jenis teori
11. Automata atas kata-kata yang tak terbatas
12. Logika kategorikal
13. Teori concurrency dan proses aljabar
14. Teori domain
15. Logika linier
16. Kompleksitas Deskriptif
17. Memeriksa Model
18. Kalkulator Poin Tetap dan logika penutupan transitif

area tumpang tindih yang kuat antara logika dan ilmu komputer membuktikan teorema otomatis , misalnya [4]. juga misalnya ref [1] adalah penggunaan teorema Boyer-Moore untuk memeriksa / memverifikasi teorema Godels. Hasil utama / mengesankan lainnya adalah penyelesaian perangkat lunak baru-baru ini dari teorema empat warna (dan yang lainnya seperti Odd Order dan Feit-Thompson [3]) pada penelitian Microsoft oleh Gonthier. [2]

[1] Metamathematika, Mesin, dan Bukti Gödel (Traktat Cambridge dalam Ilmu Komputer Teoretis oleh Shankar

[2] Bukti yang diperiksa di komputer dari Four Color Theorem Georges Gonthier

[3] Algoritma yang menarik dalam formalisasi teorema Feit-Thompson? tcs.se

[4] Di mana dan bagaimana komputer membantu membuktikan teorema? tcs.se