by Lam, Hin-ki Isaac. / Thesis (M.Phil.)--Chinese University of Hong Kong, 1992. / Includes bibliographical references (leaves 219-220). / Chapter Chapter 1 --- Introduction --- p.1 / Chapter 1.1 --- The Problem --- p.1 / Chapter 1.2 --- Related Works --- p.3 / Chapter 1.3 --- Contribution of the Present Study --- p.8 / Chapter 1.4 --- Outline of the Thesis --- p.8 / Chapter Chapter 2 --- Nontermination and Recursive Definition --- p.11 / Chapter 2.1 --- Prolog Execution Model --- p.11 / Chapter 2.2 --- Nontermination --- p.15 / Chapter 2.3 --- Exit Condition --- p.21 / Chapter 2.4 --- Exit-Reaching Process --- p.29 / Chapter 2.5 --- Parameter Based Detection --- p.35 / Chapter Chapter 3 --- Parameter Analysis --- p.38 / Chapter 3.1 --- Parameter Links --- p.39 / Chapter 3.1.1 --- Parameter Links and Parameter Modifying Process --- p.39 / Chapter 3.1.2 --- Parameter Links of Multi-Parameters --- p.43 / Chapter 3.1.3 --- Parameter Links in Indirect Recursive Definition --- p.44 / Chapter 3.1.4 --- Parameter Links with Special Parameters --- p.46 / Chapter 3.1.5 --- Parameter Links of the Same Name Parameters --- p.47 / Chapter 3.1.6 --- The Significance of Parameter Links --- p.49 / Chapter 3.2 --- Cyclic Parameter Links --- p.51 / Chapter 3.3 --- Parameter Link Detection --- p.58 / Chapter 3.3.1 --- Graph Technique --- p.58 / Chapter 3.3.1.1 --- Preliminaries --- p.58 / Chapter 3.3.1.2 --- on Parameter Links --- p.59 / Chapter 3.3.2 --- Algorithms --- p.62 / Chapter Chapter 4 --- Data Analysis --- p.70 / Chapter 4.1 --- Data Links --- p.72 / Chapter 4.1.1 --- The Direct Recursive Definition Case --- p.76 / Chapter 4.1.1.1 --- Subgoal Procedures with Facts Alone --- p.76 / Chapter 4.1.1.2 --- Procedures with Rules --- p.79 / Chapter 4.1.2 --- The Indirect Recursive Definition Case --- p.84 / Chapter 4.2 --- on the Difference between Pure and General Prolog --- p.86 / Chapter 4.3 --- Data Link Significance --- p.89 / Chapter 4.4 --- Connected Data-link Lists --- p.92 / Chapter 4.4.1 --- Data Links and Connected Data-link Lists --- p.92 / Chapter 4.4.1.1 --- Connected Data-link Lists and Data Transfer Sequence --- p.95 / Chapter 4.4.1.2 --- Connected Data-link Lists and Backtracking --- p.97 / Chapter 4.4.1.3 --- Connected Data-link Lists and the Recursion Result --- p.99 / Chapter 4.4.2 --- Cyclic and Non-Cyclic Connected Data-link Lists --- p.100 / Chapter 4.4.2.1 --- Non-Cyclic Connected Data-link Lists and Exit Conditions --- p.102 / Chapter 4.4.2.2 --- Cyclic Connected Data-link Lists and Nontermination --- p.104 / Chapter 4.4.3 --- Multi-Connected Data-link Lists --- p.107 / Chapter 4.4.3.1 --- in One Cyclic Parameter Link --- p.107 / Chapter 4.4.3.2 --- in Multi-Cyclic Parameter Links --- p.115 / Chapter 4.4.3.3 --- The Case of Multiple Recursive Subgoals in the Same Rule --- p.120 / Chapter 4.5. --- Special Parameters and Data Links --- p.125 / Chapter 4.5.1. --- Data Links with Special Parameters Only --- p.126 / Chapter 4.5.2 --- Data Links with Both Special Parameters and Subgoals --- p.136 / Chapter 4.6 --- Data Links and Infinite Data Transfer Sequence Detection --- p.142 / Chapter CHAPTER 5 --- Special Cases --- p.150 / Chapter 5.1 --- Interdependent Cyclic Parameter Links --- p.150 / Chapter 5.1.1 --- Interdependent Cyclic Parameter Links through Common Parameters --- p.151 / Chapter 5.1.1.1 --- Interdependency between Cyclic and Non-cyclic Parameter Links and Interdependency between Cyclic Parameter Link and Subgoals --- p.158 / Chapter 5.1.1.2 --- Interdependency between Cyclic Parameter Links --- p.165 / Chapter 5.1.1.2.1 --- Lengths of Cyclic Connected- data Links in Different Ratios --- p.171 / Chapter 5.1.1.2.2 --- Cyclic Parameter Links with Lengths in Different Ratios --- p.182 / Chapter 5.1.2 --- Interdependent Cyclic Parameter Links through Common Subgoals --- p.196 / Chapter 5.1.3 --- Interdependent Cyclic Parameter Links with Special Parameters --- p.202 / Chapter 5.2 --- A Special Case of Cyclic Parameter Links established through Special Parameters --- p.208 / Chapter CHAPTER 6 --- Discussion and Conclusion --- p.213 / Chapter 6.1 --- The Results and Implications --- p.213 / Chapter 6.2 --- Limitations and Future Research --- p.215 / Chapter 6.3 --- Conclusion --- p.217 / Reference --- p.219

