Maker DAO examples stub added to deontic logic experiments

deontic_logic/ct_dts.metta

@@ -57,5 +57,24 @@
 (: and1 Eventuality)
 (: and2 Eventuality)
 
+(= (NOT_EXIST_stb $x)
+ (if (== $x (match &self $x $x)) True False)
+)
+
+(= (FILTER_stb $p $set $x)
+    (match &self
+    (, ($p $set $x)
+       ($p aint-my-set $x))
+    $x)
+)
+
+(= (CONSTRUCT_stb $x $y)
+   (add-atom &self (match &self $x $y))
+)
+
+;Inference rules at the 1st level (the level of the eventualities)
+
+;“not(en, e)” states that en and e are opposite eventualities; e.g., if e refers
+;to the fact that “John leaves”, en may refer to the fact that “John does not
+;leave”.
 
-!(match )

deontic_logic/functional_examples/README.md

@@ -0,0 +1,3 @@
+# Overview
+
+This folder contains some trivial examples on reasoning in deontic logic style with a simple functional implementation of inference.

deontic_logic/functional_examples/infer2.metta

@@ -0,0 +1,64 @@
+(:-- True True)
+
+; a way to stop evaluation of what is wrapped in TV
+(: TV (-> Atom Atom))
+(= (infer-step (TV $x))
+   (match &self (:-- $x $y) (TV $y)))
+; it could possibly be improved:
+; it's enough for one of operands to be False (while the second can be empty)
+(= (infer (AND $x $y))
+   (and (infer $x)
+        (infer $y))
+
+(= (infer (OR $x $y))
+   (or (infer $x)
+        (infer $y))
+
+)
+(= (infer (NOT-TRUE $x))
+   ; could it be done without case?
+   (case (infer $x) ; a way to capture empty (unknown) results
+     ((True False)
+      ($_ True)))
+)
+
+(= (infer $x)
+   (case (infer-step (TV $x)) (
+      ((TV True) True)
+      ((TV False) False)
+      ((TV $y) (infer $y))
+    )
+   )
+)
+
+(= (infer $x)
+   (case (infer-step (TV $x)) (
+      ((TV True) True)
+      ((TV False) False)
+      ((TV $y) (infer $y))
+    )
+   )
+)
+
+;a. PE(p)⊢ ¬OB(¬p), via Modus Ponens.
+;b. ¬OB(¬p)⊢ PE(p), via Modus Ponens.
+;c. OB(¬p)⊢ ¬PE(p), via Modus Tollens.
+;d. ¬PE(p)⊢ OB(¬p), via Modus Tollens.
+
+(:-- (pe &p) (NOT-TRUE (ob (NOT-TRUE &p))))
+
+;it is impermissible that (IM)
+
+(:-- (im &p) (ob (NOT-TRUE &p)))
+
+;it is omissible that (OM)
+
+(:-- (om &p) (NOT-TRUE (ob &p)))
+
+;it is optional that (OP)
+
+:-- (op &p) (AND (om &p) (pe &p)))
+
+;it is non-optional that (NO)
+
+(:-- (no &p) (OR (ob &p) (im &p)))

deontic_logic/infer.metta

@@ -26,6 +26,11 @@
    )
 )
 
+;(Normally) there must be no fence
+;But if you do put a fence, it must be white
+;By the sea, you can put a fence
+;You decide to put a fence
+
 (:-- (Fence fence-001) True)
 (:-- (Fence fence-002) True)
 

deontic_logic/maker_atlas_examples/README.md

