We develop a cut-free nested sequent calculus as basis for a proof search procedure for an intuitionistic modal logic of actions and propositions. The actions act on propositions via a dynamic modality (the weakest precondition of program logics), whose ...
In this paper we provide the first (as far as we know) direct calculus deciding satisfiability of formulae in negation normal form in the fragment of FHL (full hybrid logic with the binder, including the global and converse modalities), where no ...
In this paper we study a version of constructive linear-time temporal logic (LTL) with the ''next'' temporal operator. The logic is originally due to Davies, who has shown that the proof system of the logic corresponds to a type system for binding-time ...
International Foundation for Autonomous Agents and Multiagent Systems
Richland, SC
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in