Chiu, Yiu Man Edmund. / Thesis submitted in: December 1999. / Thesis (M.Phil.)--Chinese University of Hong Kong, 2000. / Includes bibliographical references (leaves 269-248). / Abstracts in English and Chinese. / Abstract --- p.i / Acknowledgments --- p.iii / Chapter 1 --- Introduction --- p.1 / Chapter 1.1 --- The Beginning Story --- p.2 / Chapter 1.2 --- Background --- p.3 / Chapter 1.2.1 --- History of Nonmonotonic Reasoning --- p.3 / Chapter 1.2.2 --- Formalizations of Nonmonotonic Reasoning --- p.6 / Chapter 1.2.3 --- Belief Revision --- p.13 / Chapter 1.2.4 --- Network Representation of Knowledge --- p.17 / Chapter 1.2.5 --- Reference from Logic Programming --- p.21 / Chapter 1.2.6 --- Recent Work on Network-type Automatic Reasoning Sys- tems --- p.22 / Chapter 1.3 --- A Novel Inference Network Approach --- p.23 / Chapter 1.4 --- Objectives --- p.23 / Chapter 1.5 --- Organization of the Thesis --- p.24 / Chapter 2 --- The Predicate Inference Network PIN --- p.25 / Chapter 2.1 --- Preliminary Terms --- p.26 / Chapter 2.2 --- Overall Structure --- p.27 / Chapter 2.3 --- Object Layer --- p.29 / Chapter 2.3.1 --- Virtual Object --- p.31 / Chapter 2.4 --- Predicate Layer --- p.33 / Chapter 2.4.1 --- Node Values --- p.34 / Chapter 2.4.2 --- Information Source --- p.35 / Chapter 2.4.3 --- Belief State --- p.36 / Chapter 2.4.4 --- Predicates --- p.37 / Chapter 2.4.5 --- Prototypical Predicates --- p.37 / Chapter 2.4.6 --- Multiple Inputs for a Single Belief --- p.39 / Chapter 2.4.7 --- External Program Call --- p.39 / Chapter 2.5 --- Variable Layer --- p.40 / Chapter 2.6 --- Inter-Layer Links --- p.42 / Chapter 2.7 --- Chapter Summary --- p.43 / Chapter 3 --- Computation for PIN --- p.44 / Chapter 3.1 --- Computation Functions for Propagation --- p.45 / Chapter 3.1.1 --- Computational Functions for Combinative Links --- p.45 / Chapter 3.1.2 --- Computational Functions for Alternative Links --- p.49 / Chapter 3.2 --- Applying the Computation Functions --- p.52 / Chapter 3.3 --- Relations Represented in PIN --- p.55 / Chapter 3.3.1 --- Relations Represented by Combinative Links --- p.56 / Chapter 3.3.2 --- Relations Represented by Alternative Links --- p.59 / Chapter 3.4 --- Chapter Summary --- p.61 / Chapter 4 --- Dynamic Knowledge Update --- p.62 / Chapter 4.1 --- Operations for Knowledge Update --- p.63 / Chapter 4.2 --- Logical Expression --- p.63 / Chapter 4.3 --- Applicability of Operators --- p.64 / Chapter 4.4 --- Add Operation --- p.65 / Chapter 4.4.1 --- Add a fully instantiated single predicate proposition with no virtual object --- p.66 / Chapter 4.4.2 --- Add a fully instantiated pure disjunction --- p.68 / Chapter 4.4.3 --- Add a fully instantiated expression which is a conjunction --- p.71 / Chapter 4.4.4 --- Add a human biased relation --- p.74 / Chapter 4.4.5 --- Add a single predicate expression with virtual objects --- p.76 / Chapter 4.4.6 --- Add a IF-THEN rule --- p.80 / Chapter 4.5 --- Remove Operation --- p.88 / Chapter 4.5.1 --- Remove a Belief --- p.88 / Chapter 4.5.2 --- Remove a Rule --- p.91 / Chapter 4.6 --- Revise Operation --- p.94 / Chapter 4.6.1 --- Revise a Belief --- p.94 / Chapter 4.6.2 --- Revise a Rule --- p.96 / Chapter 4.7 --- Consistency Maintenance --- p.97 / Chapter 4.7.1 --- Logical Suppression --- p.98 / Chapter 4.7.2 --- Example on Handling Inconsistent Information --- p.99 / Chapter 4.8 --- Chapter Summary --- p.102 / Chapter 5 --- Knowledge Query --- p.103 / Chapter 5.1 --- Domains of Quantification --- p.104 / Chapter 5.2 --- Reasoning through Recursive Rules --- p.109 / Chapter 5.2.1 --- Infinite Looping Control --- p.110 / Chapter 5.2.2 --- Proof of the finite termination of recursive rules --- p.111 / Chapter 5.3 --- Query Functions --- p.117 / Chapter 5.4 --- Type I Queries --- p.119 / Chapter 5.4.1 --- Querying a Simple Single Predicate Proposition (Type I) --- p.122 / Chapter 5.4.2 --- Querying a Belief with Logical Connective(s) (Type I) --- p.128 / Chapter 5.5 --- Type II Queries --- p.132 / Chapter 5.5.1 --- Querying Single Predicate Expressions (Type II) --- p.134 / Chapter 5.5.2 --- Querying an Expression with Logical Connectives (Type II) --- p.143 / Chapter 5.6 --- Querying an Expression with Virtual Objects --- p.152 / Chapter 5.6.1 --- Type I Queries Involving Virtual Object --- p.152 / Chapter 5.6.2 --- Type II Queries involving Virtual Objects --- p.156 / Chapter 5.7 --- Chapter Summary --- p.157 / Chapter 6 --- Uniqueness and Finite Termination --- p.159 / Chapter 6.1 --- Proof Structure --- p.160 / Chapter 6.2 --- Proof for Completeness and Finite Termination of Domain Search- ing Procedure --- p.161 / Chapter 6.3 --- Proofs for Type I Queries --- p.167 / Chapter 6.3.1 --- Proof for Single Predicate Expressions --- p.167 / Chapter 6.3.2 --- Proof of Type I Queries on Expressions with Logical Con- nectives --- p.172 / Chapter 6.3.3 --- General Proof for Type I Queries --- p.174 / Chapter 6.4 --- Proofs for Type II Queries --- p.175 / Chapter 6.4.1 --- Proof for Type II Queries on Single Predicate Expressions --- p.176 / Chapter 6.4.2 --- Proof for Type II Queries on Disjunctions --- p.178 / Chapter 6.4.3 --- Proof for Type II Queries on Conjunctions --- p.179 / Chapter 6.4.4 --- General Proof for Type II Queries --- p.181 / Chapter 6.5 --- Proof for Queries Involving Virtual Objects --- p.182 / Chapter 6.6 --- Uniqueness and Finite Termination of PIN Queries --- p.183 / Chapter 6.7 --- Chapter Summary --- p.184 / Chapter 7 --- Lifschitz's Benchmark Problems --- p.185 / Chapter 7.1 --- Structure --- p.186 / Chapter 7.2 --- Default Reasoning --- p.186 / Chapter 7.2.1 --- Basic Default Reasoning --- p.186 / Chapter 7.2.2 --- Default Reasoning with Irrelevant Information --- p.187 / Chapter 7.2.3 --- Default Reasoning with Several Defaults --- p.188 / Chapter 7.2.4 --- Default Reasoning with a Disabled Default --- p.190 / Chapter 7.2.5 --- Default Reasoning in Open Domain --- p.191 / Chapter 7.2.6 --- Reasoning about Unknown Exceptions I --- p.193 / Chapter 7.2.7 --- Reasoning about Unknown Exceptions II --- p.194 / Chapter 7.2.8 --- Reasoning about Unknown Exceptions III --- p.196 / Chapter 7.2.9 --- Priorities between Defaults --- p.198 / Chapter 7.2.10 --- Priorities between Instances of a Default --- p.199 / Chapter 7.2.11 --- Reasoning about Priorities --- p.199 / Chapter 7.3 --- Inheritance --- p.200 / Chapter 7.3.1 --- Linear Inheritance --- p.200 / Chapter 7.3.2 --- Tree-Structured Inheritance --- p.202 / Chapter 7.3.3 --- One-Step Multiple Inheritance --- p.203 / Chapter 7.3.4 --- Multiple Inheritance --- p.204 / Chapter 7.4 --- Uniqueness of Names --- p.205 / Chapter 7.4.1 --- Unique Names Hypothesis for Objects --- p.205 / Chapter 7.4.2 --- Unique Names Hypothesis for Functions --- p.206 / Chapter 7.5 --- Reasoning about Action --- p.206 / Chapter 7.6 --- Autoepistemic Reasoning --- p.206 / Chapter 7.6.1 --- Basic Autoepistemic Reasoning --- p.206 / Chapter 7.6.2 --- Autoepistemic Reasoning with Incomplete Information --- p.207 / Chapter 7.6.3 --- Autoepistemic Reasoning with Open Domain --- p.207 / Chapter 7.6.4 --- Autoepistemic Default Reasoning --- p.208 / Chapter 8 --- Comparison with PROLOG --- p.214 / Chapter 8.1 --- Introduction of PROLOG --- p.215 / Chapter 8.1.1 --- Brief History --- p.215 / Chapter 8.1.2 --- Structure and Inference --- p.215 / Chapter 8.1.3 --- Why Compare PIN with Prolog --- p.216 / Chapter 8.2 --- Representation Power --- p.216 / Chapter 8.2.1 --- Close World Assumption and Negation as Failure --- p.216 / Chapter 8.2.2 --- Horn Clauses --- p.217 / Chapter 8.2.3 --- Quantification --- p.218 / Chapter 8.2.4 --- Build-in Functions --- p.219 / Chapter 8.2.5 --- Other Representation Issues --- p.220 / Chapter 8.3 --- Inference and Query Processing --- p.220 / Chapter 8.3.1 --- Unification --- p.221 / Chapter 8.3.2 --- Resolution --- p.222 / Chapter 8.3.3 --- Computation Efficiency --- p.225 / Chapter 8.4 --- Knowledge Updating and Consistency Issues --- p.227 / Chapter 8.4.1 --- PIN and AGM Logic --- p.228 / Chapter 8.4.2 --- Knowledge Merging --- p.229 / Chapter 8.5 --- Chapter Summary --- p.229 / Chapter 9 --- Conclusion and Discussion --- p.230 / Chapter 9.1 --- Conclusion --- p.231 / Chapter 9.1.1 --- General Structure --- p.231 / Chapter 9.1.2 --- Representation Power --- p.231 / Chapter 9.1.3 --- Inference --- p.232 / Chapter 9.1.4 --- Dynamic Update and Consistency --- p.233 / Chapter 9.1.5 --- Soundness and Completeness Versus Efficiency --- p.233 / Chapter 9.2 --- Discussion --- p.234 / Chapter 9.2.1 --- Different Selection Criteria --- p.234 / Chapter 9.2.2 --- Link Order --- p.235 / Chapter 9.2.3 --- Inheritance Reasoning --- p.236 / Chapter 9.3 --- Future Work --- p.237 / Chapter 9.3.1 --- Implementation --- p.237 / Chapter 9.3.2 --- Application --- p.237 / Chapter 9.3.3 --- Probabilistic and Fuzzy PIN --- p.238 / Chapter 9.3.4 --- Temporal Reasoning --- p.238 / Bibliography --- p.239

