Horn-PSOA Tarski Semantic Profile of RuleML 1.03

From RuleML Wiki
Jump to: navigation, search
  • Identifier: http://ruleml.org/1.03/profiles/HornPSOA-Tarski
  • Syntactic Scope: http://deliberation.ruleml.org/1.03/relaxng/myng-bf-d7-a7-l1-p001-i48-t633-q0-e9-sb.rnc
  • Classification: Tarski
  • Body:
    • Performatives (Assert, Retract, Query) sequentially induce effects on a dynamic global rulebase.
      • The effect of Assert and Retract is to modify the state of the global rulebase.
      • A "top-level" rulebase (a rulebase without a performative wrapper) is processed as an implicit Assert of that rulebase.
      • Before any performative is applied, the global rulebase is empty.
      • The effect of Assert is to add its formula payload (formulas contained directly or indirectly through a rulebase wrapper) to the global rulebase.
      • The effect of Retract is to (syntactically) subtract its formula payload from the global rulebase.
      • The effect of Query is to generate a query result w.r.t. the global rulebase. The global rulebase itself is unaffected.
        • A query result is either
          • a success, if one or more substitutions for the (zero or more) free variables are entailed by a Skolemization of the global rulebase where the Skolem function symbols are new relative to the global rulebase and the query. If the query contains free variables, then additionally the query result may contain a tabulation of these substitutions. If the query contains no free variables, then the tabulation is empty.
          • a failure, if no substitution for the free variables is entailed by the correspondingly Skolemized global rulebase.
    • The PSOA semantics, using slotribution instead of POSL's rest slots, is defined according to PSOA RuleML#Semantics.
    • The mapping between PSOA presentation syntax and RuleML/XML syntax is defined according to PSOA RuleML#Syntaxes.
  • Extends:
  • Restricts:
  • Parent: Predefined Semantic Profiles of RuleML 1.03
  • Example: addressRel2Obj.ruleml