We extend the monotonic and regular modal logics to the multi-modal cue, and give semantical characterization w.r.t. a semantics of minimal frames. For this we introduce a calculus over neighbourhoods and we obtain simpler conditions than those from the literature.

We investigate under what conditions contrary-to-duty (CTD) structures lacking temporal and action elements can be given a coherent reading. We argue, contrary to some recent proposals, that CTD is not an instance of defeasible reasoning, and that methods of nonmonotonic logics are inadequate since they are unable to distinguish between defeasibility and violation of primary obligations. We propose a semantic framework based on the idea that primary and CTD obligations are obligations of different kinds: a CTD obligation pertains to, or (...) pre-supposes, a certain context in which a primary obligation is already violated. This framework is presented initially as an extension of Standard Deontic Logic (SDL), a normal modal logic of type KD, and is illustrated by application to a series of examples. The concluding section is concerned with some resemblances between CTD and defeasible reasoning. We show first that the SDL-based framework contains a flaw and must be adjusted. A discussion of possible adjustments, including an alternative treatment in terms of a preference-based semantics, reveals difficulties that are reminiscent of problems in defeasible reasoning and intensional accounts of defeasible conditionals. (shrink)

How should a machine intelligence perform unsupervised structure discovery over streams of sensory input? One approach to this problem is to cast it as an apperception task [1]. Here, the task is to construct an explicit interpretable theory that both explains the sensory sequence and also satisfies a set of unity conditions, designed to ensure that the constituents of the theory are connected in a relational structure. However, the original formulation of the apperception task had one fundamental limitation: it assumed (...) the raw sensory input had already been parsed using a set of discrete categories, so that all the system had to do was receive this already-digested symbolic input, and make sense of it. But what if we don't have access to pre-parsed input? What if our sensory sequence is raw unprocessed information? The central contribution of this paper is a neuro-symbolic framework for distilling interpretable theories out of streams of raw, unprocessed sensory experience. First, we extend the definition of the apperception task to include ambiguous (but still symbolic) input: sequences of sets of disjunctions. Next, we use a neural network to map raw sensory input to disjunctive input. Our binary neural network is encoded as a logic program, so the weights of the network and the rules of the theory can be solved jointly as a single SAT problem. This way, we are able to jointly learn how to perceive (mapping raw sensory information to concepts) and apperceive (combining concepts into declarative rules). (shrink)

We investigate an extension of the formalism of interpreted systems by Halpern and colleagues to model the correct behaviour of agents. The semantical model allows for the representation and reasoning about states of correct and incorrect functioning behaviour of the agents, and of the system as a whole. We axiomatise this semantic class by mapping it into a suitable class of Kripke models. The resulting logic, KD45n i-j, is a stronger version of KD, the system often referred to as Standard (...) Deontic Logic. We extend this formal framework to include the standard epistemic notions defined on interpreted systems, and introduce a new doubly-indexed operator representing the knowledge that an agent would have if it operates under the assumption that a group of agents is functioning correctly. We discuss these issues both theoretically and in terms of applications, and present further directions of work. (shrink)

This paper attempts to answer a central question in unsupervised learning: what does it mean to “make sense” of a sensory sequence? In our formalization, making sense involves constructing a symbolic causal theory that both explains the sensory sequence and also satisfies a set of unity conditions. The unity conditions insist that the constituents of the causal theory – objects, properties, and laws – must be integrated into a coherent whole. On our account, making sense of sensory input is a (...) type of program synthesis, but it is unsupervised program synthesis. Our second contribution is a computer implementation, the Apperception Engine, that was designed to satisfy the above requirements. Our system is able to produce interpretable human-readable causal theories from very small amounts of data, because of the strong inductive bias provided by the unity conditions. A causal theory produced by our system is able to predict future sensor readings, as well as retrodict earlier readings, and impute (fill in the blanks of) missing sensory readings, in any combination. In fact, it is able to do all three tasks simultaneously. We tested the engine in a diverse variety of domains, including cellular automata, rhythms and simple nursery tunes, multi-modal binding problems, occlusion tasks, and sequence induction intelligence tests. In each domain, we test our engine's ability to predict future sensor values, retrodict earlier sensor values, and impute missing sensory data. The Apperception Engine performs well in all these domains, significantly out-performing neural net baselines. We note in particular that in the sequence induction intelligence tests, our system achieved human-level performance. This is notable because our system is not a bespoke system designed specifically to solve intelligence tests, but a general-purpose system that was designed to make sense of any sensory sequence. (shrink)

This paper formalizes part of the cognitive architecture that Kant develops in the Critique of Pure Reason. The central Kantian notion that we formalize is the rule. As we interpret Kant, a rule is not a declarative conditional stating what would be true if such and such conditions hold. Rather, a Kantian rule is a general procedure, represented by a conditional imperative or permissive, indicating which acts must or may be performed, given certain acts that are already being performed. These (...) acts are not propositions; they do not have truth-values. Our formalization is related to the input/ output logics, a family of logics designed to capture relations between elements that need not have truth-values. In this paper, we introduce KL3 as a formalization of Kant’s conception of rules as conditional imperatives and permissives. We explain how it differs from standard input/output logics, geometric logic, and first-order logic, as well as how it translates natural language sentences not well captured by first-order logic. Finally, we show how the various distinctions in Kant’s much-maligned Table of Judgements emerge as the most natural way of dividing up the various types and sub-types of rule in KL3. Our analysis sheds new light on the way in which normative notions play a fundamental role in the conception of logic at the heart of Kant’s theoretical philosophy. (shrink)

