Next Prev Up

### 3 Fusion Logic

3.1 Syntax
3.2 Semantics

#### Syntax of Fusion Logic [Slide 4]

State formulae:

 W ::= true | p | W1 ∨ W2 |¬W

Transition formulae:

 T ::= W | W | T1 ∨ T2 |¬T

Fusion expressions:

 E ::= test(W) |step(T) | E1 ∨ E2 | E1 ; E2 | E∗

Right Fusion logic formulae:

 R ::= true | p  |¬R | R1 ∨ R2 |⟨E⟩R

Left Fusion logic formulae:

 L ::= true | ﬁn(p)  |¬L | L1 ∨ L2 | L⟨E⟩

Fusion logic formulae:

 F ::= L | R

#### State [Slide 5]

A state is a mapping State from the set of propositional variables Varb to the set of Boolean values Bool {tt,}.

tt is the semantic ‘true’ value and ﬀ the semantic ‘false’ value.

State : Varb Bool

We will use σ012,… to denote states and Σ to denote the set of all possible states.

Example 1. Let σ0 be a state such that

 σ0(P) = tt σ0(Q) = ﬀ

#### Interval and Length [Slide 6]

An interval σ is a ﬁnite sequence of states

σ : σ0σ1σ2

Let Σ+ denote the set of all possible ﬁnite intervals with at least one state.

The length of an interval σ is denoted by |σ| and is the number of states minus 1.

Example 2.

 σ = σ0 |σ| = 0 σ = σ0σ1 |σ| = 1 σ = σ0σ1…σn |σ| = n

#### Preﬁx, Suﬃx and Sub Interval [Slide 7]

Let σ = σ0σ1σ2 be an interval then

• σ0…σk (where 0 k ≤|σ|) denotes a preﬁx interval of σ
• σk…σ|σ| (where 0 k ≤|σ|) denotes a suﬃx interval of σ
• σk…σl (where 0 k l ≤|σ|) denotes a sub interval of σ

Example 3. Let σ = σ0σ1σ2σ3 be an interval then

 σ0σ1 is a preﬁx interval of σ σ1σ2σ3 is a suﬃx interval of σ σ1σ2 is a sub interval of σ

#### Semantics of State Formula [Slide 8]

Let M⟦⟧ be the “meaning” function from ‘state formulae’ × Σ+ to {tt,} and let σ be a ﬁnite interval (σ Σ+) then

 M⟦true⟧(σ) = tt M⟦p⟧(σ) = σ0(p) M⟦¬W⟧(σ) = not M⟦W⟧(σ) M⟦W1 ∨ W2⟧(σ) = M⟦W1⟧(σ) or M⟦W2⟧(σ)

#### Semantics of Transition formulae [Slide 9]

Let M⟦⟧ be the “meaning” function from ‘transition formulae’ × Σ+ to {tt,} and let σ be a ﬁnite interval (σ Σ+) then

 M⟦¬T⟧(σ) = not M⟦T⟧(σ) M⟦T1 ∨ T2⟧(σ) = M⟦T1⟧(σ) or M⟦T2⟧(σ) M⟦ W⟧(σ) = M⟦W⟧(σ 1…σ|σ|) and |σ| > 0

#### Semantics of Fusion expressions [Slide 10]

Let M⟦⟧ be the “meaning” function from ‘fusion expressions’ × Σ+ to {tt,} and let σ be a ﬁnite interval (σ Σ+) then

 M⟦test(W)⟧(σ) = M⟦W⟧(σ0) and |σ| = 0 M⟦step(T)⟧(σ) = M⟦T⟧(σ0…σ1) and |σ| = 1 M⟦E1 ∨ E2⟧(σ) = M⟦E1⟧(σ) or M⟦E2⟧(σ) M⟦E0 ; E1⟧(σ) = tt iﬀ exists a k, s.t. 0 ≤ k ≤|σ| and M⟦E0⟧(σ0…σk) = tt and M⟦E1⟧(σk…σ|σ|) = tt M⟦E∗⟧(σ) = tt iﬀ exist l0,…,ln s.t. l0 = 0 and ln = |σ| and for all 0 ≤ i < n,li < li+1 and M⟦E⟧(σli…σli+1) = tt

