Alasan untuk belajar logika proposisional & predikat

Saya dapat memahami pentingnya bahwa ilmuwan komputer atau insinyur terkait pengembangan perangkat lunak harus memahami studi tentang logika dasar sebagai dasar.

Tetapi apakah ada tugas / pekerjaan yang secara eksplisit membutuhkan pengetahuan tentang hal ini, selain tugas yang membutuhkan representasi pengetahuan Knowledge Base? Saya ingin mendengar jenis tugas, bukan tanggapan konseptual.

Alasan saya bertanya ini hanya karena keingintahuan saya. Sementara siswa CS harus menghabiskan sejumlah waktu pada subjek ini, beberapa kursus intensif-praktis (misalnya AI-Class ) melewatkan topik ini sepenuhnya. Dan saya hanya ingin tahu bahwa misalnya mengetahui predicate logicmungkin membantu menggambar ER diagramtetapi mungkin bukan keharusan.

Perbarui 5/27/2012) Terima kasih atas jawaban. Sekarang saya pikir saya benar-benar mengerti & setuju dengan pentingnya logicdi CS dengan sejumlah besar aplikasi. Saya baru saja mengambil jawaban terbaik dari kesan yang saya dapatkan dari solusi untuk Windowsmasalah layar biru.

Saya cenderung menyukai Unifikasi dan apa pun yang terkait dengannya. Jika Anda tidak tahu logika proposisional & predikat, maka Anda melewatkan dasar-dasar logika. Jika Anda memiliki minat pada apa pun yang terdaftar , maka itu akan seperti memiliki minat dalam matematika dan melewatkan penambahan dan perkalian. Logika bukan hanya untuk AI.

Sebagai jawaban praktis, ingat masalah Intel floating point dan bagaimana Anda tidak pernah melihatnya lagi? Berkat penggunaan teorema pembalik mereka adalah sesuatu dari masa lalu. Ingat layar biru kematian Microsoft . Berkat solver SAT, pengecekan model dan solusi berbasis logika lainnya, mereka adalah spesies yang terancam punah.

Ada koneksi yang sangat mendalam dan meresap antara logika dan ilmu komputer. Dalam memahami apa mereka mungkin, perlu diingat bahwa ilmu komputer juga disebut "teknologi informasi" atau "informatika", yang berarti bahwa sistem komputer menangkap, memproses dan mengirimkan informasi. Logika adalah hal yang serupa. Ini mempelajari bagaimana informasi ditangkap dalam kalimat dan bagaimana dimungkinkan untuk satu pernyataan menjadi konsekuensi dari yang lain, yaitu, bagaimana konten informasinya sudah ada dalam pernyataan lain (atau kumpulan pernyataan). Dalam pengertian itu, logika dan ilmu komputer pada dasarnya samadisiplin, fokus pada berbagai aspek. Ahli logika (Gereja, Kleene, Turing, Post dan siswa serta kolega mereka) menciptakan disiplin Ilmu Komputer, dan banyak ahli logika terus memberikan kontribusi pada Ilmu Komputer, terutama Jean-Yves Girard dan murid-muridnya.

Berikut adalah beberapa aplikasi logika standar dalam Ilmu Komputer:

• Desain sirkuit digital sepenuhnya didasarkan pada logika proposal, sedemikian rupa sehingga para insinyurnya menyebutnya "desain logika" daripada "desain sirkuit". Bahkan menulis program komputer sering dianggap melibatkan merancang "logikanya". (Perhatikan bahwa "logika" dalam pengertian yang terakhir adalah ide informal daripada logika formal, digunakan untuk merujuk pada aliran informasi melalui program dan apakah itu sedang diproses dengan benar.)

• Predikat logika dan sepupunya matematis, teori himpunan, digunakan dalam berbagai bahasa komputasi , misalnya, bahasa SQL untuk kueri basis data relasional. Ada juga bahasa pemrograman berdasarkan logika, yang disebut "bahasa pemrograman logika".

