{* # This file is governed by the Creative Commons license # Attribution-NonCommercial 4.0 Unported # http://creativecommons.org/licenses/by-nc/4.0/ # http://creativecommons.org/licenses/by-nc/4.0/legalcode # # Extended licenses, in particular commercial licenses, can be obtained from the # author of the source code. # Any re-distribution as source code must acknowledge the original author of this file. # # File: deeptelos_r1.sml.txt # Author: Manfred Jeusfeld, manfred.jeusfeld@acm.org # Date: 2016-03-03 (2018-11-28) #---------------------------------------------------------------- # Formalization of DeepTelos # # Revision R1: Handle the case that the most general instance m already has subclasses (x isA m) # Then, we inherit the instantiation to the class c in (m IN c) rather than the specialization (x ISA m) # See mrule1 and mrule4. *} Proposition with attribute ISA: Proposition; {* shall have same semantics as Telos-ISA *} IN: Proposition {* relates a power type to its meta class; not identical to Telos-IN *} end DeepTelosRules in Class with rule mrule1: $ forall m,x,c/Proposition (x in c) and (m IN c) and not (x isA m) ==> (x ISA m) $; mrule2: $ forall x,c,d/Proposition (c ISA d) and (x in c) ==> (x in d) $; mrule3: $ forall c,d,m,n/Proposition (m IN c) and (n IN d) and (c ISA d) ==> (m ISA n) $; mrule4: $ forall m,x,c/Proposition (m IN c) and (x isA m) ==> (x in c) $ end