Logic programming languages have generated increasing interest over the last few years. Logic programming languages like Prolog are being explored for different applications. Prolog is inherently parallel. Attempts are being made to utilize this inherent parallelism. There are two kinds of parallelism present in Prolog, OR parallelism and AND parallelism. OR parallelism is relatively easy to exploit while AND parallelism poses interesting issues. One of the main issues is dependencies between literals. It is very important to use the AND parallelism available in the language structure as not exploiting it would result in a substantial loss of parallelism. Any system trying to make use of either or both kinds of parallelism would need to have the capability of performing faster unification, as it affects the overall execution time greatly. A new architecture design is presented in this thesis that exploits both kinds of parallelism. The architecture efficiently implements some of the key concepts in Conery's approach to parallel execution [5]. The architecture has a memory hierarchy that uses associative memory. Associative memories are useful for faster lookup and response and hence their use results in quick response time. Along with the use of a memory hierarchy, execution algorithms and rules for ordering of literals are presented. The rules for ordering of literals are helpful in determining the order of execution. The analysis of response time is done for different configurations of the architecture, from sequential execution with one processor to multiple processing units having multiple processors. A benchmark program, "query," is used for obtaining results, and the map coloring problem is also solved on different configurations and results are compared. To obtain results the goals and subgoals are assigned to different processors by creating a tree. These assignments and transferring of goals are simulated by hand. The total time includes the time needed for moving goals back and forth from one processor to another. The total time is calculated in number of cycles with some assumptions about memory response time, communication time, number of messages that can be sent on the bus at a particular instant, etc. The results obtained show that the architecture efficiently exploits the AND parallelism and OR parallelism available in Prolog. The total time needed for different configurations is then compared and conclusions are drawn.

