First-Order Logic Herbrand Semantic Profile of RuleML 1.02
From RuleML Wiki
(Redirected from Herbrand (First-Order Logic Syntax) Semantic Profile of RuleML 1.02)
- Identifier: http://ruleml.org/1.02/profiles/FOL-Herbrand
- Syntactic Scope: http://deliberation.ruleml.org/1.02/relaxng/myng-b3f-d7-a7-l1-p10-i79-t0-q0-e1-sb.rnc
- Classification: Herbrand
- RuleML rulebases are unordered in this semantics, and thus are effectively first-order theories, i.e. sets of formulas.
- 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.
- A query result is either
- The Herbrand semantics is defined for classical first-order logic syntax (FOLS) according to http://www.cs.uic.edu/~hinrichs/herbrand/html/herbrandlogic.html
- The mapping from RuleML syntax to FOLS is accomplished as follows:
- RuleML allows punning, i.e. the same name may be used for constants, functions of various arities and relations of various arities. When mapping to FOLS, these symbols must be disambiguated.
- Polyadic conjunction and disjunction are translated to appropriate compounds of binary conjunctions or disjunctions.
- Open sentences in RuleML are not allowed to be asserted, therefore there are no RuleML expressions that are mapped to this syntactic category in the defining syntax. In the inverse mapping (FOLS to RuleML), open FOLS sentences are mapped to universally quantified sentences.
- The negation of FOLS corresponds to the <Neg> element of RuleML.
- Parent: Predefined Semantic Profiles of RuleML 1.02
- Example: claim4disclaim.ruleml