Automated planning as a satisfiability problem is a method developed in theearly nineties. It has some known disadvantages, such as its inefficient encod-ing of numbers. The field of Satisfiability Modulo Teories tries to connectalready established solvers for e.g. linear constraints into SAT-solvers in orderto make reasoning about numerical values more efficient. This thesis combines planning as satisfiability and SMT to perform efficientreasoning about actions that occupy realistic time in Temporal Action Logic,a formalism developed at Linköping University for reasoning about action andchange.

The thesis aims at developing approaches to transport policy decisions, based on suggestions and ideas originating from moral philosophy and philosophical decision theory.Paper I analyzes the Swedish transport policy goals, and the problem of combining policygoals with welfare economics. A problem of circularity arises as the Swedish transport policygoals are conflicting, and hence must be subject to trade-offs, while several of the goals themselves entail statements on how to prioritize or restrain goals in case of conflict.Paper II analyzes rationality in road safety policy. Problematic features are identified and discussed. The paper argues that the Swedish road safety goal is rational, since it is actionguiding and achievement-inducing.Paper III includes a model of rational choice under risk with biased risk perception. Under certain plausible conditions, a regulator should raise the population’s risk exposure. By deteriorating the environment the regulator can motivate drivers to choose behaviour that is less biased.Paper IV provides a formal representation of goal systems. The focus is on three properties:consistency, conflict, and coherence. It is argued that consistency is adequately regarded as a property relative to the decision situation or, more specifically, the set of alternatives that the agent faces. Conflict is adequately regarded as a relation over subsets of a given goal systemand should likewise be regarded as relative to the set of alternative that the agent faces.Coherence is given a probabilistic interpretation, based on a support relation over subsets of goal systems.Paper V investigates problems associated with standard deontic logic. A deontic predicate is derived, which avoids some of the major paradoxes in the area. In particular, paradoxes occurring when one obligation is derived by logical necessity from another obligation are dealt with. / QC 20100806

Temporal Action Logic is a well established logical formalism for reasoning about action and change that has long been used as a formal specification language. Its first-order characterization and explicit time representation makes it a suitable target for automated theorem proving and the application of temporal constraint solvers. We introduce a translation from a subset of Temporal Action Logic to constraint logic programs that takes advantage of these characteristics to make the logic applicable, not just as a formal specification language, but in solving practical reasoning problems. Extensions are introduced that enable the generation of action sequences, thus paving the road for interesting applications in deductive planning. The use of qualitative temporal constraints makes it possible to follow a least commitment strategy and construct partially ordered plans. Furthermore, the logical language and logic program translation is extended with the notion of composite actions that can be used to formulate and execute scripted plans with conditional actions, non-deterministic choices, and loops. The resulting planner and reasoner is integrated with a graphical user interface in our autonomous helicopter research system and applied to logistics problems. Solution plans are synthesized together with monitoring constraints that trigger the generation of recovery actions in cases of execution failures.

<p>Temporal Action Logic is a well established logical formalism for reasoning about action and change that has long been used as a formal specification language. Its first-order characterization and explicit time representation makes it a suitable target for automated theorem proving and the application of temporal constraint solvers. We introduce a translation from a subset of Temporal Action Logic to constraint logic programs that takes advantage of these characteristics to make the logic applicable, not just as a formal specification language, but in solving practical reasoning problems. Extensions are introduced that enable the generation of action sequences, thus paving the road for interesting applications in deductive planning. The use of qualitative temporal constraints makes it possible to follow a least commitment strategy and construct partially ordered plans. Furthermore, the logical language and logic program translation is extended with the notion of composite actions that can be used to formulate and execute scripted plans with conditional actions, non-deterministic choices, and loops. The resulting planner and reasoner is integrated with a graphical user interface in our autonomous helicopter research system and applied to logistics problems. Solution plans are synthesized together with monitoring constraints that trigger the generation of recovery actions in cases of execution failures.</p>

Thèse numérisée par la Division de la gestion de documents et des archives de l'Université de Montréal.