Modern software is often realized as a modular combination of subsystems for, e. g., knowledge management, visualization, verification, or the interaction with users. As a result, software libraries from possibly different programming languages have to work together. Even more complex the case is if different programming paradigms have to be combined. This type of diversification of programming languages and paradigms in just one software application can only be mastered by mechanisms for a seamless integration of the involved programming languages. However, the integration of the common logic programming language Prolog and the popular object-oriented programming language Java is complicated by various interoperability problems which stem on the one hand from the paradigmatic gap between the programming languages, and on the other hand, from the diversity of the available Prolog systems. The subject of the thesis is the investigation of novel mechanisms for the integration of logic programming in Prolog and object–oriented programming in Java. We are particularly interested in an object–oriented, uniform approach which is not specific to just one Prolog system. Therefore, we have first identified several important criteria for the seamless integration of Prolog and Java from the object–oriented perspective. The main contribution of the thesis is a novel integration framework called the Connector Architecture for Prolog and Java (CAPJa). The framework is completely implemented in Java and imposes no modifications to the Java Virtual Machine or Prolog. CAPJa provides a semi–automated mechanism for the integration of Prolog predicates into Java. For compact, readable, and object–oriented queries to Prolog, CAPJa exploits lambda expressions with conditional and relational operators in Java. The communication between Java and Prolog is based on a fully automated mapping of Java objects to Prolog terms, and vice versa. In Java, an extensible system of gateways provides connectivity with various Prolog system and, moreover, makes any connected Prolog system easily interchangeable, without major adaption in Java. / Moderne Software ist oft modular zusammengesetzt aus Subsystemen zur Wissensverwaltung, Visualisierung, Verfikation oder Benutzerinteraktion. Dabei müssen Programmbibliotheken aus möglicherweise verschiedenen Programmiersprachen miteinander zusammenarbeiten. Noch komplizierter ist der Fall, wenn auch noch verschiedene Programmierparadigmen miteinander kombiniert werden. Diese Art der Diversifikation an Programmiersprachen und –paradigmen in nur einer Software kann nur von nahtlosen Integrationsmechansimen für die beteiligten Programmiersprachen gemeistert werden. Gerade die Einbindung der gängigen Logikprogrammiersprache Prolog und der populären objektorientierten Programmiersprache Java wird durch zahlreiche Kompatibilitätsprobleme erschwert, welche auf der einen Seite von paradigmatischen Unterschieden der beiden Programmiersprachen herrühren und auf der anderen Seite von der Vielfalt der erhältlichen Prologimplementierungen. Gegenstand dieser Arbeit ist die Untersuchung von neuartigen Mechanismen für die Zusammenführung von Logikprogrammierung in Prolog und objektorienter Programmierung in Java. Besonders interessiert uns dabei ein objektorientierter, einheitlicher Ansatz, der nicht auf eine konkrete Prologimplementierung festgelegt ist. Aus diesem Grund haben wir zunächst wichtige Kriterien für die nahtlose Integration von Prolog und Java aus der objetorientierten Sicht identifziert. Der Hauptbeitrag dieser Arbeit ist ein neuartiges Integrationssystems, welches Connector Architecture for Prolog and Java (CAPJa) heißt. Das System ist komplett in Java implementiert und benötigt keine Anpassungen der Java Virtual Machine oder Prolog. CAPJa stellt einen halbautomatischen Mechanismus zur Vernetzung von Prolog Prädikaten mit Java zur Verfügung. Für kompakte, lesbare und objektorientierte Anfragen an Prolog nutzt CAPJa Lambdaausdrücke mit logischen und relationalen Operatoren in Java. Die Kommunikation zwischen Java und Prolog basiert auf einer automatisierten Abbildung von Java Objekten auf Prolog Terme, und umgekehrt. In Java bietet ein erweiterbares System von Schnittstellen Konnektivität zu einer Vielzahl an Prologimplmentierung und macht darüber hinaus jede verbundene Prologimplementierung einfach austauschbar, und zwar ohne größere Anpassung in Java.

