Referensi yang bagus tentang metode perkiraan untuk memecahkan masalah logika

13

Diketahui bahwa banyak masalah logika (misalnya masalah kepuasan beberapa logika modal) tidak dapat ditentukan. Ada juga banyak masalah yang tidak dapat dipastikan dalam teori algoritma, misalnya dalam optimasi kombinatorial. Tetapi dalam prakteknya heuristcs dan perkiraan algoritma bekerja dengan baik untuk algoritma praktis.

Jadi orang dapat berharap bahwa algoritma perkiraan untuk masalah logika dapat cocok juga. Namun satu-satunya tren penelitian sepanjang garis ini saya telah berhasil menemukan masalah max-SAT dan pengembangannya aktif di tahun sembilan puluhan.

Apakah ada beberapa tren penelitian aktif, lokakarya, kata kunci, referensi yang baik untuk penggunaan dan pengembangan metode perkiraan untuk logika modal, pemrograman logika, dan sebagainya?

Jika penalaran otomatis diharapkan untuk menonjol dalam aplikasi ilmu komputer di masa depan maka seseorang harus dapat melampaui batasan logika dan metode perkiraan atau heuristik yang dapat menjadi jalur alami untuk diikuti, bukan begitu?

lo.logic approximation-algorithms undecidability Untuk Tuan
sumber
1
"Satu-satunya tren penelitian di sepanjang garis yang saya berhasil temukan adalah masalah max-SAT dan pengembangannya aktif di tahun sembilan puluhan." Sebenarnya, pemecah MAXSAT membaik secara signifikan hari ini: maxsat.udl.cat/12/solvers/index.html
Radu GRIGore
Setelah beberapa penelitian sekarang saya cenderung berubah pikiran. Teori model hingga harus menjadi bidang yang paling prospektif untuk AI dan logika terapan. Logika yang didasarkan pada teori model infinite mungkin bagus secara estetis tetapi tidak memiliki dua koneksi penting dengan kenyataan: 1) aplikasi praktis selalu dibatasi oleh sumber daya terbatas (misalnya daftar variabel harus dibatasi); 2) dunia fisik harus dibatasi dan lebih cenderung diskrit juga (mis. Panjang fundamental dan sebagainya). Jadi - sekarang saya tidak mengerti penggunaan teori model infinite. MEREKA adalah aproksimasi.
TomR
Satu tren lain adalah "ilmu koneksi" atau integrasi neuro-simbolik - di mana logika digunakan untuk menyatakan masalah dan memberikan input dan output pembacaan perhitungan, tetapi perhitungan itu sendiri dilakukan oleh jaringan saraf. Ada beberapa diskusi seberapa kuat NN dapat (mis. Beberapa menyarankan bahwa mereka dapat menembus batas Turing hanya ketika angka nyata digunakan sebagai bobot tetapi ini dapat didiskusikan - misalnya pertanyaan terbuka apakah bilangan real ada di alam sama sekali) tetapi adalah clrar bahwa harus ada prospek untuk menggunakan metode heuristik dalam logika dan integrasi adalah satu cara.
TomR

Jawaban:

10

Motivasi yang Anda nyatakan untuk berurusan dengan ketidakpastian diputuskan berlaku untuk masalah yang sulit diputuskan tetapi juga. Jika Anda memiliki masalah yang NP-hard atau PSPACE-hard, kami biasanya harus menggunakan beberapa bentuk pendekatan (dalam arti luas istilah) untuk menemukan solusi.

Berguna untuk membedakan antara gagasan perkiraan yang berbeda.

  • Perkiraan angka: berlaku ketika Anda memiliki metrik pada ruang solusi dan Anda dapat mengukur jarak dari solusi. Ini adalah kasus untuk masalah seperti #SAT, di mana Anda menghitung solusi dan dapat merancang algoritma aproksimasi yang mengembalikan nilai di dalamnyaε solusinya.
  • Perkiraan probabilitas: ketika Anda menggunakan algoritma acak Anda bisa memberikan kepastian dalam solusi yang Anda akan dapatkan setiap kali Anda menjalankan algoritma. Anda dapat berpindah antara keacakan dalam algoritme dan keacakan dalam ruang solusi dengan mempertimbangkan distribusi probabilitas daripada solusi. Maka perkiraan di sini adalah bahwa dengan beberapa probabilitas lebih besar dariδ, Anda akan mendapatkan solusi yang benar.

Ada (ε,δ)-algoritma untuk masalah seperti ALLSAT yang menggabungkan dua perspektif di atas. Dalam kasus khusus masalah yang tidak dapat ditentukan, atau masalah di mana tidak ada metrik yang jelas dan kami tidak ingin menggunakan algoritma acak, ada pertanyaan tentang gagasan perkiraan apa yang digunakan. Masalah ini muncul secara khusus dalam analisis program dalam mengoptimalkan penyusun dan verifikasi program. Menentukan sifat-sifat kompleks dari program dapat diputuskan atau mahal secara komputasi, sehingga beberapa bentuk pendekatan diperlukan.

