diff --git a/deontic_logic/ct_dts.metta b/deontic_logic/ct_dts.metta index ac4564d..1202e7f 100644 --- a/deontic_logic/ct_dts.metta +++ b/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 ) diff --git a/deontic_logic/functional_examples/README.md b/deontic_logic/functional_examples/README.md new file mode 100644 index 0000000..ba95ca0 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/deontic_logic/functional_examples/infer2.metta b/deontic_logic/functional_examples/infer2.metta new file mode 100644 index 0000000..ab33ccc --- /dev/null +++ b/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))) diff --git a/deontic_logic/infer.metta b/deontic_logic/infer.metta index e71915e..ddd20ee 100644 --- a/deontic_logic/infer.metta +++ b/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) diff --git a/deontic_logic/maker_atlas_examples/README.md b/deontic_logic/maker_atlas_examples/README.md new file mode 100644 index 0000000..7d3e835 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/deontic_logic/maker_atlas_examples/ctDTS.metta b/deontic_logic/maker_atlas_examples/ctDTS.metta new file mode 100644 index 0000000..a4cff1d --- /dev/null +++ b/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)))))) + diff --git a/deontic_logic/maker_atlas_examples/endgame_mip_amendment.metta b/deontic_logic/maker_atlas_examples/endgame_mip_amendment.metta new file mode 100644 index 0000000..69c2123 --- /dev/null +++ b/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)) diff --git a/deontic_logic/maker_atlas_examples/governance_scope.metta b/deontic_logic/maker_atlas_examples/governance_scope.metta new file mode 100644 index 0000000..3de7c11 --- /dev/null +++ b/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)) diff --git a/deontic_logic/maker_atlas_examples/scope_bunded_mutable_alignment.metta b/deontic_logic/maker_atlas_examples/scope_bunded_mutable_alignment.metta new file mode 100644 index 0000000..73f29e0 --- /dev/null +++ b/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) )) \ No newline at end of file diff --git a/deontic_logic/maker_atlas_examples/sky_primitives/asc_rules/asc_rules.metta b/deontic_logic/maker_atlas_examples/sky_primitives/asc_rules/asc_rules.metta new file mode 100644 index 0000000..4c37097 --- /dev/null +++ b/deontic_logic/maker_atlas_examples/sky_primitives/asc_rules/asc_rules.metta @@ -0,0 +1,109 @@ +;ASC rules +; +;The ASC rules ensure that Stars all participate in +;maintaining the stability and peg of USDS. +; +;# Actively stabilizing collateral (ASC): +; +;ASC is collateral that is actively market making against USDS, +;supporting its peg and bidding at a price of at least 0.999 USD per USDS +;(10bps downside spread). +; +;ASC can be USDC and USDT in the PSM, curve, other stablecoins, +;or crypto assets, as long as it is enforced that they enable +;real time redemption of USDS at at least 0.999 USD per USDS. +; +;ASC can also be offchain as RWA loans to market makers, +;as long as there is clear public real time information about the exposure, +;proving that it is at all times used to provide buy support of at least +;0.999 USD per USDS +; +;If a Star doesn’t maintain at least 20% of its collateral portfolio in ASC, +;it will continuously be penalized at a rate of 200% APY on the missing ASC. +;This penalty is settled monthly at the settlement cycle, and retroactively +;calculated per second. +; +;# Demand Absorption Buffer +; +;Demand Absorption Buffer is a type of ASC consisting of USDS that is +;for sale for at most 1.001 USD per USDS. Every Star must maintain a DAB +;equivalent to 25% of their standard ASC requirement. USDS held by a Star is +;not considered a part of its collateral portfolio for the purposes of +;calculating ASC requirements. DAB requirements can also be fulfilled by +;autonomous systems that generate USDS dynamically through the allocation as +;needed. +; +;# Peg Defense Event +; +;A Peg Defense Event is a situation where the volume weighted average price +;of USDS on SkyLink enabled blockchains falls below 0.999 USD per USDS. +; +;In this situation, all Stars must immediately begin to buy USDS at +;a rate of at least 6.25% of their ASC requirement every 6 hours. +; +;If they fail to fulfill this requirement, a penalty of 20 bps on +;all missing buy volume is applied, calculated in finished blocks of +;6 hours from the Peg Defense Event begins, and settled retroactively at +;the monthly settlement cycle. +; +;Peg Defense can be performed both by selling other types of collateral for +;USDS, or by using USDS, or generating new USDS via the allocation system, +;that is then used as collateral on e.g. aave to borrow USDC or USDT and +;buy USDS with it. +; +;# ALM obligation transfer +; +;The ASC and Peg Defense obligation can be transfered against payment to +;a different Star, through the ALM obligation transfer system. +;Both ASC and Peg Defense responsibilities are transferred together, +;as they are tied together. + +(= (asset usdt) 100) +(= (asset usds) 200) +(= (asset usdc) 300) + +(= (apy-rate r1) 2) + +(= (penalize $asset $rate) + (let $res (/ $asset $rate) + $res) +) + +(= (stabilizing_collateral $asset $threshold $rate) + (if(>= $asset $threshold) + (penalize $asset $rate) + False + ) + ) + +(= (volume_weighted_average_price usdt) 1000) + +;(bind! acc1 (usdt 100)) +;(bind! acc2 (usdt 200)) +;(bind! acc3 (usdt 300)) +; +;(= (asset s1) (usdt 100)) +;(= (asset s2) (usdt 200)) +;(= (asset s3) (usdc 100)) + +(= (star_agent a1) s1) + +!(bind! &acc1 (new-state (usdt 100))) + +(= (asset s1) &acc1) + +!(change-state! &acc1 (usdt 200)) + +(= (increase_by_quant $num $quant) + (+ $num $quant) +) + +(= (buy $agent $quant) + (asset $agent) +) + +(= (peg_defense_event $vwap $threshold $agent_list) + (if(>= $vwap $threshold) + (buy $asset ) + ) +) \ No newline at end of file diff --git a/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/genesis_account.metta b/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/genesis_account.metta new file mode 100644 index 0000000..792a5c5 --- /dev/null +++ b/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/genesis_account.metta @@ -0,0 +1,23 @@ +;This account counts as controlling 100% of the circulating token supply for +;governance purposes, +;enabling editing of the spark artifact before creation of the Spark token + +(= (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)) + + +(bind! &master_acc (new-state (supply percent 100))) + +(bind! &enable_editing (new-state (token_emission True))) + +(= (obliged (enable_editing $artifacts)) + ((== (proposal_alignment $artifacts) True) )) \ No newline at end of file diff --git a/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/include_test.metta b/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/include_test.metta new file mode 100644 index 0000000..37d2623 --- /dev/null +++ b/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/include_test.metta @@ -0,0 +1,8 @@ +!(import! &self spark_artifact_edits) +;!(import! &self token_distribution_obligation) +;!(import! &self token_emissions) + +!(import! &self infer2) + + +! (infer (ob (align_with_atlas prop2))) \ No newline at end of file diff --git a/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/infer2.metta b/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/infer2.metta new file mode 100644 index 0000000..8caafd2 --- /dev/null +++ b/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/infer2.metta @@ -0,0 +1,66 @@ +(:-- 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. + +(: ob (-> Atom Bool)) + +(:-- (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))) diff --git a/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/spark_artifact_edits.metta b/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/spark_artifact_edits.metta new file mode 100644 index 0000000..ca7c3c6 --- /dev/null +++ b/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/spark_artifact_edits.metta @@ -0,0 +1,70 @@ +;A.S1.P1.1 +;Name: Spark Artifact Edits + +;Spark Artifact Edits require a simple majority of SPK holders in +;a weekly SPK Snapshot poll with a minimum quorum of 10% of circulating +;token supply. To propose a Spark Artifact Edit, an SPK holder must have +;at least 1% of the circulating token supply. +;When a proposal is made the Operational Facilitator must determine its +;alignment, and if it is considered in alignment with the Atlas and +;Spark Artifact, the edit proposal is put to a snapshot poll. +;If the poll is successful, the Facilitator must instruct the operational +;govops to carry out the artifact update. + +(= (allow_spark_artifact_edits m1) False) + +(= (spk_holder h1) 2) + +(= (spk_holder h2) 4) + +(= (spk_holder h3) 5) + +(= (spk_holder h4) 2) + +(= (spk_holder h5) 0.5) + +(= (propose thresh) 0.1) + + +(= (operational_facilitator o1) True) + +(= (proposal_alignment prop1) True) +(= (proposal_alignment prop2) False) + +(= (acc prop1) 0.1) +(= (acc prop2) 0.2) + +(= (stake-size $participants) + (let $lst (collapse (spk_holder (superpose $participants))) + (foldl-atom $lst 0 $x $y (+ $x $y))) +) + +(= (enough-stake-size? $participants $threshold) + (>= (stake-size $participants) $threshold) +) + +!(enough-stake-size? (h1 h3 h5) 7) +!(enough-stake-size? (h1 h3 h5) 8) + +(= (obliged (align_with_atlas $artifacts)) + ((== (proposal_alignment $artifacts) True) )) + +(= (obliged (align_with_atlas $artifacts)) + (if (<= (acc $artifacts) (propose thresh)) + (== (proposal_alignment $artifacts) + (stake-size $artifacts)) True)) + +(= (ob (align_with_atlas $artifacts)) + ((== (proposal_alignment $artifacts) True) )) + +(= (ob (align_with_atlas $artifacts)) + (if (<= (acc $artifacts) (propose thresh)) + (== (proposal_alignment $artifacts) + (stake-size $artifacts)) True)) + +(= (vote $participants) + True) + +!(size-atom (h1 h3 h5)) + +!(obliged (align_with_atlas prop2)) \ No newline at end of file diff --git a/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/token_distribution_obligation.metta b/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/token_distribution_obligation.metta new file mode 100644 index 0000000..3262164 --- /dev/null +++ b/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/token_distribution_obligation.metta @@ -0,0 +1,37 @@ +;# A.S1.P5 +; +;Name: Token Distribution Obligation +; +;Spark is required to distribute 0.2% of +;its total token supply per year to USDS holders. + +(bind! &redist_const (new-state (value 0.2))) + +(bind! &acc1 (new-state (usdt 100))) + +(= (star_agent a1) &acc1) + +(bind! &total_inc (new-state (usdt 100))) + +(= (obliged (supply_token $artifacts)) + ((== (proposal_alignment $artifacts) True) )) + +(= (obliged (be-penalized $dao $ad)) + (and (and (== (Facilitator $dao) True) (== (misaligned $ad) True)) + (not (== (match &self (take-action $dao $ad) $ad) $ad)))) + +(= (redis_by_val_ $holder) + (let (State ($asset_type $inc)) (&total_inc) + (let (State (&_ $rc)) (&redist_const) (+ (* $inc $rc) (star_agent $holder)))) +) + +(= (redis_by_val $holder) + (change-state! $holder (usdt (redis_by_val_ $holder))) +) + +(= (redistribute $holder_list ) + + (let $holder ($holder_list)(obliged (star_agent $holder) + (redis_by_val $holder)) +) + diff --git a/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/token_emissions.metta b/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/token_emissions.metta new file mode 100644 index 0000000..7d31a01 --- /dev/null +++ b/deontic_logic/maker_atlas_examples/sky_primitives/spark_artifact/token_emissions.metta @@ -0,0 +1,19 @@ +;Token emissions +; +;Token emissions irreversibly disabled: True + +(bind! &emissions_irreversibly (new-state (token_emission False))) + + + +(= (obliged (support_council_member $m)) + (and (== (approved $m) True) + (and (== (ecosystem-actor $m) True) + (not (== (side-engagement $m) True))))) + +!(obliged (support_council_member m1)) ;False + +(= (permissible (remove $m)) + (== (paid-work-under-last-year $m) False)) + +!(permissible (remove m3)) \ No newline at end of file diff --git a/deontic_logic/maker_atlas_examples/stability_advisory.metta b/deontic_logic/maker_atlas_examples/stability_advisory.metta new file mode 100644 index 0000000..9865351 --- /dev/null +++ b/deontic_logic/maker_atlas_examples/stability_advisory.metta @@ -0,0 +1,101 @@ +;https://mips.makerdao.com/mips/details/MIP104#1-1-1-4 + +;1.1.1.5: Stability Advisory Council Requirements +;1.1.1.5.1 +;Stability Advisory Council members can be individuals, +;groups of people, legal entities, or companies. +;They can be pseudonymous or known entities. +;Stability Advisory Council members must be aligned with +;the long-term goals of MakerDAO Endgame. +; +;1.1.1.5.2 +;Desired competencies for members of the Stability Advisory Council, +;as many of the following as possible: +; +;Expertise in capital markets, bonds, equities. +;Experience as a market analyst or economist. +;Expertise in tokenomics. +;Expertise in fund management and risk profiles. +;Deep knowledge of decentralized collateral accounting and finance. +;Experience in credit risk, market risk, liquidity risk, and operational risk. +;Deep understanding of principles of portfolio construction, asset allocation, +;diversification strategies, and performance measurement. +;Experience in smart contract and DeFi risk management. +;Experience in economic modeling of high-volatility portfolios. +;Expertise in Value at Risk analysis with detailed knowledge about +;the limitations of the method. + +;(= (council-member m1) True) +;(= (council-member m2) True) +;(= (council-member m3) True) +;(= (council-member m4) True) +;(= (council-member m5) True) + +;(being m1 individual) +;(being m2 group) +;(being m3 legal-entity) +;(being m4 company) +;(being m5 government) + +(= (individual m1) True) +(= (group m2) True) +(= (legal-entity m3) True) +(= (company m4) True) +(= (government m5) True) + +;(= (permissible (council-member $m)) +; (or (unify (being $m $r) (being $s individual) +; True False) +; (or (unify (being $m $r) (being $s group) +; True False) +; (or (unify (being $m $r) (being $s legal-entity) +; True False) +; (unify (being $m $r) (being $s company) +; True False))))) + +(= (permissible (council-member $m)) + (or (== (individual $m) True) + (or (== (group $m) True) + (or (== (legal-entity $m) True) + (== (company $m) True))))) + + +;!(permissible (council-member m1)) +;!(permissible (council-member m5)) + +(= (permissible economics) True) +(= (permissible capital-markets) True) +(= (permissible tokenomics) True) +(= (permissible credit-risk) True) +(= (permissible portfolio-construction) True) + + +(= (economics m1) True) +(= (capital-markets m2) True) +(= (tokenomics m3) True) +(= (credit-risk m4) True) +(= (portfolio-construction m5) True) + +(= (tokenomics m1) True) + +(= (permissible (experience $e $m)) + (and (== ($e $m) True) + (== (permissible $e) True))) + + +(= (omissible (experience $e $m)) + (unify ($e $m) ($s $m) True False)) + +;How to do that one of the experience types became optional? +;m1 has both economics and tokenomics +;E.g. we want to call !(optional (experience economics m1)) and get true + + +(= (optional (experience $e $m)) + (and (permissible (experience $e $m)) + (omissible (experience $e $m)))) + + +;!(unify (economics m1) (tokenomics m1) True False) + +!(permissible (experience chill m1)) diff --git a/deontic_logic/maker_atlas_examples/support_advisory_council_membership_management.metta b/deontic_logic/maker_atlas_examples/support_advisory_council_membership_management.metta new file mode 100644 index 0000000..e06332e --- /dev/null +++ b/deontic_logic/maker_atlas_examples/support_advisory_council_membership_management.metta @@ -0,0 +1,99 @@ +;https://mips.makerdao.com/mips/details/MIP106#1-1-1-support-advisory-council-membership-management + +;1.1.1: Support Advisory Council Membership Management +;Members of the Advisory Council are directly approved by +;Maker Governance through a governance poll, and +;must fulfill specific criteria. +; +;1.1.1.1 +;The Support Facilitators must ensure that +;potential Advisory Council Members can apply to be approved by +;Maker Governance, using an open process with clear instructions +;as per 1.1.1.3. +; +;1.1.1.2 +;Advisory Council Members must be ecosystem actors that are not involved +;in any business, political, or other governance-related activity that +;could result in a conflict of interest, either directly or indirectly. +;They must also have relevant skills for providing professional expert input +;on the content that the Support Scope is covering. +; +;1.1.1.3 +;The Support Facilitators must periodically, +;when it is relevant, review the Advisory Council Applications, +;and if they find applications that are suitable, bring them to +;a vote through an MKR governance poll. +;When Advisory Council Applications are posted on the Maker Forum, +;which must follow the template as per 1.1.2.4.1A, +;the Support Facilitators have a review period of 30 days. +;During this review period, the applicant must host a Community Q&A and +;shall answer as many questions and doubts as possible. +; +;1.1.1.3.1 +;The Support Facilitators can extend this deadline, +;if necessary, by 15 days, provided they posted the justification +;in the Maker Forum. +; +;1.1.1.3.2 +;Once the review period is ended, the Support Facilitators must publish +;the response to the application on the Forum, along with a description of +;the reasoning behind the decision. If approved, the application will +;continue with the Governance Process and proceed to a vote as per 1.1.1.3. +; +;1.1.1.3.3 +;Upon a successful vote, the Support Facilitators must arrange +;a service contract with the Advisory Council member, +;which must be made public. Approved Advisory Council Members are +;added to 1.1.1.6.1A. +; +;1.1.1.3.4 +;Approved Advisory Council members have a term of service of 18 months from +;the time they are approved by Maker Governance. +;If desired, the Advisory Council Member can submit a new application for +;re-election when their term has between 60 and 30 days remaining. +;The re-election application must also fulfill 1.1.2 requirements and +;will open a new review period of 30 days where the Maker Community can +;provide feedback. The applicant shall again host a Community Q&A and +;respond to as many questions and doubts as possible. +;If approved, the re-election application will continue with the +;Governance Process and proceed to a vote as per 1.1.1.3. +; +;1.1.1.4 +;The Support Facilitators may, if they deem it necessary, +;hold a vote to remove an Advisory Council Member. +;If an Advisory Council Member has not done any paid work for the Scope for +;at least 1 year, then the Support Facilitators can choose to remove them at +;will, if they deem it necessary. + +;(= (support_council_member m1) True) + +(= (approved m1) True) +(= (approved m2) True) +(= (approved m3) False) + +(= (ecosystem-actor m1) True) +(= (ecosystem-actor m2) False) +(= (ecosystem-actor m3) False) + +(= (side-engagement m1) True) +(= (side-engagement m2) False) +(= (side-engagement m3) False) + +(= (paid-work-under-last-year m1) True) +(= (paid-work-under-last-year m2) False) + +(= (obliged (support_council_member $m)) + (and (== (approved $m) True) + (and (== (ecosystem-actor $m) True) + (not (== (side-engagement $m) True))))) + +!(obliged (support_council_member m1)) ;False + +(= (permissible (remove $m)) + (== (paid-work-under-last-year $m) False)) + +!(permissible (remove m3)) + +;How to remove a member from support council? +;Store a predicate for every potential member and turn them false? +;Or do an atomspace rewrite? diff --git a/deontic_logic/sparql2metta/README.md b/deontic_logic/sparql2metta/README.md new file mode 100644 index 0000000..83434f8 --- /dev/null +++ b/deontic_logic/sparql2metta/README.md @@ -0,0 +1,44 @@ +# Overview + +Examples of mapping between SPARQL language commands and some of the MeTTa concepts are collected in this folder. + +Each file except inference engine has commented example in SPARQL and corresponding example in MeTTa. + +## List of scripts + +[not_exist.metta](not_exist.metta) + +This script implements basic command, which returns false if pattern matches and true otherwise. + +[filter.metta](filter.metta) + +This script implements is a restriction on solutions over the whole group pattern in which the filter appears. + +[construct.metta](construct.metta) + +This script implements command that returns a single graph specified by a graph template. +The result is formed by taking each query solution in the solution sequence, substituting for the variables in the graph template, +and combining the triples into a single graph adding it to the space. + +[bind.metta](bind.metta) + +This script implements command that allows a value to be assigned to a variable from a basic graph pattern or property path expression. +Very similar to a `let` function in Metta. + +[union.metta](union.metta) + +This script implements command that provides a means of combining graph patterns so that one of several alternative graph patterns may match. +If more than one of the alternatives matches, all the possible pattern solutions are found. + +[very_simple_inference_engine.metta](very_simple_inference_engine.metta) + +This script implements simple variant of rule engine that takes a list of rules, each of which either populates space with new facts or returns Empty, +and consistently applies these rules until knowledge base does not change. + +[transitive_closure_clr.metta](transitive_closure_clr.metta) + +This script provides simple transitive closure example for a family graph using some of the commands above and the inference engine. + +[transitive_closure_clr2.metta](transitive_closure_clr2.metta) + +This script provides simple transitive closure example for a book authors graph using some of the commands above and the inference engine. \ No newline at end of file diff --git a/deontic_logic/sparql2metta/bind.metta b/deontic_logic/sparql2metta/bind.metta new file mode 100644 index 0000000..2b0a6f7 --- /dev/null +++ b/deontic_logic/sparql2metta/bind.metta @@ -0,0 +1,62 @@ +;@prefix dc: . +;@prefix : . +;@prefix ns: . +; +; +;PREFIX dc: +;PREFIX ns: +; +;:book1 dc:title "SPARQL Tutorial" . +;:book1 ns:price 42 . +;:book1 ns:discount 0.2 . +; +;:book2 dc:title "The Semantic Web" . +;:book2 ns:price 23 . +;:book2 ns:discount 0.25 . + +;SELECT ?title ?price +;{ ?x ns:price ?p . +; ?x ns:discount ?discount +; BIND (?p*(1-?discount) AS ?price) +; FILTER(?price < 20) +; ?x dc:title ?title . +;} + +;PREFIX dc: +;PREFIX ns: +; +;SELECT ?title ?price +;{ { ?x ns:price ?p . +; ?x ns:discount ?discount +; BIND (?p*(1-?discount) AS ?price) +; } +; {?x dc:title ?title . } +; FILTER(?price < 20) +;} + +;title price +; "The Semantic Web" 17.25 + +(book1 title sprql-tutorial) +(book1 price 42) +(book1 discount 0.2) +(book2 title semantic-web) +(book2 price 23) +(book2 discount 0.25) + + +;!(match &self ($x price $y) (match &self ($x discount $z) +; (let $price (* $y (- 1 $z)) +; (if (< $price 20) +; (match &self ($x title $t) ($t $price)) +; Empty)))) + +!(match &self (, ($x price $y) ($x discount $z)) + (let $price (* $y (- 1 $z)) + (if (< $price 20) + (match &self ($x title $t) ($t $price)) + Empty))) + +;!(match &self (, ($x price $y) ($x discount $z)) +; (let $price (* $y (- 1 $z)) +; $price)) \ No newline at end of file diff --git a/deontic_logic/sparql2metta/construct.metta b/deontic_logic/sparql2metta/construct.metta new file mode 100644 index 0000000..eea85f4 --- /dev/null +++ b/deontic_logic/sparql2metta/construct.metta @@ -0,0 +1,19 @@ +;@prefix foaf: . +; +;_:a foaf:name "Alice" . +;_:a foaf:mbox . +;PREFIX foaf: +;PREFIX vcard: +;CONSTRUCT { vcard:FN ?name } +;WHERE { ?x foaf:name ?name } +; +; vcard:FN "Alice" . + + +(a name Alice) +(a mbox mailtoAlice) + +!(match &self ($x name $name) (add-atom &self (exampleAlice FN $name))) +;!(let $atom (match &self ($x name $name) (exampleAlice FN $name)) (add-atom &self $atom)) + +!(match &self (exampleAlice FN Alice) (exampleAlice FN Alice)) \ No newline at end of file diff --git a/deontic_logic/sparql2metta/filter.metta b/deontic_logic/sparql2metta/filter.metta new file mode 100644 index 0000000..6b13974 --- /dev/null +++ b/deontic_logic/sparql2metta/filter.metta @@ -0,0 +1,43 @@ +;:book1 dc:title "SPARQL Tutorial" . +;:book1 ns:price 42 . +;:book2 dc:title "The Semantic Web" . +;:book2 ns:price 23 . + +;SELECT ?title ?price +;WHERE { ?x ns:price ?price . +; FILTER (?price < 30.5) +; ?x dc:title ?title . } + +;title price +;"The Semantic Web" 23 + +(book1 title sprql-tutorial) +(book1 price 42) +(book2 title semantic-web) +(book2 price 23) + +!(match &self ($x price $y) + (if (< $y 30.5) + (match &self ($x title $z) ($z $y)) + Empty)) + +!(match &self + (, ($x price $y) + ($x title $z)) + (if (< $y 30.5) ($z $y) Empty)) + +;(= (filter $pattern) +; (match &self ($x price $y) +; (if $pattern +; (match &self ($x title $z) ($z $y)) +; Empty))) +; +; +;(= (filter (less-than $b)) +; (match &self ($x price $y) +; (if (< ) +; (match &self ($x title $z) ($z $y)) +; Empty))) +; +;!(filter (< $y 30.5)) + diff --git a/deontic_logic/sparql2metta/inference_test.metta b/deontic_logic/sparql2metta/inference_test.metta new file mode 100644 index 0000000..e69de29 diff --git a/deontic_logic/sparql2metta/multiple_level_tr_clo.metta b/deontic_logic/sparql2metta/multiple_level_tr_clo.metta new file mode 100644 index 0000000..e69de29 diff --git a/deontic_logic/sparql2metta/not_exist.metta b/deontic_logic/sparql2metta/not_exist.metta new file mode 100644 index 0000000..2045517 --- /dev/null +++ b/deontic_logic/sparql2metta/not_exist.metta @@ -0,0 +1,12 @@ +; xsd:boolean NOT EXISTS { pattern } +;Returns false if pattern matches. Returns true otherwise. +; +;NOT EXISTS { pattern } is equivalent to fn:not(EXISTS { pattern }). +; +; xsd:boolean EXISTS { pattern } +;Returns true if pattern matches. Returns false otherwise. + +(: not_exist (-> Atom Bool)) +(= (not_exist $pattern) + (let $top-space (mod-space! top) + (unify $top-space $pattern False True))) diff --git a/deontic_logic/sparql2metta/test_recursion.metta b/deontic_logic/sparql2metta/test_recursion.metta new file mode 100644 index 0000000..e69de29 diff --git a/deontic_logic/sparql2metta/transitive_closure.metta b/deontic_logic/sparql2metta/transitive_closure.metta new file mode 100644 index 0000000..e69de29 diff --git a/deontic_logic/sparql2metta/transitive_closure_clr.metta b/deontic_logic/sparql2metta/transitive_closure_clr.metta new file mode 100644 index 0000000..95eb1eb --- /dev/null +++ b/deontic_logic/sparql2metta/transitive_closure_clr.metta @@ -0,0 +1,65 @@ +;# People and their favorite books +;ex:John a ex:Person ; +; ex:likesBook ex:BookA . +; +;ex:Alice a ex:Person ; +; ex:likesBook ex:BookC . +; +;# Books and inspiration (transitive) +;ex:BookA a ex:Book . +;ex:BookB a ex:Book . +;ex:BookC a ex:Book . +;ex:BookD a ex:Book . +; +;# Inspiration connection inspiredBy +;ex:BookB ex:inspiredBy ex:BookA . +;ex:BookC ex:inspiredBy ex:BookB . +;ex:BookD ex:inspiredBy ex:BookC . +; +;# Authors +;ex:Author1 a ex:Author ; +; ex:wrote ex:BookA . + +;PREFIX ex: +; +;SELECT DISTINCT ?person ?book +;WHERE { +; ?person a ex:Person ; +; ex:likesBook ?book . +; +; #Recursive transitive closure up to 3 levels of inspiredBy +; ?book ex:inspiredBy ?b1 . +; ?b1 ex:inspiredBy ?b2 . +; ?b2 ex:inspiredBy ?b3 . +; +; # Author wrote the initial book +; ?author a ex:Author ; +; ex:wrote ?b3 . +;} + +!(import! &self very_simple_inference_engine) +!(import! &self not_exist) + +(likesBook (Person John) BookA) +(likesBook (Person Alice) BookB) + +(Book BookA) +(Book BookB) +(Book BookC) +(Book BookD) + +(inspiredBy BookB BookA) +(inspiredBy BookC BookB) +(inspiredBy BookD BookC) + +(wrote (Author Author1) BookA) + +(= (rule1) + (match &self (inspiredBy $x $y) (if (not_exist (influenced $x $y)) (add-atom &self (influenced $x $y)) Empty))) + +(= (rule2) + (match &self (, (inspiredBy $x $y) (influenced $y $z)) (if (not_exist (influenced $x $z)) (add-atom &self (influenced $x $z)) Empty))) + +!(rule-engine (rule1 rule2)) + +!(match &self (influenced BookD $y) $y) \ No newline at end of file diff --git a/deontic_logic/sparql2metta/transitive_closure_clr2.metta b/deontic_logic/sparql2metta/transitive_closure_clr2.metta new file mode 100644 index 0000000..6b2b80e --- /dev/null +++ b/deontic_logic/sparql2metta/transitive_closure_clr2.metta @@ -0,0 +1,103 @@ +;@prefix ex: . +;@prefix rdf: . +; +;# People +;ex:Alice a ex:Person . +;ex:Bob a ex:Person . +;ex:Charlie a ex:Person . +;ex:Diana a ex:Person . +; +;# Relationships +;ex:Alice ex:isParentOf ex:Bob . +;ex:Bob ex:isParentOf ex:Charlie . +;ex:Charlie ex:isParentOf ex:Diana . + +;@prefix ex: . +;@prefix rdf: . +; +;# People +;ex:Alice a ex:Person . +;ex:Bob a ex:Person . +;ex:Charlie a ex:Person . +;ex:Diana a ex:Person . +; +;# Relationships +;ex:Alice ex:isParentOf ex:Bob . +;ex:Bob ex:isParentOf ex:Charlie . +;ex:Charlie ex:isParentOf ex:Diana . +; +;PREFIX ex: +; +;CONSTRUCT { +; ?grandparent ex:isGrandparentOf ?grandchild . +;} +;WHERE { +; ?grandparent ex:isParentOf ?parent . +; ?parent ex:isParentOf ?grandchild . +;} + +;PREFIX ex: +; +;CONSTRUCT { +; ?greatGrandparent ex:isGreatGrandparentOf ?greatGrandchild . +;} +;WHERE { +; ?greatGrandparent ex:isParentOf ?grandparent . +; ?grandparent ex:isGrandparentOf ?greatGrandchild . +;} + +;PREFIX ex: +; +;CONSTRUCT { +; ?ancestor ex:isAncestorOf ?descendant . +;} +;WHERE { +; ?ancestor ex:isParentOf ?descendant . +;} + +;PREFIX ex: +; +;CONSTRUCT { +; ?ancestor ex:isAncestorOf ?descendant . +;} +;WHERE { +; ?ancestor ex:isParentOf ?intermediate . +; ?intermediate ex:isAncestorOf ?descendant . +;} + +!(import! &self very_simple_inference_engine) +!(import! &self not_exist) + +(Parent Tom Bob) +(Parent Pam Bob) +(Parent Tom Liz) +(Parent Bob Ann) +(Parent Bob Pat) +(Parent Pat Jim) +(Parent Jim Lil) + +(Person (Female Pam)) +(Person (Female Liz)) +(Person (Female Ann)) +(Person (Female Lil)) +(Person (Male Tom)) +(Person (Male Bob)) +(Person (Male Pat)) +(Person (Male Jim)) + + +(= (rule1) + (match &self (Parent $x $y) (if (not_exist (Predecessor $x $z)) (add-atom &self (Predecessor $x $y)) Empty))) + +(= (rule2) + (match &self (, (Parent $x $y) (Predecessor $y $z)) (if (not_exist (Predecessor $x $z)) (add-atom &self (Predecessor $x $z)) Empty))) + +(= (rule3) + (match &self (, (Predecessor $y $z) (Person (Female $y))) (if (not_exist (FemPredecessor $y $z)) (add-atom &self (FemPredecessor $y $z)) Empty))) + + +!(rule-engine (rule1 rule2 rule3)) + +!(match &self (Predecessor $y Jim) $y) + +!(match &self (FemPredecessor $y Jim) $y) diff --git a/deontic_logic/sparql2metta/union.metta b/deontic_logic/sparql2metta/union.metta new file mode 100644 index 0000000..a48cade --- /dev/null +++ b/deontic_logic/sparql2metta/union.metta @@ -0,0 +1,33 @@ +;_:a dc10:title "SPARQL Query Language Tutorial" . +;_:a dc10:creator "Alice" . +; +;_:b dc11:title "SPARQL Protocol Tutorial" . +;_:b dc11:creator "Bob" . +; +;_:c dc10:title "SPARQL" . +;_:c dc11:title "SPARQL (updated)" . + +;PREFIX dc10: +;PREFIX dc11: +; +;SELECT ?title +;WHERE { { ?book dc10:title ?title } UNION { ?book dc11:title ?title } } + +;"SPARQL Protocol Tutorial" +;"SPARQL" +;"SPARQL (updated)" +;"SPARQL Query Language Tutorial" + +(Entry (a title1 tutorial1)) +(Entry (a creator Alice)) +(Entry (b title2 tutorial2)) +(Entry (b creator Bob)) +(Entry (c title1 tutorial3)) +(Entry (c title2 tutorial3Updated)) + + +!(match &self (Entry ($x $y $title)) + (case $y + ((title1 $title) + (title2 $title) + ($_ Empty)))) \ No newline at end of file diff --git a/deontic_logic/sparql2metta/very_simple_inference_engine.metta b/deontic_logic/sparql2metta/very_simple_inference_engine.metta new file mode 100644 index 0000000..525c08d --- /dev/null +++ b/deontic_logic/sparql2metta/very_simple_inference_engine.metta @@ -0,0 +1,24 @@ +(= (rule-bool $rule) + (case ($rule) ( + (Empty True) + ($_ False) + ))) + +(: rule-applicator (-> Expression Expression)) +(= (rule-applicator $rules) + (trace! (noeval $rules) (if-decons-expr $rules $head $tail + (let $res (rule-bool $head) (let $recres (rule-applicator $tail) (cons-atom $res $recres))) + ()))) + +(= (applic-checker $rules_outputs) + (foldl-atom $rules_outputs True $a $b (and $a $b))) + + +;rule engine takes a list of rules, each of which either populates space with new facts or returns Empty, +;and consistently applies these rules until knowledge base does not change + +(= (rule-engine $rules) + (if (applic-checker (rule-applicator $rules)) + Empty + (rule-engine $rules)) + ) \ No newline at end of file