Odniesienia do języków programowania opartych na logice warunkowej

11

Logiki warunkowe to logiki, które rozszerzają tradycyjną implikację logiczną za pomocą operatorów modalnych odpowiadających innym pojęciom warunku (na przykład przyczynowy warunkowy brzmi „ powoduje„ B ”lub warunkowanie probabilistyczne „ ”, które brzmi „ dany B ”).A A | B AA◻→BAA|BAB

Zazwyczaj logiki te są badane teoretycznie modelowo, ale zastanawiałem się nad ich zastosowaniami do projektowania języka programowania (na przykład do wpisywania akcji imperatywnych).

Doceniłbym odniesienia do ich teorii dowodu (tj. Rachunku sekwencyjnego / dedukcji naturalnej) lub języków programowania z typami opartymi na tego rodzaju operatorach modalnych.

Dzięki!

EDYCJA: Encyklopedia filozofii Stanforda ma dobre wprowadzenie do tematu .

reference-request lo.logic pl.programming-languages type-theory proof-theory Neel Krishnaswami
źródło
Cześć Neel, to brzmi całkiem interesująco. Próbowałem zastosować w Google „logikę warunkową”, ale nie znalazłem wiele. Czy mógłbyś zasugerować artykuł wprowadzający lub dowiedzieć się więcej o CL? dziękuję
IamMeeoh,

Odpowiedzi:

8

Sprawdź te referencje:

Języki programowania CondLP i CondLP +:

Gabbay, Giordano, Martelli, Olivetti, Sapino, Argumentacja warunkowa w programowaniu logiki, Journal of Logic Programming, tom 44, numery 1-3, 1 lipca 2000 r., Strony 37-74

Claudia, Oliveira, Implementacja CondLP, Wykłady z informatyki, 1996, Tom 1085/1996, 713-715

Gabbay, Giordano, Martelli, Olivetti, Programowanie logiki warunkowej, Proc. 11th Int. Konf. on Logic Programming, Santa Margherita Ligure, strony 272–289, 1994.

Odniesienia do teorii dowodów:

Olivetti, Pozzato, Schwind, Rachunek sekwencyjny i twierdzenie o twierdzeniach dla standardowych logik warunkowych, Journal ACM Transactions on Computational Logic (TOCL), tom 8 wydanie 4, sierpień 2007

Mohammad Al-Turkistany
źródło
Dzięki, to wygląda bardzo interesująco! Miałem jednak nadzieję zobaczyć języki funkcjonalne lub imperatywne zamiast języków logicznych.
Neel Krishnaswami,
3

Kościół może być czymś, czego szukasz - jest funkcjonalny (pochodna schematu), ale został zaprojektowany z semantyką probabilistyczną i implementuje prawdopodobieństwa warunkowe za pomocą „zapytania” w celu wnioskowania bayesowskiego. Dyskusja uwarunkowań w Kościele . Jest to (jak rozumiem) mniej więcej główna operacja w większości programów kościelnych.

Do Matteo Mio: możesz zainteresować się także książką Grahama Priesta „Wprowadzenie do logiki nieklasycznej”, która koncentruje się na definiowaniu różnych typów warunków warunkowych.

kgr
źródło