Chile’s experience with its Constitutional Convention from 2021 to 2022 sheds light on an important issue for comparative reflection: the role of procedures in constitution-making processes. The Constitutional Convention was bound by procedures that were both externally imposed and internally created. Our assessment is that, while some procedures improved representation and deliberation, the most important decision-making procedures were pernicious to the process. We argue that looking at procedures is fundamental when analysing constitutional processes, as the rules that bind rule-making processes can significantly impact not only their functioning, but also their outcomes.

This paper presents backstepping control and backstepping constraint control approaches for a quadrotor unmanned aerial vehicle (UAV) control system. The proposed methods are applied to a Parrot Mambo drone model to control rotational motion along the $x$, $y$, and $z$ axes during hovering and trajectory tracking. In the backstepping control approach, each state of the system controls the previous state and is called “virtual control.” The last state is controlled by the real control input. The idea is to compute, in several steps, a control law that ensures the asymptotic stability of the system. The backstepping constraint control method, based on barrier Lyapunov functions (BLFs), is designed not only to track the desired trajectory but also to guarantee no violation of the position and angle constraints. Symmetric BLFs are introduced in the design of the controller. A nonlinear mathematical model is considered in this study. Based on Lyapunov stability theory, it can be concluded that the proposed controllers can guarantee the stability of the UAV system and the state converges asymptotically to the desired trajectory. To make the control robust, an adaptation law is applied to the backstepping control that estimates the unknown parameters and ensures their convergence to their respective values. Validation of the proposed controllers was performed by simulation on a flying UAV system.

The World Organisation for Animal Health (OIE) policy definition that “animal welfare is a complex international public policy issue with scientific, ethical, economic, cultural and religious dimensions, plus important trade policy considerations” clearly demonstrates the multi-faceted nature of animal welfare. Progress made is inevitably incremental and compromises often have to be reached between animal welfare and other important societal values. Recognition of the need for managed change over agreed time-frames, and involving full consultation with affected animal user groups, is essential. This paper draws on case studies involving intensive livestock agriculture, live animal exports for slaughter, religious slaughter and vertebrate pest control in both New Zealand's domestic experience, gained over the last 20 years, and international (OIE) experience, gained over the last ten years. Case studies will also highlight policy considerations relating to animal health, food safety and the impact on the environment. Important drivers of animal welfare change will be discussed; as will the constraints to making changes. The paper will conclude by commenting on the direction, and rate, of animal welfare change and the impact of animal welfare being addressed, not only at the national and regional level, but now also at the international level.

We address the problem of verifying that the functions of a program meet their contracts, specified by pre/postconditions. We follow an approach based on constrained Horn clauses (CHCs) by which the verification problem is reduced to the problem of checking satisfiability of a set of clauses derived from the given program and contracts. We consider programs that manipulate algebraic data types (ADTs) and a class of contracts specified by catamorphisms, that is, functions defined by simple recursion schemata on the given ADTs. We show by several examples that state-of-the-art CHC satisfiability tools are not effective at solving the satisfiability problems obtained by direct translation of the contracts into CHCs. To overcome this difficulty, we propose a transformation technique that removes the ADT terms from CHCs and derives new sets of clauses that work on basic sorts only, such as integers and booleans. Thus, when using the derived CHCs there is no need for induction rules on ADTs. We prove that the transformation is sound, that is, if the derived set of CHCs is satisfiable, then so is the original set. We also prove that the transformation always terminates for the class of contracts specified by catamorphisms. Finally, we present the experimental results obtained by an implementation of our technique when verifying many non-trivial contracts for ADT manipulating programs.

We propose answer-set programs that specify and compute counterfactual interventions on entities that are input on a classification model. In relation to the outcome of the model, the resulting counterfactual entities serve as a basis for the definition and computation of causality-based explanation scores for the feature values in the entity under classification, namely responsibility scores. The approach and the programs can be applied with black-box models, and also with models that can be specified as logic programs, such as rule-based classifiers. The main focus of this study is on the specification and computation of best counterfactual entities, that is, those that lead to maximum responsibility scores. From them one can read off the explanations as maximum responsibility feature values in the original entity. We also extend the programs to bring into the picture semantic or domain knowledge. We show how the approach could be extended by means of probabilistic methods, and how the underlying probability distributions could be modified through the use of constraints. Several examples of programs written in the syntax of the DLV ASP-solver, and run with it, are shown.

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. CASP demonstrates promising results, including the development of a multitude of solvers: acsolver, clingcon, ezcsp, idp, inca, dingo, mingo, aspmt2smt, 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 Traveling 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.

Automated commonsense reasoning (CR) is essential for building human-like AI systems featuring, for example, explainable AI. Event calculus (EC) is a family of formalisms that model CR with a sound, logical basis. Previous attempts to mechanize reasoning using EC faced difficulties in the treatment of the continuous change in dense domains (e.g. time and other physical quantities), constraints among variables, default negation, and the uniform application of different inference methods, among others. We propose the use of s(CASP), a query-driven, top-down execution model for Predicate Answer Set Programming with Constraints, to model and reason using EC. We show how EC scenarios can be naturally and directly encoded in s(CASP) and how it enables deductive and abductive reasoning tasks in domains featuring constraints involving both dense time and dense fluents.

Coalition governments prevail at the European subnational level. Although some studies explain the formation of subnational government coalitions, we know little about the determinants of individual parties' likelihood of joining such coalitions. This article aims to fill this gap in empirical and theoretical ways. It shows that an important institutional constraint matters for political actors' strategies when forming subnational coalitions: the party affiliation of the directly elected head of the executive. Being the party of the head of the executive or being ideologically close to that party significantly increases a party's likelihood of joining a coalition. The empirical evidence results from multinomial choice models using a novel data set on subnational parties' likelihood of joining 92 coalition governments at the local level in Germany between 1999 and 2016. The findings have substantive implications for subnational institutional settings resembling ‘mixed’ political systems (i.e. neither purely presidential nor purely parliamentarian).

Probabilistic logic programming is an effective formalism for encoding problems characterized by uncertainty. Some of these problems may require the optimization of probability values subject to constraints among probability distributions of random variables. Here, we introduce a new class of probabilistic logic programs, namely probabilistic optimizable logic programs, and we provide an effective algorithm to find the best assignment to probabilities of random variables, such that a set of constraints is satisfied and an objective function is optimized.