The authors describe a logic programming approach to the representation of legislative texts. They consider the potential uses of simple systems which incorporate a single, fixed interpretation of a text. These include assisting in the routine administration of complex areas of the law. The authors also consider the possibility of constructing more complex systems which incorporate several, possibly conflicting interpretations. Such systems are needed for dealing with ambiguity and vagueness in the law. Moreover, they are more suitable than single interpretation (...) systems for helping to test proposed legislation and for helping to give citizens advice. (shrink)

One of the best known approaches to the logic of agency are the ‘stit’ logics. Often, it is not the actions of an individual agent that bring about a certain outcome but the joint actions of a set of agents, collectively. Collective agency has received comparatively little attention in ‘stit’. The paper maps out several different forms, several different senses in which a particular set of agents, collectively, can be said to bring about a certain outcome, and examines how these (...) forms can be expressed in ‘stit’ and stit-like logics. The outcome that is brought about may be unintentional, and perhaps even accidental; the account deliberately ignores aspects such as joint intention, communication between agents, awareness of other agents’ intentions and capabilities, even the awareness of another agent’s existence. The aim is to investigate what can be said about collective agency when all such considerations are ignored, besides mere consequences of joint actions. The account will be related to the ‘strictly stit’ of Belnap and Perloff, 25–48 1993) and their suggestions concerning ‘inessential members’ and ‘mere bystanders’. We will adjust some of those conjectures and distinguish further between ‘potentially contributing bystanders’ and ‘impotent bystanders’. (shrink)

The action language C+ of Giunchiglia, Lee, Lifschitz, McCain and Turner is a high-level, logical formalism for the representation of domains involving action and change. However, one cannot directly express relationships which hold between states more than one time-step distant, or even say that one action determines another at the next time. We present C+timed, a generalization of C+ which removes these limitations. As for C+, translations to the language of causal theories are given. We also define a new kind (...) of transition system called a ‘run system’ to provide a graphical semantics. Finally, we show how domains involving prohibition and permission can be modelled, by incorporating the ideas of another extension of C+. (shrink)

This paper studies some normative relations that hold between actions, their preconditions and their effects, with particular attention to connecting what are often called ‘ought to be’ norms with ‘ought to do’ norms. We use a formal model based on a form of transition system called a ‘coloured labelled transition system’ (coloured LTS) introduced in a series of papers by Sergot and Craven. Those works have variously presented a formalism (an ‘action language’) nC+ for defining and computing with a (coloured) (...) LTS, and another, separate formalism, a modal language interpreted on a (coloured) LTS used to express its properties. We consolidate these two strands. Instead of specifying the obligatory and prohibited states and transitions as part of the construction of a coloured LTS as in nC+, we represent norms in the modal language and use those to construct a coloured LTS from a given regular (uncoloured) one. We also show how connections between norms on states and norms on transitions previously treated as fixed constraints of a coloured LTS can instead be defined within the modal language used for representing norms. (shrink)

Multi-agent systems where the agents are developed by parties with competing interests, and where there is no access to an agent’s internal state, are often classified as ‘open’. The members of such systems may inadvertently fail to, or even deliberately choose not to, conform to the system specification. Consequently, it is necessary to specify the normative relations that may exist between the members, such as permission, obligation, and institutional power. We present a framework being developed for executable specification of open (...) multi-agent systems. We adopt a bird’s eye view of these systems, as opposed to an agent’s perspective whereby it reasons about how it should act. This paper is devoted to the presentation of various examples from the NetBill protocol formalised in terms of institutional power, permission and obligation. We express the system specification in the Event Calculus and execute the specification by means of a logic programming implementation. We also give several example formalisations of sanctions for dealing with violations of permissions and obligations. We distinguish between an open multi-agent system and the procedure by which an agent enters and leaves the system. We present examples from the specification of a role-management protocol for NetBill, and demonstrate the interplay between such a protocol and the corresponding multi-agent system. (shrink)

The paper outlines ongoing research on logic-based tools for the analysis and representation of legal contracts, of the kind frequently encountered in large-scale engineering projects and complex, long-term trading agreements. We consider both contract formation and contract performance, in each case identifying the representational issues and the prospects for providing automated support tools.

The paper tackles the problem of the relation between rights and obligations. Two examples of situations in which such a relation occurs are discussed. One concerns the abortion regulations in Polish law, the other one—a clash between freedom of expression and freedom of enterprise occurring in the context of discrimination. The examples are analysed and formalised using labelled transition systems in the \ framework. Rights are introduced to the system as procedures allowing for their fulfilment. Obligations are based on the (...) requirement of cooperation in the realisation of the goals of the agent that has a right. If the right of an agent cannot be fulfilled without an action of another agent, then that action is obligatory for that agent. If there are many potential contributors who are individually allowed to refuse, then the last of them is obliged to help when all the others have already refused. By means of formalisation this account of the relation under consideration is precisely expressed and shown consistent. (shrink)

There seems to be no clear consensus in the existing literature about the role of deontic logic in legal knowledge representation — in large part, we argue, because of an apparent misunderstanding of what deontic logic is, and a misplaced preoccupation with the surface formulation of legislative texts. Our aim in this paper is to indicate, first, which aspects of legal reasoning are addressed by deontic logic, and then to sketch out the beginnings of a methodology for its use in (...) the analysis and representation of law.The essential point for which we argue is that deontic logic — in some form or other —needs to be taken seriously whenever it is necessary to make explicit, and then reason about, the distinction between what ought to be the case and what is the case, or as we also say, between the ideal and the actual. We take the library regulations at Imperial College as the main illustration, and small examples from genuinely legal domains to introduce specific points. In conclusion, we touch on the role of deontic logic in the development of the theory of normative positions. (shrink)