11
$\begingroup$

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.

Improve this question
$\endgroup$
1
  • $\begingroup$ 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 $\endgroup$
    – OldFella
    Apr 12, 2011 at 9:58

2 Answers 2

Reset to default
8
$\begingroup$

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

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks, this looks very interesting! I was hoping to see some functional or imperative languages rather than logic languages, though. $\endgroup$
    – Neel Krishnaswami
    Apr 12, 2011 at 13:38
3
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.