Referensi ke bahasa pemrograman berdasarkan pada logika kondisional

11

Logika bersyarat adalah logika yang menambah implikasi logis tradisional dengan operator modal yang sesuai dengan pengertian kondisi lainnya (misalnya, kondisional kausal Ke berbunyi " menyebabkan" B ", atau pengkondisian probabilistik " ", yang bertuliskan " given ").A A | B A BA◻→BAA|BAB

Biasanya logika ini dipelajari model-secara teoritis, tetapi saya bertanya-tanya tentang aplikasi mereka untuk merancang bahasa pemrograman (misalnya, untuk mengetik tindakan imperatif).

Saya akan menghargai referensi teori pembuktian mereka (yaitu, kalkulus berurutan / deduksi alami), atau ke bahasa pemrograman dengan tipe berdasarkan pada jenis ini dari operator modal.

Terima kasih!

EDIT: The Stanford Encyclopedia of Philosophy memiliki pengantar yang bagus untuk subjek .

reference-request lo.logic pl.programming-languages type-theory proof-theory Neel Krishnaswami
sumber
Halo Neel, ini kedengarannya cukup menarik. Saya mencoba Google "logika kondisional" tetapi tidak menemukan banyak. Bisakah Anda menyarankan makalah pengantar atau sesuatu untuk mengetahui lebih banyak tentang CL? terima kasih
IamMeeoh

Jawaban:

8

Periksa referensi ini:

Bahasa pemrograman CondLP dan CondLP +:

Gabbay, Giordano, Martelli, Olivetti, Sapino, Penalaran bersyarat dalam pemrograman logika, Jurnal Pemrograman Logika, Volume 44, Masalah 1-3, 1 Juli 2000, Halaman 37-74

Claudia, Oliveira, Implementasi CondLP, Catatan Kuliah dalam Ilmu Komputer, 1996, Volume 1085/1996, 713-715

Gabbay, Giordano, Martelli, Olivetti, pemrograman logika kondisional, Proc. Int 11. Conf. tentang Pemrograman Logika, Santa Margherita Ligure, halaman 272–289, 1994.

Referensi teori pembuktian:

Olivetti, Pozzato, Schwind, Kalkulus berurutan dan teorema teorema untuk logika kondisional standar, Jurnal ACM Transaction on Computational Logic (TOCL), Volume 8 Edisi 4, Agustus 2007

Mohammad Al-Turkistany
sumber
Terima kasih, ini terlihat sangat menarik! Saya berharap untuk melihat beberapa bahasa fungsional atau imperatif daripada bahasa logika.
Neel Krishnaswami
3

Gereja mungkin jenis hal yang Anda cari - itu fungsional (skema turunan), tetapi dirancang dengan semantik probabilistik, dan mengimplementasikan probabilitas bersyarat menggunakan "kueri" untuk melakukan inferensi Bayesian. Diskusi pengkondisian di Gereja . Ini (seperti yang saya mengerti) kurang lebih merupakan operasi utama di sebagian besar program Gereja.

Bagi Matteo Mio: Anda mungkin juga tertarik dengan buku Graham Priest, "Pengantar logika non-klasik", yang dipusatkan pada pendefinisian berbagai jenis kondisional.

kgr
sumber