Even if strategy research often assumes that strategies are the result of intentional and purposeful behaviour the individual and human agency have tended to be neglected. Few empirical studies focus on how the individuals, their conceptions and actions interact with strategy formation. Based on ideas from process research and critical realism we made a review of the research and we maintain that the bulk of the research is based on simplified assumptions. We therefore propose a supplementary socio-cognitive approach based on more realistic assumptions, a synthesis and action logic approach, emphasising the individuals, the leading team and their embeddedness. In a process study with a comparative case study design we followed, in real time for about a decade, strategy formation processes in intermediate organisation in local economic development. Various methods of data collection and analysis were combined. By laying bare some of the mechanisms that explain the outcome in four processes we demonstrate the use of the proposed approach. A theoretical construction, the agent´s strategic concepts of action (SCA), aims at capturing the conceptions as an expression of the individual frame of reference providing reasons for action. The SCA carries explanatory power and is significant for both the process and content of the strategies. A typology of the SCAs is developed. The composition, the interaction and the structure of the team are other central aspects. We conclude that a strong group well suited to lead a formation process include a proactive strategist with a strategic idea and social capability; the role constellation is differentiated, and supplementary and other strategic actors relate to the strategy and the contextual roots in a way that will support the strategy. We also demonstrate in which circumstances some cognitive, social and political mechanisms discussed in earlier research are activated.

Thèse numérisée par la Division de la gestion de documents et des archives de l'Université de Montréal

No description available.

Thèse par articles. / La présente thèse fait état des avancées en logique déontique et propose des outils formels pertinents à l'analyse de la validité des inférences légales. D'emblée, la logique vise l'abstraction de différentes structures. Lorsqu'appliquée en argumentation, la logique permet de déterminer les conditions de validité des inférences, fournissant ainsi un critère afin de distinguer entre les bons et les mauvais raisonnements. Comme le montre la multitude de paradoxes en logique déontique, la modélisation des inférences normatives fait cependant face à divers problèmes. D'un point de vue historique, ces difficultés ont donné lieu à différents courants au sein de la littérature, dont les plus importants à ce jour sont ceux qui traitent de l'action et ceux qui visent la modélisation des obligations conditionnelles. La présente thèse de doctorat, qui a été rédigée par articles, vise le développement d'outils formels pertinents à l'analyse du discours juridique. En première partie, nous proposons une revue de la littérature complémentaire à ce qui a été entamé dans Peterson (2011). La seconde partie comprend la contribution théorique proposée. Dans un premier temps, il s'agit d'introduire une logique déontique alternative au système standard. Sans prétendre aller au-delà de ses limites, le système standard de logique déontique possède plusieurs lacunes. La première contribution de cette thèse est d'offrir un système comparable répondant au différentes objections pouvant être formulées contre ce dernier. Cela fait l'objet de deux articles, dont le premier introduit le formalisme nécessaire et le second vulgarise les résultats et les adapte aux fins de l'étude des raisonnements normatifs. En second lieu, les différents problèmes auxquels la logique déontique fait face sont abordés selon la perspective de la théorie des catégories. En analysant la syntaxe des différents systèmes à l'aide des catégories monoïdales, il est possible de lier certains de ces problèmes avec des propriétés structurelles spécifiques des logiques utilisées. Ainsi, une lecture catégorique de la logique déontique permet de motiver l'introduction d'une nouvelle approche syntaxique, définie dans le cadre des catégories monoïdales, de façon à pallier les problèmes relatifs à la modélisation des inférences normatives. En plus de proposer une analyse des différentes logiques de l'action selon la théorie des catégories, la présente thèse étudie les problèmes relatifs aux inférences normatives conditionnelles et propose un système déductif typé. / The present thesis develops formal tools relevant to the analysis of legal discourse. When applied to legal reasoning, logic can be used to model the structure of legal inferences and, as such, it provides a criterion to discriminate between good and bad reasonings. But using logic to model normative reasoning comes with some problems, as shown by the various paradoxes one finds within the literature. From a historical point of view, these paradoxes lead to the introduction of different approaches, such as the ones that emphasize the notion of action and those that try to model conditional normative reasoning. In the first part of this thesis, we provide a review of the literature, which is complementary to the one we did in Peterson (2011). The second part of the thesis concerns our theoretical contribution. First, we propose a monadic deontic logic as an alternative to the standard system, answering many objections that can be made against it. This system is then adapted to model unconditional normative inferences and test their validity. Second, we propose to look at deontic logic from the proof-theoretical perspective of category theory. We begin by proposing a categorical analysis of action logics and then we show that many problems that arise when trying to model conditional normative reasoning come from the structural properties of the logic we use. As such, we show that modeling normative reasoning within the framework of monoidal categories enables us to answer many objections in favour of dyadic and non-monotonic foundations for deontic logic. Finally, we propose a proper typed deontic system to model legal inferences.