# References to programming languages based on conditional logics

Conditional logics are logics which augment traditional logical implication with modal operators corresponding to other notions of condition (for example, the causal conditional $A\; \square\!\!\!\!\to B$ reads "$A$ causes "B", or probabilistic conditioning "$A|B$", which reads "$A$ given $B$").

Typically these logics are studied model-theoretically, but I've wondered about their applications to programming language design (for example, to type imperative actions).

I'd appreciate references to their proof theory (ie, sequent calculus/natural deduction), or to programming languages with types based on these kinds of modal operators.

Thanks!

EDIT: The Stanford Encyclopedia of Philosophy has a nice introduction to the subject.

• Hello Neel, this sounds quite interesting. I tried to Google "conditional logics" but couldn't find much. Could you please suggest an introductory paper or something to know more about CL? thank you – IamMeeoh Apr 12 '11 at 9:58

Check these references:

Programming languages CondLP and CondLP+:

Gabbay, Giordano, Martelli, Olivetti, Sapino, Conditional reasoning in logic programming, Journal of Logic Programming, Volume 44, Issues 1-3, 1 July 2000, Pages 37-74

Claudia, Oliveira, The implementation of CondLP, Lecture Notes in Computer Science, 1996, Volume 1085/1996, 713-715

Gabbay, Giordano, Martelli, Olivetti, Conditional logic programming, Proc. 11th Int. Conf. on Logic Programming, Santa Margherita Ligure, pages 272–289, 1994.

References to proof theory:

Olivetti, Pozzato, Schwind, A sequent calculus and a theorem prover for standard conditional logics, Journal ACM Transactions on Computational Logic (TOCL), Volume 8 Issue 4, August 2007

• Thanks, this looks very interesting! I was hoping to see some functional or imperative languages rather than logic languages, though. – Neel Krishnaswami Apr 12 '11 at 13:38

Church might be the kind of thing you are looking for -- it is functional (scheme derivative), but is designed with a probabilistic semantics, and implements conditional probabilities using "query" for doing Bayesian inference. Discussion of conditioning in Church. This is (as I understand it) more or less the main operation in most Church programs.

To Matteo Mio: you might also be interested in Graham Priest's book, "An introduction to non-classical logic", which is centered around defining different types of conditionals.