Cette thèse est consacrée a l'étude de l'implantation du langage Prolog sur les architectures parallèles Mimd sans mémoire commune. Nous présentons le modèle opéra qui exploite implicitement le parallélisme ou le Prolog pour repartir dynamiquement l'évaluation des programmes sur les différents nœuds du réseau de processeurs. Le système opéra est de type multisequentiel: il n'y a parallélisation que lorsqu'un processeur est inoccupé. Ce système se décompose en une partie operative chargée de l'évaluation du programme Prolog, et une partie contrôle chargée de l'allocation des travaux aux processeurs de la partie operative. Les principaux problèmes de ce type de systèmes sont d'une part le choix de représentation en mémoire de l'arbre ou ainsi que la gestion des liaisons multiples, et d'autre part, le contrôle de l'allocation des différentes branches de l'arbre aux machines abstraites qui effectuent des évaluations séquentielles. La technique de régulation de charge utilisée est fondée sur des méthodes heuristiques. L'ordonnanceur d'opera travaille sur une image approchée de l'état global du système obtenu par échantillonnage des états locaux de chaque unités de travail. Un prototype d'opera a été réalisé sur un réseau de transputers reconfigurable dynamiquement: le supernode. Cette propriété a ete mise a profit dans notre implantation pour réduire les couts de communication. Les communications sont effectuées en parallèle avec le calcul. Le prototype réalisé fournit des gains de performances importants et opera figure parmi les systèmes Prolog parallèles les plus efficaces a l'heure actuelle

