The Practical Significance of Kant’s Categorical Imperative

On a standard interpretation, the aim of the formula of universal law is to provide a decision procedure for determining the deontic status of actions. By contrast, this chapter argues for the practical significance of the Categorical Imperative (CI) centering on Kant’s account of the dynamics of incentives. This approach avoids some widespread misconceptions about how the CI operates and false expectations about what it promises and delivers. In particular, it explains how it differs from deductive practical inferences. The CI is the supreme form of morality, and yet not in the sense that particular categorical principles can be derived deductively from it, once the relevant details are supplied. The efficacy of practical reasoning primarily concerns agents and consists in their reorientation toward the right end. Moral knowledge is knowledge about what we ought to do, but it is also a distinctive variety of self-knowledge, that is, knowledge of ourselves as rationally efficacious agents.

Tight Polynomial Bounds for Loop Programs in Polynomial Space

We consider the following problem: given a program, find tight asymptotic bounds on the values of some variables at the end of the computation (or at any given program point) in terms of its input values. We focus on the case of polynomially-bounded variables, and on a weak programming language for which we have recently shown that tight bounds for polynomially-bounded variables are computable. These bounds are sets of multivariate polynomials. While their computability has been settled, the complexity of this program-analysis problem remained open. In this paper, we show the problem to be PSPACE-complete. The main contribution is a new, space-efficient analysis algorithm. This algorithm is obtained in a few steps. First, we develop an algorithm for univariate bounds, a sub-problem which is already PSPACE-hard. Then, a decision procedure for multivariate bounds is achieved by reducing this problem to the univariate case; this reduction is orthogonal to the solution of the univariate problem and uses observations on the geometry of a set of vectors that represent multivariate bounds. Finally, we transform the univariate-bound algorithm to produce multivariate bounds.

Integrating Cardinality Constraints into Constraint Logic Programming with Sets

Formal reasoning about finite sets and cardinality is important for many applications, including software verification, where very often one needs to reason about the size of a given data structure. The Constraint Logic Programming tool $$\{ log\} $$ provides a decision procedure for deciding the satisfiability of formulas involving very general forms of finite sets, although it does not provide cardinality constraints. In this paper we adapt and integrate a decision procedure for a theory of finite sets with cardinality into $$\{ log\} $$ . The proposed solver is proved to be a decision procedure for its formulas. Besides, the new CLP instance is implemented as part of the $$\{ log\} $$ tool. In turn, the implementation uses Howe and King’s Prolog SAT solver and Prolog’s CLP(Q) library, as an integer linear programming solver. The empirical evaluation of this implementation based on +250 real verification conditions shows that it can be useful in practice. Under consideration in Theory and Practice of Logic Programming (TPLP)

Time is of the essence: Explaining the duration of European Union lawmaking under the co-decision procedure

The article explores factors affecting the duration of the co-decision procedure (currently the ordinary legislative procedure), the main procedure for adopting legislation in the European Union. Drawing from rational choice institutionalism, it expects the speed of co-decision to be determined by three attributes: the impatience of legislators, issue linkage and the characteristics of Council and European Parliament negotiators ( relais actors). The hypotheses are tested using survival analysis on a dataset of 599 controversial legislative acts submitted and enacted under co-decision between 1999 and 2009. The results show that co-decision proposals are decided faster when they are urgent, negotiated prior to the European Parliament elections and concluded through single proposal logrolls. By contrast, multi-proposal packages and the ideological distance between relais actors prolong decision-making. Overall, the article contributes to the literature by showing that the impatience of legislators, package deals and the properties of negotiators are relevant drivers of co-decision duration.

Equivalence checking for weak bi-Kleene algebra

Pomset automata are an operational model of weak bi-Kleene algebra, which describes programs that can fork an execution into parallel threads, upon completion of which execution can join to resume as a single thread. We characterize a fragment of pomset automata that admits a decision procedure for language equivalence. Furthermore, we prove that this fragment corresponds precisely to series-rational expressions, i.e., rational expressions with an additional operator for bounded parallelism. As a consequence, we obtain a new proof that equivalence of series-rational expressions is decidable.

Optimization of a Depiction Procedure for an Artificial Intelligence-Based Network Protection System Using a Genetic Algorithm

The current demand for remote work, remote teaching and video conferencing has brought a surge not only in network traffic, but unfortunately, in the number of attacks as well. Having reliable, safe and secure functionality of various network services has never been more important. Another serious phenomenon that is apparent these days and that must not be discounted is the growing use of artificial intelligence techniques for carrying out network attacks. To combat these attacks, effective protection methods must also utilize artificial intelligence. Hence, we are introducing a specific neural network-based decision procedure that can be considered for application in any flow characteristic-based network-traffic-handling controller. This decision procedure is based on a convolutional neural network that processes the incoming flow characteristics and provides a decision; the procedure can be understood as a firewall rule. The main advantage of this decision procedure is its depiction process, which has the ability to transform the incoming flow characteristics into a graphical structure. Graphical structures are regarded as very efficient data structures for processing by convolutional neural networks. This article’s main contribution consists of the development and improvement of the depiction process using a genetic algorithm. The results presented at the end of the article show that the decision procedure using an optimized depiction process brings significant improvements in comparison to previous experiments.

Representation and application of Fuzzy soft sets in type-2 environment

This paper has represented a soft-set in the type-2 environment by its simplest form as an augmentation to soft-set theories. Furthermore, we have applied the type-2 fuzzy soft set(T2FSS) by using our most straightforward representation to find the solution of a decision-making-problem (DMP) based-on T2FSS as well as weighted type-2 fuzzy soft set (WT2FSS). We have proposed two definitions, namely, Mid-$$\alpha $$ α -threshold fuzzy-set of a T2FSS and Mid-$$\lambda $$ λ -threshold fuzzy-set of a T2FSS. Furthermore, we have presented the definition, namely, level fuzzy-soft-set(LFSS) of a T2FSS. Using this concept, we have prepared two algorithms to select one object in T2FSS as well as WT2FSS based on DMP, which take regret disinclination and expectation preference of decision-makers into consideration in the decision procedure. Also, we have presented two numerical examples at the end.

Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity

Sentential Calculus with Identity ($$\mathsf {SCI}$$ SCI ) is an extension of classical propositional logic, featuring a new connective of identity between formulas. In $$\mathsf {SCI}$$ SCI two formulas are said to be identical if they share the same denotation. In the semantics of the logic, truth values are distinguished from denotations, hence the identity connective is strictly stronger than classical equivalence. In this paper we present a sound, complete, and terminating algorithm deciding the satisfiability of $$\mathsf {SCI}$$ SCI -formulas, based on labelled tableaux. To the best of our knowledge, it is the first implemented decision procedure for $$\mathsf {SCI}$$ SCI which runs in NP, i.e., is complexity-optimal. The obtained complexity bound is a result of dividing derivation rules in the algorithm into two sets: decomposition and equality rules, whose interplay yields derivation trees with branches of polynomial length with respect to the size of the investigated formula. We describe an implementation of the procedure and compare its performance with implementations of other calculi for $$\mathsf {SCI}$$ SCI (for which, however, the termination results were not established). We show possible refinements of our algorithm and discuss the possibility of extending it to other non-Fregean logics.