RuleML, profile picture
Uploaded byRuleML
PDF, PPTX664 views

RuleML 2015: Semantics of Notation3 Logic: A Solution for Implicit Quantification

The document discusses the semantics of Notation3 logic, which is a rule logic for the Semantic Web invented by Tim Berners-Lee and Dan Connolly. Notation3 logic allows for implicit quantification using blank nodes and variables starting with question marks. The semantics of Notation3 logic is not fully defined, though implementations provide some guidance. The paper proposes handling implicit quantification by defining the scope of existential variables as the formula they occur in, while universal variables have scope that includes descendant formulas. A formal semantics is introduced using substitutions and their component-wise and total applications to formulas.

Download as PDF, PPTX
ELIS – Multimedia Lab Semantics of Notation3 Logic: A solution for implicit quantification Dörthe Arndt, Ruben Verborgh, Jos De Roo, Hong Sun, Erik Mannens, and Rik Van De Walle Multimedia Lab, Ghent University - iMinds, Belgium Agfa Healthcare - Ghent, Belgium RuleML 2015, Berlin, August 04, 2015 1 / 28
ELIS – Multimedia Lab Outline Notation3 Logic Implicit Quantification Formal Semantics 2 / 28
ELIS – Multimedia Lab Notation3 Logic Notation3 Logic What is Notation3 Logic? Syntax Semantics Implicit Quantification Formal Semantics 3 / 28
ELIS – Multimedia Lab What is Notation3 Logic? A rule logic for the Semantic Web 4 / 28
ELIS – Multimedia Lab What is Notation3 Logic? A rule logic for the Semantic Web Invented by Tim Berners-Lee and Dan Connolly (∼2005) 4 / 28
ELIS – Multimedia Lab What is Notation3 Logic? A rule logic for the Semantic Web Invented by Tim Berners-Lee and Dan Connolly (∼2005) Superset of RDF/Turtle 4 / 28
ELIS – Multimedia Lab Syntax 5 / 28
ELIS – Multimedia Lab Syntax Simple Turtle triples: 5 / 28
ELIS – Multimedia Lab Syntax Simple Turtle triples: :Socrates a :Man. 5 / 28
ELIS – Multimedia Lab Syntax Simple Turtle triples: :Socrates a :Man. Rules: 5 / 28
ELIS – Multimedia Lab Syntax Simple Turtle triples: :Socrates a :Man. Rules: {:Socrates a :Man.} => {:Socrates a :Mortal.}. 5 / 28
ELIS – Multimedia Lab Syntax Statements about formulas: 6 / 28
ELIS – Multimedia Lab Syntax Statements about formulas: :Plato :says {:Socrates a Mortal.}. 6 / 28
ELIS – Multimedia Lab Syntax Statements about formulas: :Plato :says {:Socrates a Mortal.}. Use of (quantified) variables: 6 / 28
ELIS – Multimedia Lab Syntax Statements about formulas: :Plato :says {:Socrates a Mortal.}. Use of (quantified) variables: :Plato :knows _:x. _:x a :Man. 6 / 28
ELIS – Multimedia Lab Syntax Statements about formulas: :Plato :says {:Socrates a Mortal.}. Use of (quantified) variables: :Plato :knows _:x. _:x a :Man. {?x a :Man.}=>{?x a :Mortal.}. 6 / 28
ELIS – Multimedia Lab What about Semantics? The formal semantics of N3 is not defined 7 / 28
ELIS – Multimedia Lab What about Semantics? The formal semantics of N3 is not defined(yet) 7 / 28
ELIS – Multimedia Lab What about Semantics? The formal semantics of N3 is not defined(yet) Some implementations even differ! 7 / 28
ELIS – Multimedia Lab What about Semantics? The formal semantics of N3 is not defined(yet) Some implementations even differ! But: 7 / 28
ELIS – Multimedia Lab What about Semantics? The formal semantics of N3 is not defined(yet) Some implementations even differ! But: Documents like the W3C Team Submission describe the desired semantics 7 / 28
ELIS – Multimedia Lab What about Semantics? The formal semantics of N3 is not defined(yet) Some implementations even differ! But: Documents like the W3C Team Submission describe the desired semantics Implementations such as reasoners can also be helpful. In particular: 7 / 28
ELIS – Multimedia Lab What about Semantics? The formal semantics of N3 is not defined(yet) Some implementations even differ! But: Documents like the W3C Team Submission describe the desired semantics Implementations such as reasoners can also be helpful. In particular: Cwm 7 / 28
ELIS – Multimedia Lab What about Semantics? The formal semantics of N3 is not defined(yet) Some implementations even differ! But: Documents like the W3C Team Submission describe the desired semantics Implementations such as reasoners can also be helpful. In particular: Cwm EYE 7 / 28
ELIS – Multimedia Lab What about Semantics? The formal semantics of N3 is not defined(yet) Some implementations even differ! But: Documents like the W3C Team Submission describe the desired semantics Implementations such as reasoners can also be helpful. In particular: Cwm EYE   We use all these as sources to define N3’s formal semantics 7 / 28
ELIS – Multimedia Lab Implicit Quantification Notation3 Logic Implicit Quantification Existentials Universals Formal Semantics 8 / 28
ELIS – Multimedia Lab What is implicit quantification? In N3 quantified variables can be expressed without explicitly stating the quantifier 9 / 28
ELIS – Multimedia Lab What is implicit quantification? In N3 quantified variables can be expressed without explicitly stating the quantifier Blank nodes _:x are existentially quantified variables 9 / 28
ELIS – Multimedia Lab What is implicit quantification? In N3 quantified variables can be expressed without explicitly stating the quantifier Blank nodes _:x are existentially quantified variables Variables beginning with a question mark ?x are universally quantified 9 / 28
ELIS – Multimedia Lab What is implicit quantification? In N3 quantified variables can be expressed without explicitly stating the quantifier Blank nodes _:x are existentially quantified variables Variables beginning with a question mark ?x are universally quantified But: What is the scope? 9 / 28
ELIS – Multimedia Lab Simple Examples _:x :knows :Socrates. 10 / 28
ELIS – Multimedia Lab Simple Examples _:x :knows :Socrates. → ∃x : knows(x, Socrates) 10 / 28
ELIS – Multimedia Lab Simple Examples _:x :knows :Socrates. → ∃x : knows(x, Socrates) ?x :knows :Socrates. 10 / 28
ELIS – Multimedia Lab Simple Examples _:x :knows :Socrates. → ∃x : knows(x, Socrates) ?x :knows :Socrates. → ∀x : knows(x, Socrates) 10 / 28
ELIS – Multimedia Lab Both types of variables ?x :loves _:y. 11 / 28
ELIS – Multimedia Lab Both types of variables ?x :loves _:y. ∀x∃y : loves(x, y) "Everybody loves someone." 11 / 28
ELIS – Multimedia Lab Both types of variables ?x :loves _:y. ∀x∃y : loves(x, y) "Everybody loves someone." or ∃y∀x : loves(x, y) "There is someone who is loved by everyone." 11 / 28
ELIS – Multimedia Lab Both types of variables ?x :loves _:y. ∀x∃y : loves(x, y) "Everybody loves someone." or ∃y∀x : loves(x, y) "There is someone who is loved by everyone." 11 / 28
ELIS – Multimedia Lab Both types of variables “If both universal and existential quantification are specified for the same formula, then the scope of the universal quantification is outside the scope of the existentials”. Source: W3C Team submission; cwm and EYE give the same result. 12 / 28
ELIS – Multimedia Lab Existentials _:x :says {_:x a :Mortal}. 13 / 28
ELIS – Multimedia Lab Existentials _:x :says {_:x a :Mortal}. ∃x : says(x, Mortal(x)) There is someone who says about himself that he is mortal. 13 / 28
ELIS – Multimedia Lab Existentials _:x :says {_:x a :Mortal}. ∃x : says(x, Mortal(x)) There is someone who says about himself that he is mortal. or ∃x1 : says(x, (∃x2 : Mortal(x2))) There is someone who says that someone is mortal. 13 / 28
ELIS – Multimedia Lab Existentials _:x :says {_:x a :Mortal}. ∃x : says(x, Mortal(x)) There is someone who says about himself that he is mortal. or ∃x1 : says(x, (∃x2 : Mortal(x2))) There is someone who says that someone is mortal. 13 / 28
ELIS – Multimedia Lab Existentials “When formulae are nested, _: blank nodes syntax [is] used to only identify blank node in the formula it occurs directly in. It is an arbitrary temporary name for a symbol which is existentially quantified within the current formula (not the whole file). They can only be used within a single formula, and not within nested formulae.” Source: W3C Team submission; cwm and EYE give the same result. 14 / 28
ELIS – Multimedia Lab Universals {{?x :p :a.} = {?x :q :b.}.} = {{?x :r :c.} = {?x :s :d.}.}. 15 / 28
ELIS – Multimedia Lab Universals {{?x :p :a.} = {?x :q :b.}.} = {{?x :r :c.} = {?x :s :d.}.}. (∀x1 : p(x1, a) → q(x1, b)) → (∀x2 : r(x2, c) → s(x2, d)) 15 / 28
ELIS – Multimedia Lab Universals {{?x :p :a.} = {?x :q :b.}.} = {{?x :r :c.} = {?x :s :d.}.}. (∀x1 : p(x1, a) → q(x1, b)) → (∀x2 : r(x2, c) → s(x2, d)) or ∀x : ((p(x, a) → q(x, b)) → (r(x, c) → s(x, d))) 15 / 28
ELIS – Multimedia Lab Universals {{?x :p :a.} = {?x :q :b.}.} = {{?x :r :c.} = {?x :s :d.}.}. (∀x1 : p(x1, a) → q(x1, b)) → (∀x2 : r(x2, c) → s(x2, d)) or ∀x : ((p(x, a) → q(x, b)) → (r(x, c) → s(x, d))) Here the reasoning results differ! EYECwm 15 / 28
ELIS – Multimedia Lab Who is right? 16 / 28
ELIS – Multimedia Lab Universals The team submission states: “Apart from the set of statements, a formula also has a set of URIs of symbols which are universally quantified, and a set of URIs of symbols which are existentially quantified. Variables are then in general symbols which have been quantified. There is a also a shorthand syntax ?x which is the same as :x except that it implies that x is universally quantified not in the formula but in its parent formula.” 17 / 28
ELIS – Multimedia Lab Universals Which is the parent? 18 / 28
ELIS – Multimedia Lab Universals Which is the parent? :Plato :says { :Socrates a Mortal. Formula }. Parent formula 18 / 28
ELIS – Multimedia Lab Universals Which is the parent? :Plato :says { :Socrates a Mortal. Formula }. Parent formula  The parent formula p of a formula f is the formula containing {f } as a component. 18 / 28
ELIS – Multimedia Lab Universals But: Universal quantification also counts for descendants 19 / 28
ELIS – Multimedia Lab Universals But: Universal quantification also counts for descendants {?x :p :a.}={ :s :q { ?x :r :b. Formula }. Parent formula }. Grandparent formula 19 / 28
ELIS – Multimedia Lab Universals But: Universal quantification also counts for descendants {?x :p :a.}={ :s :q { ?x :r :b. Formula }. Parent formula }. Grandparent formula Is interpreted as: ∀x : p(x, a) → q(s, r(x, b)) 19 / 28
ELIS – Multimedia Lab Universals But: Universal quantification also counts for descendants {?x :p :a.}={ :s :q { ?x :r :b. Formula }. Parent formula }. Grandparent formula Is interpreted as: ∀x : p(x, a) → q(s, r(x, b)) And not as ∀x1 : p(x1, a) → (∀x2 : q(s, r(x2, b))) 19 / 28
ELIS – Multimedia Lab Universals But: Universal quantification also counts for descendants {?x :p :a.}={ :s :q { ?x :r :b. Formula }. Parent formula }. Grandparent formula Is interpreted as: ∀x : p(x, a) → q(s, r(x, b)) And not as ∀x1 : p(x1, a) → (∀x2 : q(s, r(x2, b))) ((((((((((((((((((hhhhhhhhhhhhhhhhhh 19 / 28
ELIS – Multimedia Lab Formal Semantics Notation3 Logic Implicit Quantification Formal Semantics Handling variables N3 context 20 / 28
ELIS – Multimedia Lab Handling variables The scope of an existential variable is always only the formula it occurs in, not its descendant 21 / 28
ELIS – Multimedia Lab Handling variables The scope of an existential variable is always only the formula it occurs in, not its descendant The scope of a universal variable depends on its context, scoping is also valid on the descendants of a quantified formula 21 / 28
ELIS – Multimedia Lab Handling variables We define two ways to apply a substitution σ: 22 / 28
ELIS – Multimedia Lab Handling variables We define two ways to apply a substitution σ: 1. Component wise application σc: replace only direct components of a formula 22 / 28
ELIS – Multimedia Lab Handling variables We define two ways to apply a substitution σ: 1. Component wise application σc: replace only direct components of a formula 2. Total application σt: replace all direct components and nested components 22 / 28
ELIS – Multimedia Lab Handling variables For f = ?x :says {?x a :Mortal.}. and σ = {?x/:Socrates} 23 / 28
ELIS – Multimedia Lab Handling variables For f = ?x :says {?x a :Mortal.}. and σ = {?x/:Socrates} we obtain: f σc = :Socrates :says {?x a :Mortal.}. 23 / 28
ELIS – Multimedia Lab Handling variables For f = ?x :says {?x a :Mortal.}. and σ = {?x/:Socrates} we obtain: f σc = :Socrates :says {?x a :Mortal.}. and f σt = :Socrates :says {:Socrates a :Mortal.}. 23 / 28
ELIS – Multimedia Lab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: 24 / 28
ELIS – Multimedia Lab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. 24 / 28
ELIS – Multimedia Lab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. → nf (?x) = 1 24 / 28
ELIS – Multimedia Lab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. → nf (?x) = 1 f = ?x :p1 {?x :p2 :o2}. 24 / 28
ELIS – Multimedia Lab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. → nf (?x) = 1 f = ?x :p1 {?x :p2 :o2}. → nf (?x) = 1 24 / 28
ELIS – Multimedia Lab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. → nf (?x) = 1 f = ?x :p1 {?x :p2 :o2}. → nf (?x) = 1 f = ?y :p1 {?x :p2 :o2}. 24 / 28
ELIS – Multimedia Lab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. → nf (?x) = 1 f = ?x :p1 {?x :p2 :o2}. → nf (?x) = 1 f = ?y :p1 {?x :p2 :o2}. → nf (?x) = 2 24 / 28
ELIS – Multimedia Lab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. → nf (?x) = 1 f = ?x :p1 {?x :p2 :o2}. → nf (?x) = 1 f = ?y :p1 {?x :p2 :o2}. → nf (?x) = 2 f = ?y :p1 {?y :p2 {?x :p3 :o3}}. 24 / 28
ELIS – Multimedia Lab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. → nf (?x) = 1 f = ?x :p1 {?x :p2 :o2}. → nf (?x) = 1 f = ?y :p1 {?x :p2 :o2}. → nf (?x) = 2 f = ?y :p1 {?y :p2 {?x :p3 :o3}}. → nf (?x) = 3 24 / 28
ELIS – Multimedia Lab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. → nf (?x) = 1 f = ?x :p1 {?x :p2 :o2}. → nf (?x) = 1 f = ?y :p1 {?x :p2 :o2}. → nf (?x) = 2 f = ?y :p1 {?y :p2 {?x :p3 :o3}}. → nf (?x) = 3 We call a universal variable accessible in a formula f iff 0 nf(?x) ≤ 2 . 24 / 28
ELIS – Multimedia Lab Handling variables Consider { {?x :p :a.} = {?x :q :b.}. f11 } = {{?x :r :c.} = {?x :s :d.}. f12 }. f0 25 / 28
ELIS – Multimedia Lab Handling variables Consider { {?x :p :a.} = {?x :q :b.}. f11 } = {{?x :r :c.} = {?x :s :d.}. f12 }. f0 nf0 (?x) = 3 25 / 28
ELIS – Multimedia Lab Handling variables Consider { {?x :p :a.} = {?x :q :b.}. f11 } = {{?x :r :c.} = {?x :s :d.}. f12 }. f0 nf0 (?x) = 3 → ?x is not accessible in f0 25 / 28
ELIS – Multimedia Lab Handling variables Consider { {?x :p :a.} = {?x :q :b.}. f11 } = {{?x :r :c.} = {?x :s :d.}. f12 }. f0 nf0 (?x) = 3 → ?x is not accessible in f0 nf11 (?x) = 2 and nf12 (?x) = 2 25 / 28
ELIS – Multimedia Lab Handling variables Consider { {?x :p :a.} = {?x :q :b.}. f11 } = {{?x :r :c.} = {?x :s :d.}. f12 }. f0 nf0 (?x) = 3 → ?x is not accessible in f0 nf11 (?x) = 2 and nf12 (?x) = 2 → ?x is accessible in f11 and f12 25 / 28
ELIS – Multimedia Lab Handling variables Consider { {?x :p :a.} = {?x :q :b.}. f11 } = {{?x :r :c.} = {?x :s :d.}. f12 }. f0 nf0 (?x) = 3 → ?x is not accessible in f0 nf11 (?x) = 2 and nf12 (?x) = 2 → ?x is accessible in f11 and f12 Those are exactly the formulas where the two ?x are quantified: 25 / 28
ELIS – Multimedia Lab Handling variables Consider { {?x :p :a.} = {?x :q :b.}. f11 } = {{?x :r :c.} = {?x :s :d.}. f12 }. f0 nf0 (?x) = 3 → ?x is not accessible in f0 nf11 (?x) = 2 and nf12 (?x) = 2 → ?x is accessible in f11 and f12 Those are exactly the formulas where the two ?x are quantified: { {?x :p :a.} = {?x :q :b.}. }= { {?x :q :c.} = {?x :r :d.}. } (∀x1 : (p(x1, a) → q(x1, b))) → (∀x2 : (r(x2, c) → s(x2, d))) 25 / 28
ELIS – Multimedia Lab N3 context Our model definition is oriented on the RDF semantics with the following additions: 26 / 28
ELIS – Multimedia Lab N3 context Our model definition is oriented on the RDF semantics with the following additions: Ground implications have the usual first order meaning 26 / 28
ELIS – Multimedia Lab N3 context Our model definition is oriented on the RDF semantics with the following additions: Ground implications have the usual first order meaning Except if they occur in implications, graphs are handled as simple URIs 26 / 28
ELIS – Multimedia Lab N3 context Our model definition is oriented on the RDF semantics with the following additions: Ground implications have the usual first order meaning Except if they occur in implications, graphs are handled as simple URIs We add grounding steps for any formula f in the following order: 26 / 28
ELIS – Multimedia Lab N3 context Our model definition is oriented on the RDF semantics with the following additions: Ground implications have the usual first order meaning Except if they occur in implications, graphs are handled as simple URIs We add grounding steps for any formula f in the following order: 1. If f contains accessible universal variables, it is valid iff f σt is valid for every ground substitution σ for those variables. 26 / 28
ELIS – Multimedia Lab N3 context Our model definition is oriented on the RDF semantics with the following additions: Ground implications have the usual first order meaning Except if they occur in implications, graphs are handled as simple URIs We add grounding steps for any formula f in the following order: 1. If f contains accessible universal variables, it is valid iff f σt is valid for every ground substitution σ for those variables. 2. If f contains existentials on top level it is valid iff there exists a ground substitution σ for those variables such that f σc is valid. 26 / 28
ELIS – Multimedia Lab Notation3 Logic Implicit Quantification Formal Semantics 27 / 28
ELIS – Multimedia Lab Conclusion It is possible to define the semantics as in the team submission 28 / 28
ELIS – Multimedia Lab Conclusion It is possible to define the semantics as in the team submission It is difficult and rather unusual to define the scope of universals as it is proposed in the team submission 28 / 28
ELIS – Multimedia Lab Conclusion It is possible to define the semantics as in the team submission It is difficult and rather unusual to define the scope of universals as it is proposed in the team submission Implicit universal quantification could be handled easier, for example on formula level 28 / 28
ELIS – Multimedia Lab Conclusion It is possible to define the semantics as in the team submission It is difficult and rather unusual to define the scope of universals as it is proposed in the team submission Implicit universal quantification could be handled easier, for example on formula level Let’s simplify this! 28 / 28
ELIS – Multimedia Lab Example: Explicit quantification @forAll #x. @forSome #y. #x #loves #y . @forSome #y. @forAll #x. #x #loves #y . 29 / 28
ELIS – Multimedia Lab Example: Explicit quantification @forAll #x. @forSome #y. #x #loves #y . @forSome #y. @forAll #x. #x #loves #y . Have the same meaning: ∀x∃y : loves(x, y). 29 / 28
ELIS – Multimedia Lab Example: Variable of not? @forSome :y. :x :p :y. @forAll :x. :x :q :o. 30 / 28
ELIS – Multimedia Lab Example: Variable of not? @forSome :y. :x :p :y. @forAll :x. :x :q :o. Is the first :x quantified? 30 / 28

More Related Content

PDF
RuleML 2015: Ontology Reasoning using Rules in an eHealth Context
byRuleML
 
PDF
Irpb workshop
byKhalid Belhajjame
 
PDF
An introduction to Julia
byJiahao Chen
 
PDF
Linear Logic and Constructive Mathematics, after Shulman
byValeria de Paiva
 
PPT
NeXML
byRutger Vos
 
PDF
Genomics data analysis in Julia
byJiahao Chen
 
PDF
Benchmarking Linear Logic Proofs
byValeria de Paiva
 
PDF
Fun with Constructive Modalities
byValeria de Paiva
 
RuleML 2015: Ontology Reasoning using Rules in an eHealth Context
byRuleML
 
Irpb workshop
byKhalid Belhajjame
 
An introduction to Julia
byJiahao Chen
 
Linear Logic and Constructive Mathematics, after Shulman
byValeria de Paiva
 
NeXML
byRutger Vos
 
Genomics data analysis in Julia
byJiahao Chen
 
Benchmarking Linear Logic Proofs
byValeria de Paiva
 
Fun with Constructive Modalities
byValeria de Paiva
 

What's hot

PDF
A Julia package for iterative SVDs with applications to genomics data analysis
byJiahao Chen
 
PDF
Constructive Modal and Linear Logics
byValeria de Paiva
 
PDF
Categorical Semantics for Explicit Substitutions
byValeria de Paiva
 
PPT
A Distributed Architecture System for Recognizing Textual Entailment
byFaculty of Computer Science
 
PDF
Dialectica Categories and Petri Nets
byValeria de Paiva
 
PDF
Relevant Dialectica Categories
byValeria de Paiva
 
PDF
Dialectica Categories for the Lambek Calculus
byValeria de Paiva
 
PDF
Natural Language Inference for Humans
byValeria de Paiva
 
PDF
Going Without: a modality and its role
byValeria de Paiva
 
A Julia package for iterative SVDs with applications to genomics data analysis
byJiahao Chen
 
Constructive Modal and Linear Logics
byValeria de Paiva
 
Categorical Semantics for Explicit Substitutions
byValeria de Paiva
 
A Distributed Architecture System for Recognizing Textual Entailment
byFaculty of Computer Science
 
Dialectica Categories and Petri Nets
byValeria de Paiva
 
Relevant Dialectica Categories
byValeria de Paiva
 
Dialectica Categories for the Lambek Calculus
byValeria de Paiva
 
Natural Language Inference for Humans
byValeria de Paiva
 
Going Without: a modality and its role
byValeria de Paiva
 

Viewers also liked

PDF
RuleML2015: How to combine event stream reasoning with transactions for the...
byRuleML
 
DOCX
History of Induction and Recursion B
byDamien MacFarland
 
PPT
Induction and Decision Tree Learning (Part 1)
bybutest
 
PDF
RuleML 2015: When Processes Rule Events
byRuleML
 
PDF
11X1 T14 08 mathematical induction 1 (2011)
byNigel Simmons
 
PDF
Challenge@RuleML2015 Transformation and aggregation preprocessing for top-k r...
byRuleML
 
PDF
Challenge@rule ml2015 rule based recommender systems for the Web of Data
byRuleML
 
PDF
Iteration, induction, and recursion
byMohammed Hussein
 
PDF
Math induction principle (slides)
byIIUM
 
PPSX
Mathematical induction
bysonia -
 
PPT
Mathematical induction
bySman Abbasi
 
PPTX
5.4 mathematical induction
bymath260
 
PPTX
Principle of mathematical induction
byKriti Varshney
 
PPT
mathematical induction
byankush_kumar
 
RuleML2015: How to combine event stream reasoning with transactions for the...
byRuleML
 
History of Induction and Recursion B
byDamien MacFarland
 
Induction and Decision Tree Learning (Part 1)
bybutest
 
RuleML 2015: When Processes Rule Events
byRuleML
 
11X1 T14 08 mathematical induction 1 (2011)
byNigel Simmons
 
Challenge@RuleML2015 Transformation and aggregation preprocessing for top-k r...
byRuleML
 
Challenge@rule ml2015 rule based recommender systems for the Web of Data
byRuleML
 
Iteration, induction, and recursion
byMohammed Hussein
 
Math induction principle (slides)
byIIUM
 
Mathematical induction
bysonia -
 
Mathematical induction
bySman Abbasi
 
5.4 mathematical induction
bymath260
 
Principle of mathematical induction
byKriti Varshney
 
mathematical induction
byankush_kumar
 

Similar to RuleML 2015: Semantics of Notation3 Logic: A Solution for Implicit Quantification

PDF
RuleML2015: Semantics of Notation3 Logic: A Solution for Implicit Quantifica...
byRuleML
 
PPTX
Ai quantifiers
byTayyaba Jabeen
 
PPTX
PredicateLogic.pptx
bysanthosh sriprada
 
PPT
PredicateLogic (1).ppt
bykeerthana592112
 
PDF
I am kind of confused about quantifiers. I am not sure how to transl.pdf
byAMITPANCHAL154
 
PPT
Jarrar.lecture notes.aai.2011s.descriptionlogic
byPalGov
 
PPT
Propositional Logic and Pridicate logic
byRoorkee College of Engineering, Roorkee
 
PPT
Predicate calculus
byRajendran
 
PPT
Semantics
byMohammed Al-Meqdad
 
PPTX
Module_5_1.pptx
byDrKalaavathiBuvanesh
 
PPTX
Knowledge Representation in Artificial Intelligence
byMehak533057
 
PDF
Point-free foundation of Mathematics
byMarco Benini
 
PDF
Truth, deduction, computation lecture b
byVlad Patryshev
 
PPT
Logic
byFlora Mae Angtud-Galenzoga
 
PPT
PROPOSISTION LOGIC IN ARTIFICIAL INTELLIGENCE
byRaghavendraPrasad179187
 
PDF
AI Lesson 11
byAssistant Professor
 
PPTX
Introduction of predicate logics
bychauhankapil
 
PPT
Ai 02
byShailesh Singh
 
PDF
Formal Logic - Lesson 8 - Predicates and Quantifiers
byLaguna State Polytechnic University
 
PDF
Formal languages
byVestforsk.no
 
RuleML2015: Semantics of Notation3 Logic: A Solution for Implicit Quantifica...
byRuleML
 
Ai quantifiers
byTayyaba Jabeen
 
PredicateLogic.pptx
bysanthosh sriprada
 
PredicateLogic (1).ppt
bykeerthana592112
 
I am kind of confused about quantifiers. I am not sure how to transl.pdf
byAMITPANCHAL154
 
Jarrar.lecture notes.aai.2011s.descriptionlogic
byPalGov
 
Propositional Logic and Pridicate logic
byRoorkee College of Engineering, Roorkee
 
Predicate calculus
byRajendran
 
Semantics
byMohammed Al-Meqdad
 
Module_5_1.pptx
byDrKalaavathiBuvanesh
 
Knowledge Representation in Artificial Intelligence
byMehak533057
 
Point-free foundation of Mathematics
byMarco Benini
 
Truth, deduction, computation lecture b
byVlad Patryshev
 
Logic
byFlora Mae Angtud-Galenzoga
 
PROPOSISTION LOGIC IN ARTIFICIAL INTELLIGENCE
byRaghavendraPrasad179187
 
AI Lesson 11
byAssistant Professor
 
Introduction of predicate logics
bychauhankapil
 
Ai 02
byShailesh Singh
 
Formal Logic - Lesson 8 - Predicates and Quantifiers
byLaguna State Polytechnic University
 
Formal languages
byVestforsk.no
 

More from RuleML

PDF
Aggregates in Recursion: Issues and Solutions
byRuleML
 
PDF
A software agent controlling 2 robot arms in co-operating concurrent tasks
byRuleML
 
PDF
Port Clearance Rules in PSOA RuleML: From Controlled-English Regulation to Ob...
byRuleML
 
PDF
Challenge@RuleML2015 Developing Situation-Aware Applications for Disaster Man...
byRuleML
 
PDF
Rule Generalization Strategies in Incremental Learning of Disjunctive Concepts
byRuleML
 
PDF
RuleML 2015 Constraint Handling Rules - What Else?
byRuleML
 
PDF
RuleML2015 The Herbrand Manifesto - Thinking Inside the Box
byRuleML
 
PDF
RuleML2015 PSOA RuleML: Integrated Object-Relational Data and Rules
byRuleML
 
PDF
Industry@RuleML2015: Norwegian State of Estate A Reporting Service for the St...
byRuleML
 
PDF
A Service for Improving the Assignments of Common Agriculture Policy Funds to...
byRuleML
 
PDF
Datalog+-Track Introduction & Reasoning on UML Class Diagrams via Datalog+-
byRuleML
 
PDF
RuleML2015: Binary Frontier-guarded ASP with Function Symbols
byRuleML
 
PDF
RuleML2015: API4KP Metamodel: A Meta-API for Heterogeneous Knowledge Platforms
byRuleML
 
PDF
RuleML2015: Rule-Based Exploration of Structured Data in the Browser
byRuleML
 
PDF
RuleML2015: Ontology-Based Multidimensional Contexts with Applications to Qua...
byRuleML
 
PDF
RuleML2015: Compact representation of conditional probability for rule-based...
byRuleML
 
PDF
RuleML2015: Learning Characteristic Rules in Geographic Information Systems
byRuleML
 
PDF
RuleML2015: Using Substitutive Itemset Mining Framework for Finding Synonymou...
byRuleML
 
PDF
RuleML2015: User Extensible System to Identify Problems in OWL Ontologies and...
byRuleML
 
PDF
RuleML2015: Representing Flexible Role-Based Access Control Policies Using Ob...
byRuleML
 
Aggregates in Recursion: Issues and Solutions
byRuleML
 
A software agent controlling 2 robot arms in co-operating concurrent tasks
byRuleML
 
Port Clearance Rules in PSOA RuleML: From Controlled-English Regulation to Ob...
byRuleML
 
Challenge@RuleML2015 Developing Situation-Aware Applications for Disaster Man...
byRuleML
 
Rule Generalization Strategies in Incremental Learning of Disjunctive Concepts
byRuleML
 
RuleML 2015 Constraint Handling Rules - What Else?
byRuleML
 
RuleML2015 The Herbrand Manifesto - Thinking Inside the Box
byRuleML
 
RuleML2015 PSOA RuleML: Integrated Object-Relational Data and Rules
byRuleML
 
Industry@RuleML2015: Norwegian State of Estate A Reporting Service for the St...
byRuleML
 
A Service for Improving the Assignments of Common Agriculture Policy Funds to...
byRuleML
 
Datalog+-Track Introduction & Reasoning on UML Class Diagrams via Datalog+-
byRuleML
 
RuleML2015: Binary Frontier-guarded ASP with Function Symbols
byRuleML
 
RuleML2015: API4KP Metamodel: A Meta-API for Heterogeneous Knowledge Platforms
byRuleML
 
RuleML2015: Rule-Based Exploration of Structured Data in the Browser
byRuleML
 
RuleML2015: Ontology-Based Multidimensional Contexts with Applications to Qua...
byRuleML
 
RuleML2015: Compact representation of conditional probability for rule-based...
byRuleML
 
RuleML2015: Learning Characteristic Rules in Geographic Information Systems
byRuleML
 
RuleML2015: Using Substitutive Itemset Mining Framework for Finding Synonymou...
byRuleML
 
RuleML2015: User Extensible System to Identify Problems in OWL Ontologies and...
byRuleML
 
RuleML2015: Representing Flexible Role-Based Access Control Policies Using Ob...
byRuleML
 

Recently uploaded

PDF
Introduction__to_Algae_Detailed.pptx.pdf
byjayapriya99574
 
PDF
Quantum Tunneling quantum tunneling ppt
byByomakeshBiswal1
 
PPTX
AN OVERVIEW OF APPLIED PHYCOLOGY. pptx .
byswathin2411
 
PDF
Economically important of microalgae ...
byrkaviyadharshini555
 
PDF
goodfoodscience@gfi.org
byThe Good Food Institute
 
PPT
Bacterial gene for crop improvement plant.ppt
bytarun23142002
 
PPTX
Recombination(Introduction, Homologous recombination, Site specific recombina...
byRashmiMG2
 
PPTX
Principle and Applications of pH Meter and Spectrophotometer.pptx
byDr Showkat Ahmad Wani
 
PPTX
Learn Human IL-6R ELISA Kit in 3 minutes
byorder29
 
PPTX
General characteristics and Classification of Protista .pptx
byJamakala Obaiah
 
PDF
DISTRIBUTION OF ALGAE ( Fresh water, Marine Water and Brackish Water algae)
bydharshinisampath6
 
PPTX
chromosomal abnormalities in humans PPT .pptx
byRachanaTripathi6
 
PPTX
Process of Reproduction-in-Protists.pptx
byJamakala Obaiah
 
PPTX
Dorothy Crowfoot Hodgkin_ A Pioneer of Science.pptx
bysophiements
 
PDF
invertebrates-150828165241-lva1-app6892.pdf
bylmuller1
 
PPT
Biosensors and their Applications agriculture.ppt
bytarun23142002
 
PPTX
"vaccine components/ingredients. Powerpoint
byEhsanJan3
 
PPTX
Curtin-Hammet Principle and Winstein-Holness Equation.pptx
bySocratesM3
 
PPTX
Raceway ponds - Mixotrophic and heterotrophic cultivation of microalgae _ ppt
byNandhiniV90
 
PDF
Cytoskeleton- it's different types and Cytodifferentiation
byNistarini College, Purulia (W.B) India
 
Introduction__to_Algae_Detailed.pptx.pdf
byjayapriya99574
 
Quantum Tunneling quantum tunneling ppt
byByomakeshBiswal1
 
AN OVERVIEW OF APPLIED PHYCOLOGY. pptx .
byswathin2411
 
Economically important of microalgae ...
byrkaviyadharshini555
 
goodfoodscience@gfi.org
byThe Good Food Institute
 
Bacterial gene for crop improvement plant.ppt
bytarun23142002
 
Recombination(Introduction, Homologous recombination, Site specific recombina...
byRashmiMG2
 
Principle and Applications of pH Meter and Spectrophotometer.pptx
byDr Showkat Ahmad Wani
 
Learn Human IL-6R ELISA Kit in 3 minutes
byorder29
 
General characteristics and Classification of Protista .pptx
byJamakala Obaiah
 
DISTRIBUTION OF ALGAE ( Fresh water, Marine Water and Brackish Water algae)
bydharshinisampath6
 
chromosomal abnormalities in humans PPT .pptx
byRachanaTripathi6
 
Process of Reproduction-in-Protists.pptx
byJamakala Obaiah
 
Dorothy Crowfoot Hodgkin_ A Pioneer of Science.pptx
bysophiements
 
invertebrates-150828165241-lva1-app6892.pdf
bylmuller1
 
Biosensors and their Applications agriculture.ppt
bytarun23142002
 
"vaccine components/ingredients. Powerpoint
byEhsanJan3
 
Curtin-Hammet Principle and Winstein-Holness Equation.pptx
bySocratesM3
 
Raceway ponds - Mixotrophic and heterotrophic cultivation of microalgae _ ppt
byNandhiniV90
 
Cytoskeleton- it's different types and Cytodifferentiation
byNistarini College, Purulia (W.B) India
 

RuleML 2015: Semantics of Notation3 Logic: A Solution for Implicit Quantification

  • 1.
    ELIS – MultimediaLab Semantics of Notation3 Logic: A solution for implicit quantification Dörthe Arndt, Ruben Verborgh, Jos De Roo, Hong Sun, Erik Mannens, and Rik Van De Walle Multimedia Lab, Ghent University - iMinds, Belgium Agfa Healthcare - Ghent, Belgium RuleML 2015, Berlin, August 04, 2015 1 / 28
  • 2.
    ELIS – MultimediaLab Outline Notation3 Logic Implicit Quantification Formal Semantics 2 / 28
  • 3.
    ELIS – MultimediaLab Notation3 Logic Notation3 Logic What is Notation3 Logic? Syntax Semantics Implicit Quantification Formal Semantics 3 / 28
  • 4.
    ELIS – MultimediaLab What is Notation3 Logic? A rule logic for the Semantic Web 4 / 28
  • 5.
    ELIS – MultimediaLab What is Notation3 Logic? A rule logic for the Semantic Web Invented by Tim Berners-Lee and Dan Connolly (∼2005) 4 / 28
  • 6.
    ELIS – MultimediaLab What is Notation3 Logic? A rule logic for the Semantic Web Invented by Tim Berners-Lee and Dan Connolly (∼2005) Superset of RDF/Turtle 4 / 28
  • 7.
    ELIS – MultimediaLab Syntax 5 / 28
  • 8.
    ELIS – MultimediaLab Syntax Simple Turtle triples: 5 / 28
  • 9.
    ELIS – MultimediaLab Syntax Simple Turtle triples: :Socrates a :Man. 5 / 28
  • 10.
    ELIS – MultimediaLab Syntax Simple Turtle triples: :Socrates a :Man. Rules: 5 / 28
  • 11.
    ELIS – MultimediaLab Syntax Simple Turtle triples: :Socrates a :Man. Rules: {:Socrates a :Man.} => {:Socrates a :Mortal.}. 5 / 28
  • 12.
    ELIS – MultimediaLab Syntax Statements about formulas: 6 / 28
  • 13.
    ELIS – MultimediaLab Syntax Statements about formulas: :Plato :says {:Socrates a Mortal.}. 6 / 28
  • 14.
    ELIS – MultimediaLab Syntax Statements about formulas: :Plato :says {:Socrates a Mortal.}. Use of (quantified) variables: 6 / 28
  • 15.
    ELIS – MultimediaLab Syntax Statements about formulas: :Plato :says {:Socrates a Mortal.}. Use of (quantified) variables: :Plato :knows _:x. _:x a :Man. 6 / 28
  • 16.
    ELIS – MultimediaLab Syntax Statements about formulas: :Plato :says {:Socrates a Mortal.}. Use of (quantified) variables: :Plato :knows _:x. _:x a :Man. {?x a :Man.}=>{?x a :Mortal.}. 6 / 28
  • 17.
    ELIS – MultimediaLab What about Semantics? The formal semantics of N3 is not defined 7 / 28
  • 18.
    ELIS – MultimediaLab What about Semantics? The formal semantics of N3 is not defined(yet) 7 / 28
  • 19.
    ELIS – MultimediaLab What about Semantics? The formal semantics of N3 is not defined(yet) Some implementations even differ! 7 / 28
  • 20.
    ELIS – MultimediaLab What about Semantics? The formal semantics of N3 is not defined(yet) Some implementations even differ! But: 7 / 28
  • 21.
    ELIS – MultimediaLab What about Semantics? The formal semantics of N3 is not defined(yet) Some implementations even differ! But: Documents like the W3C Team Submission describe the desired semantics 7 / 28
  • 22.
    ELIS – MultimediaLab What about Semantics? The formal semantics of N3 is not defined(yet) Some implementations even differ! But: Documents like the W3C Team Submission describe the desired semantics Implementations such as reasoners can also be helpful. In particular: 7 / 28
  • 23.
    ELIS – MultimediaLab What about Semantics? The formal semantics of N3 is not defined(yet) Some implementations even differ! But: Documents like the W3C Team Submission describe the desired semantics Implementations such as reasoners can also be helpful. In particular: Cwm 7 / 28
  • 24.
    ELIS – MultimediaLab What about Semantics? The formal semantics of N3 is not defined(yet) Some implementations even differ! But: Documents like the W3C Team Submission describe the desired semantics Implementations such as reasoners can also be helpful. In particular: Cwm EYE 7 / 28
  • 25.
    ELIS – MultimediaLab What about Semantics? The formal semantics of N3 is not defined(yet) Some implementations even differ! But: Documents like the W3C Team Submission describe the desired semantics Implementations such as reasoners can also be helpful. In particular: Cwm EYE   We use all these as sources to define N3’s formal semantics 7 / 28
  • 26.
    ELIS – MultimediaLab Implicit Quantification Notation3 Logic Implicit Quantification Existentials Universals Formal Semantics 8 / 28
  • 27.
    ELIS – MultimediaLab What is implicit quantification? In N3 quantified variables can be expressed without explicitly stating the quantifier 9 / 28
  • 28.
    ELIS – MultimediaLab What is implicit quantification? In N3 quantified variables can be expressed without explicitly stating the quantifier Blank nodes _:x are existentially quantified variables 9 / 28
  • 29.
    ELIS – MultimediaLab What is implicit quantification? In N3 quantified variables can be expressed without explicitly stating the quantifier Blank nodes _:x are existentially quantified variables Variables beginning with a question mark ?x are universally quantified 9 / 28
  • 30.
    ELIS – MultimediaLab What is implicit quantification? In N3 quantified variables can be expressed without explicitly stating the quantifier Blank nodes _:x are existentially quantified variables Variables beginning with a question mark ?x are universally quantified But: What is the scope? 9 / 28
  • 31.
    ELIS – MultimediaLab Simple Examples _:x :knows :Socrates. 10 / 28
  • 32.
    ELIS – MultimediaLab Simple Examples _:x :knows :Socrates. → ∃x : knows(x, Socrates) 10 / 28
  • 33.
    ELIS – MultimediaLab Simple Examples _:x :knows :Socrates. → ∃x : knows(x, Socrates) ?x :knows :Socrates. 10 / 28
  • 34.
    ELIS – MultimediaLab Simple Examples _:x :knows :Socrates. → ∃x : knows(x, Socrates) ?x :knows :Socrates. → ∀x : knows(x, Socrates) 10 / 28
  • 35.
    ELIS – MultimediaLab Both types of variables ?x :loves _:y. 11 / 28
  • 36.
    ELIS – MultimediaLab Both types of variables ?x :loves _:y. ∀x∃y : loves(x, y) "Everybody loves someone." 11 / 28
  • 37.
    ELIS – MultimediaLab Both types of variables ?x :loves _:y. ∀x∃y : loves(x, y) "Everybody loves someone." or ∃y∀x : loves(x, y) "There is someone who is loved by everyone." 11 / 28
  • 38.
    ELIS – MultimediaLab Both types of variables ?x :loves _:y. ∀x∃y : loves(x, y) "Everybody loves someone." or ∃y∀x : loves(x, y) "There is someone who is loved by everyone." 11 / 28
  • 39.
    ELIS – MultimediaLab Both types of variables “If both universal and existential quantification are specified for the same formula, then the scope of the universal quantification is outside the scope of the existentials”. Source: W3C Team submission; cwm and EYE give the same result. 12 / 28
  • 40.
    ELIS – MultimediaLab Existentials _:x :says {_:x a :Mortal}. 13 / 28
  • 41.
    ELIS – MultimediaLab Existentials _:x :says {_:x a :Mortal}. ∃x : says(x, Mortal(x)) There is someone who says about himself that he is mortal. 13 / 28
  • 42.
    ELIS – MultimediaLab Existentials _:x :says {_:x a :Mortal}. ∃x : says(x, Mortal(x)) There is someone who says about himself that he is mortal. or ∃x1 : says(x, (∃x2 : Mortal(x2))) There is someone who says that someone is mortal. 13 / 28
  • 43.
    ELIS – MultimediaLab Existentials _:x :says {_:x a :Mortal}. ∃x : says(x, Mortal(x)) There is someone who says about himself that he is mortal. or ∃x1 : says(x, (∃x2 : Mortal(x2))) There is someone who says that someone is mortal. 13 / 28
  • 44.
    ELIS – MultimediaLab Existentials “When formulae are nested, _: blank nodes syntax [is] used to only identify blank node in the formula it occurs directly in. It is an arbitrary temporary name for a symbol which is existentially quantified within the current formula (not the whole file). They can only be used within a single formula, and not within nested formulae.” Source: W3C Team submission; cwm and EYE give the same result. 14 / 28
  • 45.
    ELIS – MultimediaLab Universals {{?x :p :a.} = {?x :q :b.}.} = {{?x :r :c.} = {?x :s :d.}.}. 15 / 28
  • 46.
    ELIS – MultimediaLab Universals {{?x :p :a.} = {?x :q :b.}.} = {{?x :r :c.} = {?x :s :d.}.}. (∀x1 : p(x1, a) → q(x1, b)) → (∀x2 : r(x2, c) → s(x2, d)) 15 / 28
  • 47.
    ELIS – MultimediaLab Universals {{?x :p :a.} = {?x :q :b.}.} = {{?x :r :c.} = {?x :s :d.}.}. (∀x1 : p(x1, a) → q(x1, b)) → (∀x2 : r(x2, c) → s(x2, d)) or ∀x : ((p(x, a) → q(x, b)) → (r(x, c) → s(x, d))) 15 / 28
  • 48.
    ELIS – MultimediaLab Universals {{?x :p :a.} = {?x :q :b.}.} = {{?x :r :c.} = {?x :s :d.}.}. (∀x1 : p(x1, a) → q(x1, b)) → (∀x2 : r(x2, c) → s(x2, d)) or ∀x : ((p(x, a) → q(x, b)) → (r(x, c) → s(x, d))) Here the reasoning results differ! EYECwm 15 / 28
  • 49.
    ELIS – MultimediaLab Who is right? 16 / 28
  • 50.
    ELIS – MultimediaLab Universals The team submission states: “Apart from the set of statements, a formula also has a set of URIs of symbols which are universally quantified, and a set of URIs of symbols which are existentially quantified. Variables are then in general symbols which have been quantified. There is a also a shorthand syntax ?x which is the same as :x except that it implies that x is universally quantified not in the formula but in its parent formula.” 17 / 28
  • 51.
    ELIS – MultimediaLab Universals Which is the parent? 18 / 28
  • 52.
    ELIS – MultimediaLab Universals Which is the parent? :Plato :says { :Socrates a Mortal. Formula }. Parent formula 18 / 28
  • 53.
    ELIS – MultimediaLab Universals Which is the parent? :Plato :says { :Socrates a Mortal. Formula }. Parent formula  The parent formula p of a formula f is the formula containing {f } as a component. 18 / 28
  • 54.
    ELIS – MultimediaLab Universals But: Universal quantification also counts for descendants 19 / 28
  • 55.
    ELIS – MultimediaLab Universals But: Universal quantification also counts for descendants {?x :p :a.}={ :s :q { ?x :r :b. Formula }. Parent formula }. Grandparent formula 19 / 28
  • 56.
    ELIS – MultimediaLab Universals But: Universal quantification also counts for descendants {?x :p :a.}={ :s :q { ?x :r :b. Formula }. Parent formula }. Grandparent formula Is interpreted as: ∀x : p(x, a) → q(s, r(x, b)) 19 / 28
  • 57.
    ELIS – MultimediaLab Universals But: Universal quantification also counts for descendants {?x :p :a.}={ :s :q { ?x :r :b. Formula }. Parent formula }. Grandparent formula Is interpreted as: ∀x : p(x, a) → q(s, r(x, b)) And not as ∀x1 : p(x1, a) → (∀x2 : q(s, r(x2, b))) 19 / 28
  • 58.
    ELIS – MultimediaLab Universals But: Universal quantification also counts for descendants {?x :p :a.}={ :s :q { ?x :r :b. Formula }. Parent formula }. Grandparent formula Is interpreted as: ∀x : p(x, a) → q(s, r(x, b)) And not as ∀x1 : p(x1, a) → (∀x2 : q(s, r(x2, b))) ((((((((((((((((((hhhhhhhhhhhhhhhhhh 19 / 28
  • 59.
    ELIS – MultimediaLab Formal Semantics Notation3 Logic Implicit Quantification Formal Semantics Handling variables N3 context 20 / 28
  • 60.
    ELIS – MultimediaLab Handling variables The scope of an existential variable is always only the formula it occurs in, not its descendant 21 / 28
  • 61.
    ELIS – MultimediaLab Handling variables The scope of an existential variable is always only the formula it occurs in, not its descendant The scope of a universal variable depends on its context, scoping is also valid on the descendants of a quantified formula 21 / 28
  • 62.
    ELIS – MultimediaLab Handling variables We define two ways to apply a substitution σ: 22 / 28
  • 63.
    ELIS – MultimediaLab Handling variables We define two ways to apply a substitution σ: 1. Component wise application σc: replace only direct components of a formula 22 / 28
  • 64.
    ELIS – MultimediaLab Handling variables We define two ways to apply a substitution σ: 1. Component wise application σc: replace only direct components of a formula 2. Total application σt: replace all direct components and nested components 22 / 28
  • 65.
    ELIS – MultimediaLab Handling variables For f = ?x :says {?x a :Mortal.}. and σ = {?x/:Socrates} 23 / 28
  • 66.
    ELIS – MultimediaLab Handling variables For f = ?x :says {?x a :Mortal.}. and σ = {?x/:Socrates} we obtain: f σc = :Socrates :says {?x a :Mortal.}. 23 / 28
  • 67.
    ELIS – MultimediaLab Handling variables For f = ?x :says {?x a :Mortal.}. and σ = {?x/:Socrates} we obtain: f σc = :Socrates :says {?x a :Mortal.}. and f σt = :Socrates :says {:Socrates a :Mortal.}. 23 / 28
  • 68.
    ELIS – MultimediaLab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: 24 / 28
  • 69.
    ELIS – MultimediaLab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. 24 / 28
  • 70.
    ELIS – MultimediaLab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. → nf (?x) = 1 24 / 28
  • 71.
    ELIS – MultimediaLab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. → nf (?x) = 1 f = ?x :p1 {?x :p2 :o2}. 24 / 28
  • 72.
    ELIS – MultimediaLab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. → nf (?x) = 1 f = ?x :p1 {?x :p2 :o2}. → nf (?x) = 1 24 / 28
  • 73.
    ELIS – MultimediaLab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. → nf (?x) = 1 f = ?x :p1 {?x :p2 :o2}. → nf (?x) = 1 f = ?y :p1 {?x :p2 :o2}. 24 / 28
  • 74.
    ELIS – MultimediaLab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. → nf (?x) = 1 f = ?x :p1 {?x :p2 :o2}. → nf (?x) = 1 f = ?y :p1 {?x :p2 :o2}. → nf (?x) = 2 24 / 28
  • 75.
    ELIS – MultimediaLab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. → nf (?x) = 1 f = ?x :p1 {?x :p2 :o2}. → nf (?x) = 1 f = ?y :p1 {?x :p2 :o2}. → nf (?x) = 2 f = ?y :p1 {?y :p2 {?x :p3 :o3}}. 24 / 28
  • 76.
    ELIS – MultimediaLab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. → nf (?x) = 1 f = ?x :p1 {?x :p2 :o2}. → nf (?x) = 1 f = ?y :p1 {?x :p2 :o2}. → nf (?x) = 2 f = ?y :p1 {?y :p2 {?x :p3 :o3}}. → nf (?x) = 3 24 / 28
  • 77.
    ELIS – MultimediaLab Handling variables To cope with the behavior of universal quantification we define the nesting level nf(?x) of a variable ?x in a formula f as the lowest level, counted from above, where ?x can be found: f = ?x :p :o. → nf (?x) = 1 f = ?x :p1 {?x :p2 :o2}. → nf (?x) = 1 f = ?y :p1 {?x :p2 :o2}. → nf (?x) = 2 f = ?y :p1 {?y :p2 {?x :p3 :o3}}. → nf (?x) = 3 We call a universal variable accessible in a formula f iff 0 nf(?x) ≤ 2 . 24 / 28
  • 78.
    ELIS – MultimediaLab Handling variables Consider { {?x :p :a.} = {?x :q :b.}. f11 } = {{?x :r :c.} = {?x :s :d.}. f12 }. f0 25 / 28
  • 79.
    ELIS – MultimediaLab Handling variables Consider { {?x :p :a.} = {?x :q :b.}. f11 } = {{?x :r :c.} = {?x :s :d.}. f12 }. f0 nf0 (?x) = 3 25 / 28
  • 80.
    ELIS – MultimediaLab Handling variables Consider { {?x :p :a.} = {?x :q :b.}. f11 } = {{?x :r :c.} = {?x :s :d.}. f12 }. f0 nf0 (?x) = 3 → ?x is not accessible in f0 25 / 28
  • 81.
    ELIS – MultimediaLab Handling variables Consider { {?x :p :a.} = {?x :q :b.}. f11 } = {{?x :r :c.} = {?x :s :d.}. f12 }. f0 nf0 (?x) = 3 → ?x is not accessible in f0 nf11 (?x) = 2 and nf12 (?x) = 2 25 / 28
  • 82.
    ELIS – MultimediaLab Handling variables Consider { {?x :p :a.} = {?x :q :b.}. f11 } = {{?x :r :c.} = {?x :s :d.}. f12 }. f0 nf0 (?x) = 3 → ?x is not accessible in f0 nf11 (?x) = 2 and nf12 (?x) = 2 → ?x is accessible in f11 and f12 25 / 28
  • 83.
    ELIS – MultimediaLab Handling variables Consider { {?x :p :a.} = {?x :q :b.}. f11 } = {{?x :r :c.} = {?x :s :d.}. f12 }. f0 nf0 (?x) = 3 → ?x is not accessible in f0 nf11 (?x) = 2 and nf12 (?x) = 2 → ?x is accessible in f11 and f12 Those are exactly the formulas where the two ?x are quantified: 25 / 28
  • 84.
    ELIS – MultimediaLab Handling variables Consider { {?x :p :a.} = {?x :q :b.}. f11 } = {{?x :r :c.} = {?x :s :d.}. f12 }. f0 nf0 (?x) = 3 → ?x is not accessible in f0 nf11 (?x) = 2 and nf12 (?x) = 2 → ?x is accessible in f11 and f12 Those are exactly the formulas where the two ?x are quantified: { {?x :p :a.} = {?x :q :b.}. }= { {?x :q :c.} = {?x :r :d.}. } (∀x1 : (p(x1, a) → q(x1, b))) → (∀x2 : (r(x2, c) → s(x2, d))) 25 / 28
  • 85.
    ELIS – MultimediaLab N3 context Our model definition is oriented on the RDF semantics with the following additions: 26 / 28
  • 86.
    ELIS – MultimediaLab N3 context Our model definition is oriented on the RDF semantics with the following additions: Ground implications have the usual first order meaning 26 / 28
  • 87.
    ELIS – MultimediaLab N3 context Our model definition is oriented on the RDF semantics with the following additions: Ground implications have the usual first order meaning Except if they occur in implications, graphs are handled as simple URIs 26 / 28
  • 88.
    ELIS – MultimediaLab N3 context Our model definition is oriented on the RDF semantics with the following additions: Ground implications have the usual first order meaning Except if they occur in implications, graphs are handled as simple URIs We add grounding steps for any formula f in the following order: 26 / 28
  • 89.
    ELIS – MultimediaLab N3 context Our model definition is oriented on the RDF semantics with the following additions: Ground implications have the usual first order meaning Except if they occur in implications, graphs are handled as simple URIs We add grounding steps for any formula f in the following order: 1. If f contains accessible universal variables, it is valid iff f σt is valid for every ground substitution σ for those variables. 26 / 28
  • 90.
    ELIS – MultimediaLab N3 context Our model definition is oriented on the RDF semantics with the following additions: Ground implications have the usual first order meaning Except if they occur in implications, graphs are handled as simple URIs We add grounding steps for any formula f in the following order: 1. If f contains accessible universal variables, it is valid iff f σt is valid for every ground substitution σ for those variables. 2. If f contains existentials on top level it is valid iff there exists a ground substitution σ for those variables such that f σc is valid. 26 / 28
  • 91.
    ELIS – MultimediaLab Notation3 Logic Implicit Quantification Formal Semantics 27 / 28
  • 92.
    ELIS – MultimediaLab Conclusion It is possible to define the semantics as in the team submission 28 / 28
  • 93.
    ELIS – MultimediaLab Conclusion It is possible to define the semantics as in the team submission It is difficult and rather unusual to define the scope of universals as it is proposed in the team submission 28 / 28
  • 94.
    ELIS – MultimediaLab Conclusion It is possible to define the semantics as in the team submission It is difficult and rather unusual to define the scope of universals as it is proposed in the team submission Implicit universal quantification could be handled easier, for example on formula level 28 / 28
  • 95.
    ELIS – MultimediaLab Conclusion It is possible to define the semantics as in the team submission It is difficult and rather unusual to define the scope of universals as it is proposed in the team submission Implicit universal quantification could be handled easier, for example on formula level Let’s simplify this! 28 / 28
  • 96.
    ELIS – MultimediaLab Example: Explicit quantification @forAll #x. @forSome #y. #x #loves #y . @forSome #y. @forAll #x. #x #loves #y . 29 / 28
  • 97.
    ELIS – MultimediaLab Example: Explicit quantification @forAll #x. @forSome #y. #x #loves #y . @forSome #y. @forAll #x. #x #loves #y . Have the same meaning: ∀x∃y : loves(x, y). 29 / 28
  • 98.
    ELIS – MultimediaLab Example: Variable of not? @forSome :y. :x :p :y. @forAll :x. :x :q :o. 30 / 28
  • 99.
    ELIS – MultimediaLab Example: Variable of not? @forSome :y. :x :p :y. @forAll :x. :x :q :o. Is the first :x quantified? 30 / 28