Deontic logics are formalisms for reasoning over norms, obligations, permissions and prohibitions. Input/Output (I/O) Logics are a particular family of so-called norm-based deontic logics that formalize conditional norms outside of the underlying object logic language, where conditional norms do not carry a truth-value themselves. In this paper, an automation approach for I/O logics is presented that makes use of suitable reductions to (sequences of) propositional satisfiability problems. A prototypical implementation, named rio (reasoner for input/output logics), of the proposed procedures is presented and applied to illustrative examples.
The logic IK is the intuitionistic variant of modal logic introduced by Fischer Servi, Plotkin and Stirling, and studied by Simpson. This logic is considered a fundamental intuitionstic modal system as it corresponds, modulo the standard translation, to a fragment of intuitionstic first-order logic. In this paper we present a labelled-free bi-nested sequent calculus for IK. This proof system comprises two kinds of nesting, corresponding to the two relations of bi-relational models for IK: a pre-order relation, from intuitionistic models, and a binary relation, akin to the accessibility relation of Kripke models. The calculus provides a decision procedure for IK by means of a suitable proof-search strategy. This is the first labelled-free calculus for IK which allows direct counter-model extraction: from a single failed derivation, it is possible to construct a finite countermodel for the formula at the root. We further show the bi-nested calculus can simulate both the (standard) nested calculus and labelled sequent calculus, which are two best known calculi proposed in the literature for IK.
We consider a family of two-valued "fully evaluated left-sequential logics" (FELs), of which Free FEL (defined by Staudt in 2012) is most distinguishing (weakest) and immune to atomic side effects. Next is Memorising FEL, in which evaluations of subexpressions are memorised. The following stronger logic is Conditional FEL (inspired by Guzmán and Squier's Conditional logic, 1990). The strongest FEL is static FEL, a sequential version of propositional logic. We use evaluation trees as a simple, intuitive semantics and provide complete axiomatisations for closed terms (left-sequential propositional expressions). For each FEL except Static FEL, we also define its three-valued version, with a constant U for "undefinedness" and again provide complete, independent axiomatisations, each one containing two additional axioms for U on top of the axiomatisations of the two-valued case. In this setting, the strongest FEL is equivalent to Bochvar's strict logic.
Theory of Mind (ToM), the cognitive capacity to attribute internal mental states to oneself and others, is a crucial component of social skills. Its formal study has become important, witness recent research on reasoning and information update by intelligent agents, and some proposals for its formal modelling have put forward settings based on Epistemic Logic (EL). Still, due to intrinsic idealisations, it is questionable whether EL can be used to model the high-order cognition of 'real' agents. This manuscript proposes a framework that takes visibility, memory, perspective and communication as the main factors underpinning mental attributions. This is more in-line with findings in cognitive science and allows us to model well-known False-Belief Tasks that are typically used in testing people's ToM. We discuss some of the framework's technical features, arguing why it does justice to empirical observations.
For a dialetheist, it is rational to believe that true contradictions exist. However, we argue that a dialetheist faces a complex dilemma given some bridge principles for rational beliefs that connect possibility and probability, including the so-called 'Regularity Principle'. Either her belief is not doxastically possible even for her, or she must assign positive credence to the proposition that dialetheia exists. The former makes her belief prima facie self-defeating. The latter seems to compel her to choose between several more fine-grained options, each of which seems undesirable for a regular and rational probability theory. It is unclear how a dialetheist would stay rationally regular, so we pose this challenge, seeking a response from a dialetheist.