• Representasi pengetahuan , yang telah Anda sebutkan, memiliki banyak formalisme berdasarkan logika. Bahkan jika menggunakan formalisme non-logis, banyak dari mereka masih memiliki makna logis , dan karenanya didasarkan pada logika.

• Logika probabilistik, di mana pernyataan tidak hanya memiliki nilai benar / salah, tetapi tingkat kepastian / ketidakpastian, semakin fondasi untuk sistem pembelajaran mesin .

• Jika Anda ingin secara resmi menyatakan apa yang dilakukan suatu program, yaitu, memberikan spesifikasi program , Anda pada akhirnya akan menggunakan beberapa bentuk bahasa logis. Memang, ada banyak bahasa spesifikasi program, seperti Z dan B, yang didasarkan pada logika predikat dan teori himpunan. Ada juga bahasa spesifikasi berdasarkan logika persamaan, seperti Larch. Ilmuwan Komputer sering menciptakan logika baru untuk mewakili kebutuhan ilmu komputer, misalnya, Logika Hoare dan Logika Pemisahan, atau mereka mengambil dan mengembangkan berbagai bentuk logika tradisional yang kurang digunakan, seperti logika temporal dan logika modal, dan mengembangkannya lebih lanjut.

• Jika Anda ingin memverifikasi apakah suatu program melakukan apa yang seharusnya dilakukan, maka Anda akhirnya tidak hanya menggunakan bahasa logika, tetapi juga seluruh mesin logika: teori bukti, teori model, dan prosedur keputusan. Teknologi verifikasi sekarang berkembang pesat, dan saya berharap, dalam satu dekade atau lebih, mereka akan secara rutin digunakan untuk hampir semua pengembangan perangkat lunak.

Faktanya, hubungan antara logika dan ilmu komputer begitu dalam dan meresap sehingga saya akan mengatakan bahwa sulit untuk menjadi ilmuwan komputer yang baik tanpa pemahaman logika yang menyeluruh.

Alasan beberapa ilmuwan AI meremehkan logika pada saat ini adalah bahwa beberapa pengembang awal AI telah mengusulkan logika tidak masuk akal sebagai alat.bukannya sebuah yayasan. AI, pada dasarnya, berjanji untuk memberikan sihir. Kami tidak harus melakukan pekerjaan berat dari sistem pemrograman untuk memberikan hasil. Mereka akan dapat mengetahui sendiri bagaimana menghasilkan solusi karena mereka akan "cerdas". Logika tampaknya menunjukkan jalannya karena jika sistem komputer memahami logika dan tahu bagaimana memproses informasi menggunakan aturan logika, mereka akan dapat memberikan keajaiban. Iman semacam itu dalam logika, dalam retrospeksi, salah tempat. Pertama-tama, logika di luar rak terlalu kuat dan terlalu lemah pada saat bersamaan. Terlalu kuat dalam arti bahwa aturan logika terlalu umum untuk merancang prosedur yang efektif. Ini juga terlalu lemah karena itu adalah logika yang dirancang oleh matematikawan untuk kebutuhan matematika dan tidak tidak memiliki kosa kata yang diperlukan untuk berurusan dengan banyak jenis informasi dunia nyata yang harus ditangani oleh sistem AI (seperti ketidakpastian, informasi kontekstual seperti waktu, perubahan, pengetahuan, agensi, dan sebagainya). Jadi, AI saat ini sedang mengalami serangan balik terhadap logika. Tapi saya pikir, ketika mereka mengatasi reaksi itu, para ilmuwan AI akan menyadari bahwa semua metode yang lebih baru masih didasarkanlogika, ditafsirkan secara luas .

Logika sangat mendasar bagi semua ilmu komputer teoretis. Tanpa mempelajari ini, Anda tidak akan dapat memahami semantik bahasa pemrograman dengan baik, mesin Turing, pemrograman logika, komputabilitas, dan sebagainya. Bahkan beralasan tentang program Anda akan lebih sulit tanpanya. Tentu saja, mencoba melakukan pembuktian matematis dari beberapa konsep CS hampir mustahil dilakukan.