#### Semantics of right Fusion logic [Slide 11]

Let M⟦⟧ be the “meaning” function from ‘right fusion logic formulae’ × Σ+ to {tt,} and let σ be a ﬁnite interval (σ Σ+) then

 M⟦¬R⟧(σ) = = not M⟦R⟧(σ) M⟦R1 ∨ R2⟧(σ) = M⟦R1⟧(σ) or M⟦R2⟧(σ) M⟦⟨E⟩R⟧(σ) = tt iﬀ exists a k, s.t. 0 ≤ k ≤|σ| and M⟦E⟧(σ0…σk) = tt and M⟦R⟧(σk…σ|σ|) = tt

#### Semantics of left Fusion logic [Slide 12]

Let M⟦⟧ be the “meaning” function from ‘left fusion logic formulae’ × Σ+ to {tt,} and let σ be a ﬁnite interval (σ Σ+) then

 M⟦ﬁn(p)⟧(σ) = σ|σ|(p) M⟦¬L⟧(σ) = not M⟦L⟧(σ) M⟦L1 ∨ L2⟧(σ) = M⟦L1⟧(σ) or M⟦L2⟧(σ) M⟦L⟨E⟩⟧(σ) = tt iﬀ exists a k, s.t. 0 ≤ k ≤|σ| and M⟦L⟧(σ0…σk) = tt and M⟦E⟧(σk…σ|σ|) = tt

#### Derived operators [Slide 13]

Derived Fusion expression operators

 lene(0) ≜ test(true) lene(n + 1) ≜ step(true) ; lene(n) truee ≜ step(true)∗ moree ≜ step(true) ; truee eW ≜ truee ; test(W) ; truee eW ≜ step(W)∗ ; test(W) n : W ≜ truee ; test(W) ; lene(n)

#### Derived operators [Slide 14]

Derived right Fusion logic operators

 R1 ∧ R2 ≜ ¬(¬R1 ∨¬R2) R1 ⊃ R2 ≜ ¬R1 ∨ R2 morer ≜ ⟨step(true)⟩true emptyr ≜ ¬morer lenr(0) ≜ emptyr lenr(n + 1) ≜ ⟨step(true)⟩lenr(n) rR ≜ ⟨truee⟩R rR ≜ ¬r(¬R) rT ≜ r⟨step(T)⟩true rW ≜ r⟨truee⟩⟨test(W)⟩true rW ≜ ¬r(¬W) n : rW ≜ ⟨truee⟩⟨test(W)⟩lenr(n) [E]R ≜ ¬(⟨E⟩¬R)

#### Derived operators [Slide 15]

Derived left Fusion logic operators

 L1 ∧ L2 ≜ ¬(¬L1 ∨¬L2) L1 ⊃ L2 ≜ ¬L1 ∨ L2 morel ≜ true⟨step(true)⟩ emptyl ≜ ¬morel lenl(0) ≜ emptyl lenl(n + 1) ≜ lenl(n)⟨step(true)⟩ lW ≜ true⟨test(W)⟩⟨truee⟩ lW ≜ ¬l(¬W) lL ≜ L⟨truee⟩ lL ≜ ¬l(¬L) n : lW ≜ true⟨test(W)⟩⟨lene(n)⟩ L[E] ≜ ¬(¬L⟨E⟩)

#### Satisﬁable and valid [Slide 16]

• A fusion logic formula F is satisﬁable if and only if there exists an interval σ such that MF(σ) = tt
• Decision procedure checks whether F is satisﬁable or not, when F is satisﬁable a satisfying interval is generated.
• A fusion logic formula F is valid if and only if for all intervals σ, MF(σ) = tt
• F is not valid if and only if ¬F is satisﬁable i.e., satisfying interval for ¬F will represent a counter example for F’s validity F is valid if and only if ¬F is not satisﬁable

 Next Prev Up

 2024-08-02 Contact | Home | ITL home | Course | Proofs | Algebra | FL © 1996-2024