@@ -0,0 +1,6 @@
+# Overview
+
+This folder contains attampts to map Maker Atlas regulatory documentation to a MeTTa atomspace knowledge base.
+
+[not_exist.metta](not_exist.metta) is a stub script with direct mapping of [DeonticTraditionalScheme](https://github.com/liviorobaldo/conflict-tolerantDeonticTraditionalScheme)
+repo to the MeTTa language

deontic_logic/maker_atlas_examples/ctDTS.metta

@@ -0,0 +1,137 @@
+;#------------------------------------------------------------------------------------------------------------------------------------------------
+;# Inference rules
+;#
+;# :InferenceRule is a special class that contains the SPARQL rules in the form CONSTRUCT-WHERE to execute. Each individual of this
+;# class is associated through the property has-sparql-code with a xsd:string that executes it. The automated reasoner first collects
+;# all individuals of the class :InferenceRule; then, it iteratively re-execute the SPARQL rules in the range of :has-sparql-code
+;# until no new individual is inferred.
+;#------------------------------------------------------------------------------------------------------------------------------------------------
+;
+;:InferenceRule rdf:type rdfs:Class.
+;:has-sparql-code rdf:type rdf:Property;
+;	rdfs:domain :InferenceRule;
+;	rdfs:range xsd:string.
+
+;#------------------------------------------------------------------------------------------------------------------------------------------------
+;# 1st-level classes and properties (Hobbs's logic) - eventualities, modalities, and thematic roles
+
+
+;#Rexist modality:
+;:Rexist rdf:type rdfs:Class,:Modality.
+
+(= (not_exist pattern)
+    !(unify &self (pattern) T F))
+
+(rexist class modality)
+
+;#Top classes:
+;:Eventuality rdf:type rdfs:Class.
+;:Modality rdf:type rdfs:Class.
+;:ThematicRole rdf:type rdfs:Class.
+
+(eventuality class type)
+(modality class type)
+(thematic_role class type)
+
+;#negation, conjunction, and disjunction of eventualities:
+;:not rdf:type rdf:Property; rdfs:domain :Eventuality; rdfs:range :Eventuality.
+;:and1 rdf:type rdf:Property; rdfs:domain :Eventuality; rdfs:range :Eventuality.
+;:and2 rdf:type rdf:Property; rdfs:domain :Eventuality; rdfs:range :Eventuality.
+;:or1 rdf:type rdf:Property; rdfs:domain :Eventuality; rdfs:range :Eventuality.
+;:or2 rdf:type rdf:Property; rdfs:domain :Eventuality; rdfs:range :Eventuality.
+
+
+(NOT property eventuality)
+(AND1 property eventuality)
+(AND2 property eventuality)
+(OR1 property eventuality)
+(OR2 property eventuality)
+
+;#Deontic modalities:
+;:DeonticModality rdf:type rdfs:Class; rdfs:subClassOf :Modality.
+;:Obligatory rdf:type rdfs:Class,:DeonticModality.
+;:Permitted rdf:type rdfs:Class,:DeonticModality.
+;:Optional rdf:type rdfs:Class,:DeonticModality.
+
+(deontic_modality class modality)
+(oligatory class deontic_modality)
+(permitted class deontic_modality)
+(optional class deontic_modality)
+
+;#------------------------------------------------------------------------------------------------------------------------------------------------
+
+;# 2nd-level classes and properties - classical logic operators applied to rdf:Statement(s), i.e., reifications of 1st-level assertions.
+;# These are needed because RDF vocabulary does not implement several operators from classical logic (negation, disjunction, etc.), nor
+;# the alethic modal logic operators of necessity (□) and possibility (◊)
+
+
+;:statement rdf:type rdfs:Class; rdfs:subClassOf rdf:Statement.
+;:true rdf:type rdfs:Class; rdfs:subClassOf :statement.
+;:false rdf:type rdfs:Class; rdfs:subClassOf :statement.
+;:hold rdf:type rdfs:Class; rdfs:subClassOf :statement.
+;:necessary a rdfs:Class; rdfs:subClassOf :statement.
+;:possible a rdfs:Class; rdfs:subClassOf :statement.
+;
+;:disjunction rdf:type rdf:Property;
+;	rdfs:domain :statement;
+;	rdfs:range :statement.
+
+(true class statement)
+(false class statement)
+(hold class statement)
+(necessary class statement)
+(possible class statement)
+
+(disjunction property (statement statement)) ;!!!!!!
+
+;#------------------------------------------------------------------------------------------------------------------------------------------------
+
+;3rd-level - explicit representation of contradictions, conflicts, violations, and other undesirable consequences (fallacies, mistakes, etc.)
+
+;:is-in-contradiction-with rdf:type rdf:Property;
+;	rdfs:domain :statement;
+;	rdfs:range :statement.
+;:is-in-conflict-with rdf:type rdf:Property;
+;	rdfs:domain :statement;
+;	rdfs:range :statement.
+;:is-complied-with-by rdf:type rdf:Property;
+;	rdfs:domain :statement;
+;	rdfs:range :statement.
+;:is-violated-by rdf:type rdf:Property;
+;	rdfs:domain :statement;
+;	rdfs:range :statement.
+;:is-necessary-violated-by rdf:type rdf:Property;
+;	rdfs:domain :statement;
+;	rdfs:range :statement.
+
+(is_in_contradiction_with property (statement statement))
+(is_in_conflict_with property (statement statement))
+(is_complied_with_by property (statement statement))
+(is_violated_by property (statement statement))
+(is_necessary_violated_by property (statement statement))
+
+;#------------------------------------------------------------------------------------------------------------------------------------------------
+;# Inference rules at the 1st level (the level of the eventualities)
+
+;#The following rule infers that if two eventualities are direct instantiations of the same abstract eventuality (i.e., they both describe the
+;#same action/state with the same thematic roles) but for at least one thematic role, for which it is asserted that one of the two eventualities
+;#has a certain value on that thematic role while the other one does not, then the two eventualities are connected by the ":not" property.
+
+;[rdf:type :InferenceRule;
+;	:has-sparql-code """CONSTRUCT{?e1 :not ?e2}
+;						WHERE{?e1 rdf:type ?c. ?e2 rdf:type ?c. ?c rdf:type :Eventuality. FILTER(?e1!=?e2)
+;						  ?trn rdf:type :ThematicRole. ?e1 ?trn ?vn. ?r rdf:type :false,:hold; rdf:subject ?e2; rdf:predicate ?trn; rdf:object ?vn.
+;						  NOT EXISTS{?tr rdf:type :ThematicRole. FILTER(?tr!=?trn) ?e1 ?tr ?tv1. NOT EXISTS{?e2 ?tr ?tv2}}
+;						  NOT EXISTS{?tr rdf:type :ThematicRole. FILTER(?tr!=?trn) ?e2 ?tr ?tv2. NOT EXISTS{?e1 ?tr ?tv1}}
+;						  NOT EXISTS{?tr rdf:type :ThematicRole. FILTER(?tr!=?trn) ?e1 ?tr ?tv1. ?e2 ?tr ?tv2. FILTER(?tv1!=?tv2)}}"""^^xsd:string].
+
+!(match &self (, ($e1 rdf:type $c) ($e2 rdf:type $c) ($c property eventuality))
+                 (if (not (== $e1 $e2))
+
+                    (match &self (, ($trn rdf:type :ThematicRole) ($e1 $trn $vn) (hold ($r rdf:type :false)) )
+                        (if (and (not_exist (, ($tr rdf:type :ThematicRole) ($e1 $tr $tv1) (not_exist ($e2 $tr $tv2))))
+                                 (not_exist (, ($tr rdf:type :ThematicRole) ($e2 $tr $tv2) (not_exist ($e1 $tr $tv1))))
+                                 (not_exist (, ($tr rdf:type :ThematicRole) ($e1 $tr $tv1) (($e2 $tr $tv2)))))
+
+                            (add-atom &self (NOT $e1 $e2))))))
+

deontic_logic/maker_atlas_examples/endgame_mip_amendment.metta

@@ -0,0 +1,34 @@
+;https://mips.makerdao.com/mips/details/MIP102#MIP102c1
+;MIP102c1: Purpose Description
+;Amendments
+;MIP Amendments that preserve the MIP number can be performed
+;to modify any aspect of an existing MIP, including MIP0.
+;There are no restrictions on how an existing MIP can be amended.
+;
+;Multiple amendments to multiple MIPs are allowed to be submitted
+;as a single subproposal.
+;
+;Removals
+;MIP102 also enables the removal of one or multiple MIPs
+;that are inactive as a part of the Endgame transition.
+;
+;Multiple MIPs may be removed in a single MIP Removal subproposal.
+
+(= (exist mip1) True)
+
+(= (inactive mip1) True)
+
+(= (preserve_mip_number amendment1 mip1) True)
+(= (preserve_mip_number amendment2 mip1) False)
+
+(= (preserve_mip_number amendment3 mip2) True)
+(= (preserve_mip_number amendment4 mip2) False)
+
+(= (permissible (modify $amendment $mip))
+    (and (== (preserve_mip_number $amendment $mip) True) (== (exist $mip) True)))
+
+(= (permissible (remove $mip))
+    (== (inactive $mip) True))
+
+!(permissible (modify amendment2 mip1))
+!(permissible (remove mip2))

deontic_logic/maker_atlas_examples/governance_scope.metta

@@ -0,0 +1,39 @@
+;https://mips.makerdao.com/mips/details/MIP101#2-the-governance-scope-gov
+
+;2.6.5.1.2
+;If FacilitatorDAOs fail to take action against misaligned AD,
+;they must be severely penalized.
+
+;Aligned Delegate (AD)
+;Aligned Delegates are Anonymous Alignment Conservers that
+;use the Protocol Delegation System
+;to enable regular MKR holders to easily
+;and safely delegate their MKR voting power
+;towards implementing the Aligned Governance Strategy of an AVC,
+;while earning Governance Participation Rewards in the process.
+
+;2.6.5.1
+;If a FacilitatorDAO finds that an AD has performed a misaligned act
+;or breached their requirements, they can derecognize the AD
+;and confiscate their AD Buffer.
+;The AD Buffer can be used as a whistleblower bounty in case
+;an ecosystem actor provided useful data, information or evidence
+;that led to the derecognition of the AD.
+;GOV6 must specify sufficient safety mechanisms around the payment of
+;the whistleblower bounty.
+
+(= (Facilitator DAO) True)
+(= (misaligned AD1) False)
+(= (misaligned AD2) True)
+
+(take-action DAO AD1)
+
+(= (obliged  (take-action $dao $ad))
+    (and (== (Facilitator $dao) True) (== (misaligned $ad) True)))
+
+(= (obliged  (be-penalized $dao $ad))
+    (and (and (== (Facilitator $dao) True) (== (misaligned $ad) True))
+    (not (== (match &self (take-action $dao $ad) $ad) $ad))))
+
+!(obliged (take-action DAO AD1))
+!(obliged (be-penalized DAO AD1))

deontic_logic/maker_atlas_examples/scope_bunded_mutable_alignment.metta

@@ -0,0 +1,10 @@
+;https://mips.makerdao.com/mips/details/MIP101#2-3-scope-bounded-mutable-alignment-artifacts-gov3
+
+
+;Scope Artifacts are continuously updated.
+;Their updates must always be aligned with the specifications of the Atlas.
+
+(= (update scope_artifacts) True)
+
+(= (obliged (align_with_specs $artifacts))
+    ((== (update $artifacts) True) ))