Berikut adalah contoh gagasan perkiraan yang berbeda. Misalkan Anda melakukan perhitungan seperti mengalikan dua angka besar dan ingin memeriksa apakah perkaliannya benar. Ada banyak teknik heuristik yang digunakan dalam praktik untuk memeriksa kebenaran tanpa mengulangi perhitungan lagi. Anda dapat memeriksa bahwa tanda-tanda itu dikalikan untuk mendapatkan tanda yang benar. Anda dapat memeriksa apakah angka memiliki paritas yang tepat (properti genap / ganjil). Anda dapat menggunakan pemeriksaan yang lebih canggih seperti Casting out nines. Semua teknik ini memiliki properti umum yang dapat mereka beri tahu jika Anda melakukan kesalahan, tetapi mereka tidak dapat menjamin jika Anda mendapat jawaban yang benar. Properti ini dapat dilihat sebagai perkiraan logis karena Anda mungkin dapat membuktikan bahwa perhitungan asli salah tetapi Anda mungkin tidak dapat membuktikan bahwa itu benar.

Semua cek yang saya sebutkan di atas adalah contoh teknik yang disebut interpretasi abstrak. Interpretasi abstrak membuat sepenuhnya dugaan dugaan logis berbeda dari perkiraan numerik dan probabilistik. Masalah yang saya jelaskan dengan analisis perhitungan tunggal meluas ke kasus analisis program yang lebih kompleks. Literatur tentang interpretasi abstrak telah mengembangkan teknik dan kerangka kerja untuk perkiraan, penalaran logis tentang program, dan baru-baru ini tentang logika. Referensi berikut mungkin berguna.

  1. Abstrak Interpretasi Singkatnya oleh Patrick Cousot, yang merupakan gambaran sederhana.
  2. Tinjauan Abstraksi oleh Patrick Cousot, sebagai bagian dari programnya. Ada contoh abstraksi yang sangat bagus untuk menentukan properti dari sekuntum bunga. Analogi buket mencakup titik-titik tetap dan dapat dibuat benar-benar tepat secara matematis.
  3. Kursus tentang Interpretasi Abstrak oleh Patrick Cousot, jika Anda ingin semua kedalaman dan detail.
  4. Interpretasi abstrak dan aplikasi untuk program logika , Patrick Cousot dan Radhia Cousot, 1992. Berlaku untuk program logika, sesuai permintaan Anda. Bagian awal juga meresmikan prosedur penugasan sembilan sebagai interpretasi abstrak.

Semua ini biasanya diterapkan pada alasan tentang program komputer. Telah ada pekerjaan yang cukup baru pada penerapan ide-ide dari interpretasi abstrak untuk mempelajari prosedur keputusan logika. Fokusnya bukan modal logika tetapi kepuasan dalam logika proposisional dan teori first-order bebas-kuantifier. (Karena saya telah bekerja di ruang ini, satu kertas di bawah ini adalah milik saya)

  1. Generalisasi metode Staalmarck oleh Aditya Thakur dan Thomas Reps, 2012. Memberikan generalisasi metode Staalmarck untuk masalah dalam analisis program.
  2. Produk berkurang dari domain abstrak dan kombinasi prosedur keputusan , Patrick Cousot, Radhia Cousot, dan Laurent Mauborgne, 2011. Makalah ini mempelajari teknik Nelson-Oppen untuk menggabungkan prosedur keputusan dan menunjukkan bahwa itu juga dapat digunakan untuk kombinasi tidak lengkap, yang sangat menarik jika Anda memiliki masalah yang tidak dapat ditentukan.
  3. Pemecah Kepuasan adalah Analisis Statis , makalah saya dengan Leopold Haller dan Daniel Kroening, 2012. Menerapkan pandangan pendekatan berbasis kisi untuk mengkarakterisasi pemecah yang ada. Anda juga bisa melihat slide saya pada topik , sebagai gantinya.

Sekarang tidak ada kertas di atas yang menjawab pertanyaan spesifik Anda tentang menyerang masalah kepuasan yang tidak dapat diputuskan. Apa yang dilakukan oleh makalah ini adalah mengambil tampilan berorientasi masalah logis yang tidak numerik atau probabilistik. Pandangan ini telah diterapkan secara luas pada alasan tentang program dan saya percaya ini menjawab apa yang Anda tanyakan.

Untuk menerapkannya pada modal logika, saya akan menyarankan titik awal adalah menggunakan semantik aljabar Jonsson dan Tarski atau semantik selanjutnya dari Lemmon dan Scott. Ini karena interpretasi abstrak dirumuskan dalam hal fungsi kisi dan monoton, sehingga aljabar Boolean dengan operator adalah semantik yang nyaman untuk digunakan. Jika Anda ingin memulai dengan bingkai Kripke, Anda dapat menerapkan teorema dualitas Jonsson dan Tarski (yang beberapa orang menyebutnya dualitas Batu) dan mendapatkan representasi aljabar. Setelah itu, Anda dapat menerapkan teorema interpretasi abstrak untuk pendekatan logis.

Vijay D
sumber