Luo Z.,Royal Holloway, University of London |
Soloviev S.,IRIT |
Xue T.,Royal Holloway, University of London
Information and Computation | Year: 2013
Coercive subtyping is a useful and powerful framework of subtyping for type theories. The key idea of coercive subtyping is subtyping as abbreviation. In this paper, we give a new and adequate formulation of T [C], the system that extends a type theory T with coercive subtyping based on a set C of basic subtyping judgements, and show that coercive subtyping is a conservative extension and, in a more general sense, a definitional extension. We introduce an intermediate system, the star-calculus T [C]., in which the positions that require coercion insertions are marked, and show that T [C]. is a conservative extension of T and that T [C]. is equivalent to T [C]. This makes clear what we mean by coercive subtyping being a conservative extension, on the one hand, and amends a technical problem that has led to a gap in the earlier conservativity proof, on the other. We also compare coercive subtyping with the ′ordinary′ notion of subtyping-subsumptive subtyping, and show that the former is adequate for type theories with canonical objects while the latter is not. An improved implementation of coercive subtyping is done in the proof assistant Plastic. © 2012 Elsevier Inc. All rights reserved.
Ait-Ameur Y.,IRIT |
Mery D.,University of Lorraine
Science of Computer Programming | Year: 2016
Modeling languages are concerned with providing techniques and tool support for the design, synthesis and analysis of the models resulting from a given modeling activity, this activity being usually part of a system development model or process. These languages quite successfully focused on the analysis of the designed system exploiting the expressed semantic power of the underlying modeling language. The semantics of these modeling languages are well understood by the system designers and/or the modeling language users i.e. implicit semantics. In general, modeling languages are not equipped with resources, concepts or entities handling explicitly domain engineering features and characteristics (domain knowledge) in which the modeled systems evolve. Indeed, the designer has to explicitly handle the knowledge issued and/or mined from an analysis of this application domain i.e. explicit semantics. Nowadays, making explicit the domain knowledge inside system design models does not obey to any methodological rule validated by the practice. The modeling languages users introduce through types, constraints, profiles, etc. these domain knowledge features. Our claim is that ontologies are good candidates for handling explicit domain knowledge. They define domain theories and provide resources for uniquely identifying domain knowledge concepts. Therefore, allowing models to make references to ontologies is a modular solution for models to explicitly handle domain knowledge. Overcoming the absence of explicit semantics expression in the modeling languages used to specify systems models will increase the robustness of the designed system models. Indeed, the axioms and theorems resulting from the ontologies, thanks to references, can be used to strengthen the properties of the designed models. The objective of this paper is to offer rigorous mechanisms for handling domain knowledge in design models. This paper also shows how these mechanisms are set up in the cases of static, dynamic and formal models. © 2015 Elsevier B.V.
De Saint-Cyr F.D.,IRIT
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Year: 2011
This paper is a first attempt to define a framework to handle enthymeme in a time-limited persuasion dialog. The notion of incomplete argument is explicited and a protocol is proposed to regulate the utterances of a persuasion dialog with respect to the three criteria of consistency, non-redundancy and listening. This protocol allows the use of enthymemes concerning the support or conclusion of the argument, enables the agent to retract or re-specify an argument. The system is illustrated on a small example and some of its properties are outlined. © 2011 Springer-Verlag.
Fargier H.,IRIT |
Rollon E.,University of Barcelona
Constraints | Year: 2010
Many computational problems linked to uncertainty and preference management can be expressed in terms of computing the marginal(s) of a combination of a collection of valuation functions. Shenoy and Shafer showed how such a computation can be performed using a local computation scheme. A major strength of this work is that it is based on an algebraic description: what is proved is the correctness of the local computation algorithm under a few axioms on the algebraic structure. The instantiations of the framework in practice make use of totally ordered scales. The present paper focuses on the use of partially ordered scales and examines how such scales can be cast in the Shafer-Shenoy framework and thus benefit from local computation algorithms. It also provides several examples of such scales, thus showing that each of the algebraic structures explored here is of interest. © 2010 Springer Science+Business Media, LLC.
Herzig A.,French National Center for Scientific Research |
Lorini E.,French National Center for Scientific Research |
Moisan F.,IRIT |
Troquard N.,University of Essex
IJCAI International Joint Conference on Artificial Intelligence | Year: 2011
We propose a logical framework to represent and reason about agent interactions in normative systems. Our starting point is a dynamic logic of propositional assignments whose satisfiability problem is PSPACE-complete. We show that it embeds Coalition Logic of Propositional Control CL-PC and that various notions of ability and capability can be captured in it. We illustrate it on a water resource management case study. Finally, we show how the logic can be easily extended in order to represent constitutive rules which are also an essential component of the modelling of social reality.