L'objectif de cette thèse est la conception d'une implantation parallèle efficace de Prolog. Sur une machine sans mémoire commune. Le modèle de calcul exploite le parallélisme ou selon l'approche multisequentielle classique. La partie principale de cette thèse est l'étude de méthodes de partage de contexte entre plusieurs machines abstraites Prolog. Un prototype est présent et des résultats préliminaires décrits. Ce prototype délivre un accroissement de performance effectif par parallélisation par rapport a des systèmes séquentiels

Contribution à l'approche inferentielle pour l'introduction de la notion de type en Prolog. Cette approche consiste à déduire automatiquement d'un programme les types des prédicats. Le programmeur peut ainsi s'assurer de la conformité du programme à ses intentions. Une méthode d'inférence de type pour Prolog est présentée. Elle se base sur une simulation de l'unification et une simulation de la résolution, avec un traitement particulier sur les appels récursifs

.

Cette étude met en évidence l'utilité des modes directionnels pour l'optimisation de la résolution dans le langage Prolog. Ils se caractérisent essentiellement par le fait qu'ils permettent de distinguer les différentes utilisations possibles d'un même prédicat. Un algorithme de production automatique de ces modes est décrit. L'étude est concrétisée par la réalisation du compilateur Starlog, fonctionnant sur un cas particulier de modes directionnels

Description d'un outil d'aide à la conception et à la vérification de systèmes communicants qui est basé sur le calcul CCS de Milner.