Atau mungkin Anda bertanya tentang kegunaan dalam industri. Logika pembelajaran membentuk dasar untuk belajar bagaimana bernalar dengan jelas dan melihat lubang dalam argumen orang lain. Logika itu fundamental, apakah Anda menggunakan simbol formal atau tidak.

Salah satu tugas berulang yang dihadapi oleh praktisi dan ahli teori CS adalah mendapatkan kepercayaan pada kebenaran kode mereka.

Ada dua pendekatan utama:

1. Bukti: Merancang bukti logis bahwa bagian dari sistem memiliki sifat tertentu, mungkin dibantu oleh prasyarat, desain-kontrak, pemeriksa kode.
2. Pengujian: Menguji sifat-sifat tertentu yang menahan berbagai input dan kemudian menginduksi bahwa sifat itu berlaku untuk input lain.

Yang pertama, berdasarkan metode logis, seringkali merupakan satu-satunya pilihan ketika

1. Tidak ada input khas. Misalnya, saat menguji properti keamanan, input atipikal yang harus Anda khawatirkan, kecuali jika Anda dapat secara logis alasan tentang input mana yang atipikal, Anda tidak mungkin mendapatkan cakupan yang baik.
2. Ruang konfigurasi sangat besar, jadi Anda harus menguraikannya menjadi bagian-bagian dengan secara logis mempertimbangkan bagian mana yang dapat memengaruhi bagian lain mana sebelum menguji secara lokal.
3. Anda hanya memiliki dokumentasi yang menjelaskan perilaku tepi-kasus dari sistem di luar kendali Anda. Anda mungkin dapat mensimulasikan mereka tetapi tidak dapat menguji apa yang terjadi ketika ketergantungan eksternal gagal karena Anda tidak mampu menyebabkannya gagal karena alasan hukum atau etika.

Pengujian empiris dengan tidak adanya bukti pada dasarnya adalah pengganti untuk bukti. Saat Anda merancang sistem yang dapat diuji, Anda sedang membuat sketsa bukti tempat Anda mengisi bagian-bagian bukti dengan "test X, Y, dan Z di sini." Kemampuan untuk berpikir secara logis sangat penting untuk dapat merancang sistem yang dapat diuji. Jika sistem tidak dapat diuji atau dibuktikan maka perancang / arsiteknya tidak memiliki bisnis yang mengatakan itu sesuai untuk penggunaan yang dimaksudkan.

Dua bidang paling penting yang dimainkan oleh logika adalah:

1. Spesifikasi dan verifikasi Bahasa Formal .
2. Memperbaiki kelas traktat parameter .

Tampaknya perlu beberapa klarifikasi, dalam bahasa formal Anda perlu sangat bekerja pada logika, untuk klarifikasi lihat: 1. Bahasa formal . 2. Pengantar$Z$.

Singkatnya: 1. Definisi bahasa membutuhkan logika, 2: Keadilan prosedur itu membutuhkan logika, 3. prosedur verifikasi membutuhkan logika.

Saya harus menyebutkan bahwa ini berbeda dari desain kompiler atau ..., Ini adalah definisi "formal" bahasa, alasan utama untuk melakukan ini adalah membuktikan kebenaran bahasa atau model, juga memiliki bukti formal. Ini dapat digunakan dalam verifikasi model perangkat lunak, menemukan kesalahan sebelum implementasi, menemukan kebuntuan lagi sebelum mengimplementasikan, ...., Untuk perangkat lunak yang mensimulasikan ini, Anda dapat melihat NModel .

Sekarang mengapa dalam masalah traktat parameter tetap yang Anda perlukan untuk bekerja dengan logika, Anda dapat membagi kelas traktabilitas parameter tetap dengan berbagai tingkat logika, mereka dapat dikonversi satu sama lain: logika ke automata, automata ke grafik, dan sebaliknya, tetapi jika Anda menjadi ahli dalam logika Anda dapat membagi dan memutuskannya secara sederhana, teorema yang paling penting (setelah teorema Robertson dan Seymour ), dalam bidang ini adalah teorema Courcelle . untuk informasi lebih lanjut baca survei Meta Algorithmic Theorem .