An epistemic model for decentralized discrete-event systems with non-binary control is presented. This framework combines existing work on conditional control decisions with existing work on formal reasoning about knowledge in discrete-event systems. The novelty in the model presented is that the necessary and sufficient conditions for problem solvability encapsulate the actions that supervisors must take. This direct coupling between knowledge and action -- in a formalism that mimics natural language -- makes it easier, when the problem conditions fail, to determine how the problem requirements should be revised.

To design and engineer ethical and legal reasoners and responsible systems, Benzm\"{u}ller, Parent and van der Torre introduce LogiKEy methodology based on the semantical embedding of deontic logics into classic higher-order logic. In this paper, we considerably extend the LogiKEy deontic logics and dataset using an algebraic approach. We develop theory of input/output operations for normative reasoning on top of Boolean algebras.

If an agent, or a coalition of agents, has a strategy, knows that she has a strategy, and knows what the strategy is, then she has a know-how strategy. Several modal logics of coalition power for know-how strategies have been studied before. The contribution of the article is three-fold. First, it proposes a new class of know-how strategies that depend on the intelligence information about the opponents' actions. Second, it shows that the coalition power modality for the proposed new class of strategies cannot be expressed through the standard know-how modality. Third, it gives a sound and complete logical system that describes the interplay between the coalition power modality with intelligence and the distributed knowledge modality in games with imperfect information.

We approach the question "What is Consciousness?" in a new way, not as Descartes' "systematic doubt", but as how organisms find their way in their world. Finding one's way involves finding possible uses of features of the world that might be beneficial or avoiding those that might be harmful. "Possible uses of X to accomplish Y" are "Affordances". The number of uses of X is indefinite (or unknown), the different uses are unordered and are not deducible from one another. All biological adaptations are either affordances seized by heritable variation and selection or, far faster, by the organism acting in its world finding uses of X to accomplish Y. Based on this, we reach rather astonishing conclusions: (1) Artificial General Intelligence based on Universal Turing Machines (UTMs) is not possible, since UTMs cannot "find" novel affordances. (2) Brain-mind is not purely classical physics for no classical physics system can be an analogue computer whose dynamical behavior can be isomorphic to "possible uses". (3) Brain mind must be partly quantum - supported by increasing evidence at 6.0 sigma to 7.3 Sigma. (4) Based on Heisenberg's interpretation of the quantum state as "Potentia" converted to "Actuals" by Measurement, a natural hypothesis is that mind actualizes Potentia. This is supported at 5.2 Sigma. Then Mind's actualizations of entangled brain-mind-world states are experienced as qualia and allow "seeing" or "perceiving" of uses of X to accomplish Y. We can and do jury-rig. Computers cannot. (5) Beyond familiar quantum computers, we discuss the potentialities of Trans-Turing-Systems.

In this paper we introduce a simple modal logic framework to reason about the expertise of an information source. In the framework, a source is an expert on a proposition $p$ if they are able to correctly determine the truth value of $p$ in any possible world. We also consider how information may be false, but true after accounting for the lack of expertise of the source. This is relevant for modelling situations in which information sources make claims beyond their domain of expertise. We use non-standard semantics for the language based on an expertise set with certain closure properties. It turns out there is a close connection between our semantics and S5 epistemic logic, so that expertise can be expressed in terms of knowledge at all possible states. We use this connection to obtain a sound and complete axiomatisation.

We describe how answer-set programs can be used to declaratively specify counterfactual interventions on entities under classification, and reason about them. In particular, they can be used to define and compute responsibility scores as attribution-based explanations for outcomes from classification models. The approach allows for the inclusion of domain knowledge and supports query answering. A detailed example with a naive-Bayes classifier is presented.

Saturation-style automated theorem provers (ATPs) based on the given clause procedure are today the strongest general reasoners for classical first-order logic. The clause selection heuristics in such systems are, however, often evaluating clauses in isolation, ignoring other clauses. This has changed recently by equipping the E/ENIGMA system with a graph neural network (GNN) that chooses the next given clause based on its evaluation in the context of previously selected clauses. In this work, we describe several algorithms and experiments with ENIGMA, advancing the idea of contextual evaluation based on learning important components of the graph of clauses.

We propose an approach based on Answer Set Programming for reasoning about actions with domain descriptions including ontological knowledge, expressed in the lightweight description logic EL^\bot. We consider a temporal action theory, which allows for non-deterministic actions and causal rules to deal with ramifications, and whose extensions are defined by temporal answer sets. We provide conditions under which action consistency can be guaranteed with respect to an ontology, by a polynomial encoding of an action theory extended with an EL^\bot knowledge base (in normal form) into a temporal action theory.

Constraint answer set programming or CASP, for short, is a hybrid approach in automated reasoning putting together the advances of distinct research areas such as answer set programming, constraint processing, and satisfiability modulo theories. Constraint answer set programming demonstrates promising results, including the development of a multitude of solvers: acsolver, clingcon, ezcsp, idp, inca, dingo, mingo, aspmt, clingo[l,dl], and ezsmt. It opens new horizons for declarative programming applications such as solving complex train scheduling problems. Systems designed to find solutions to constraint answer set programs can be grouped according to their construction into, what we call, integrational or translational approaches. The focus of this paper is an overview of the key ingredients of the design of constraint answer set solvers drawing distinctions and parallels between integrational and translational approaches. The paper also provides a glimpse at the kind of programs its users develop by utilizing a CASP encoding of Travelling Salesman problem for illustration. In addition, we place the CASP technology on the map among its automated reasoning peers as well as discuss future possibilities for the development of CASP.

We convert the DeepMind Mathematics Dataset into a reinforcement learning environment by interpreting it as a program synthesis problem. Each action taken in the environment adds an operator or an input into a discrete compute graph. Graphs which compute correct answers yield positive reward, enabling the optimization of a policy to construct compute graphs conditioned on problem statements. Baseline models are trained using Double DQN on various subsets of problem types, demonstrating the capability to learn to correctly construct graphs despite the challenges of combinatorial explosion and noisy rewards.