Are there extensions of predicate logic which focus on resource models, possibly even in actor models?

And if so, would it be possible to reason on a meta-level on how many resources should be expended to find further proofs in the same or other systems?

  • $\begingroup$ First order linear logic ? What do you mean by "resource"? $\endgroup$ – Boris Jan 16 '19 at 8:36
  • $\begingroup$ try linear logic (and now I see that I'm merely replaying the previous comment) so if we had linearity in the comment space, I could not have made the exact same comment as my predecessor. $\endgroup$ – Kai Jan 16 '19 at 11:26

Do you mean a resource-aware logic? If so, yes, there's linear logic [Girard, 1987] (as was already noted in the comments). It has had a big influence on the study of concurrency and implicit computational complexity. You might be interested in the latter, where reasoning is focused on the efficiency of programs.

What do you mean exactly by "actor models"? If you mean concurrency, please have a look at: What is the Curry-Howard analogue for linear logics? If you mean identifying who/what uses/implements resources at the level of propositions, we explored an extension of linear logic for that [Carbone et al., 2016], but mainly for the notion of communication protocol (who performs which communications). Useful inspiration might also come from hybrid logics that support notions of "worlds", like this one: https://www.cs.cmu.edu/~rwh/theses/reed.pdf

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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