Horn Clauses in Hybrid-Dynamic First-Order
Logic
Daniel Găină

Ionuţ ŢuţuInstitute of Mathematics for Industry, Kyushu University, Japan
Department of Mathematics and Statistics, La Trobe University, Australia
Simion Stoilow Institute of Mathematics of the Romanian Academy, Romania
Department of Computer Science, Royal Holloway University of London, UK

The 15th Theorem Proving and Provers meeting

Reconfiguration paradigm● The present work is a part of a larger project: logical foundations ofreconfiguration paradigm● In many cases, the applications with reconfigurable features involvesafety-critical areas. For example, the new generation ofsoftware-driven medical devices such as imaging machines, pill cameras,
artificial pacemakers, the insulin infusion pump, etc.
● The safety requirements can be fulfilled only with formal methods● The safety requirements can be fulfilled only by applying formal
methods.
● “One of the main issues is that there is no real formal method of
implementing the reconfiguration of an application” [Szepesi andCiocarlie, Theory Appl. Math. Comput. Sci. 2011].

D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

2 / 21Hybrid-dynamic logics
Safe
reconfigurable systems

MedicaldevicesIntelligent
Driver applications
Cloud systems
transportation systems
They interact with users and the environment in which they coexist

All developments above
are powered by formal
methods

Formal methods are mathematically-based techniques for the specification and verification of software systems, and the only way to ensure safety of applications

Alldevelopments
above are powered by
math/logic

The design of a formal method relies on

1. model-theoretic studies
2. proof-theoretic support

Reconfigurable systems can be regarded as transition systems in the following way:
● the configurations are states, and● switching from one configuration to another is a transition.
Hybrid dynamic logics are modal logics that can describe transitions systems and express the
dynamics of (re)configurations:● the configurations of the software in use today may be modeled with first-order logic,
higher-order logic, rewriting logic, etc; these are considered base logics;● the construction of a hybrid logic on top of a base logic is called
hybridization [Diaconescu and Madeira, Math. Struct. Comput. Sci. 2016].

D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

3 / 21

Formal method design● Institution category-based formalization of the intuitive definition of logical system[Goguen and Burstall, Journal of the ACM 1992]● Hybrid institution formalizes the notion of hybrid logic by supplementing the definition of
institution with an additional structure to extract (a) nominals and modalities fromsignatures, and (b) frames from models.
Formal method design
1. Underlying logic

Formalization at appropriate
abstraction level

2. Structured specifications/language
constructs
3. Specification & Verification methodology
4. Tool support

Result instantiation

Theory of institutions
Proof oflogical properties
O1) Abstract model theory
O2) Proof-theoretic support● the design of a formal method consists of several steps depicted in the left node of the
figure above● each step relies on some model-theoretic or proof-theoretic properties which should be
defined at an appropriate abstraction level in the framework of hybrid institutions● the proof of model-theoretic and proof-theoretic properties should be performed within theframework of hybrid institutions as depicted in the right side of the figure above● once proved the abstract results are instantiated to concrete logical systems

D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

4 / 21Preparation status● Definition of hybrid institution and foundation of logic programming in
hybrid institutions [Gaina, Theor. Comput. Sci. 2017]● Abstract proof calculus for hybrid institutions whose sentences are
Horn clauses [Gaina, Formal Asp. Comput. 2017]● Proof calculus for the Horn clauses of hybrid-dynamic first-order logic[Gaina and Tutu, TABLEAUX 2019]● Forcing in hybrid institutions [Gaina, Journal of the ACM accepted]
The following figure shows the advancements for this project and how
this work will be completed in the present project.
Proof calculi(for all sentences)
Birkhoff proof calculi(for Horn clauses only)
Structured specifications(initiality + imports)

D. Găină and I. ŢuţuHybrid institutions

Hybrid-dynamic institutions[Gaina, Journal of the ACM accepted]

future work

[Gaina, Formal Asp. Comput. 2017][Gaina and Tutu, TABLEAUX 2019] + future work

[Gaina, Theor. Comput. Sci. 2017][Gaina and Tutu, TABLEAUX 2019] + future work

Hybrid-Dynamic First-Order Logic

5 / 21

Semantics first: Kripke models● mathematical structures used to model the behaviour of a system● underlie the semantics of modal, hybrid, dynamic and temporal logics● typically, a Kripke structure consists in a (hyper)graph where:– each node (possible world) represents a state of the system– each edge (part of an accessibility relation) represents a transition● the original definition has been extended in various ways:– complex algebraic structures as labels of the states– structured actions as labels of transitions– model constraints

D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

6 / 21Hybrid-Dynamic First-Order Logic with user-defined sharing
A logic for specifying and reasoning about Kripke structures. . . obtained by enriching first-order logic
with features that are characteristic tohybrid logics (nominals and local-satisfaction operators) anddynamic logics (structured actions over modalities). . . and with a number of distinctive attributes:● a first-order structure on possible worlds● supports sharing between possible worlds / rigidity constraints● hybrid terms (annotated with nominals)

D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

7 / 21

Signatures
Definition. An HDFOL-signature is a tuple ∆ = (Σn , Σr ⊆ Σ), where:● Σn = (F n , P n ) is a single-sorted first-order signature of nominals,
where Fin is a set of nominal operations of arity i ∈ N● Σr = (S r , F r , P r ) is a many-sorted signature of rigid symbols, wherer
Far→s
is a set of operations of arity ar ∈ S r∗ and sort s ∈ S r● Σ = (S, F, P ) is a many-sorted first-order signature of both rigid andflexible symbols
An HDFOL-signature morphism ϕ∶ ∆ → ∆′ consists of a pair of first-ordersignature morphisms ϕn ∶ Σn → Σ′n and ϕ∶ Σ → Σ′ such that ϕ(Σr ) ⊆ Σ′r .

D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

8 / 21

Semantics

Definition. A Kripke model of ∆ = (Σn , Σr ⊆ Σ) is a pair ⟨W, M ⟩:● W is a Σn -model, whose carrier set we denote by ∣W ∣● M = (Mw )w∈∣W ∣ is a family of Σ-models, indexed by worlds, such that
Mw1 ,ς = Mw2 ,ς for all w1 , w2 ∈ ∣W ∣ and symbols ς in Σr(rigid symbols have the same interpretation across possible worlds)
A homomorphism h∶ ⟨V, N ⟩ → ⟨W, M ⟩ is also a pair, consisting offirst-order homomorphisms h∶ V → W and hv ∶ Nv → Mh(v) , for every
world v ∈ ∣V ∣, such that hv1 ,s = hv2 ,s for all v1 , v2 ∈ ∣V ∣ and s ∈ S r .

D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

9 / 21Syntax
The set actions over ∆ is defined in an inductive fashion, according to the following grammar:a ∶∶= λ ∈ P2n ∣ a ; a ∣ a ∪ a ∣ a∗
The atomic sentences defined over a signature ∆ are given by:
nominal equations and relationsρ ∶∶= k1 = k2 ∣ λ(k′ ) ∣ t1 =k,s t2 ∣ $(t) ∣ π(k; t)hybrid equations and relations

Full sentences over ∆ are built from atomic sentences according to the following grammar:γ ∶∶= ρ ∣ a(k1 , k2 ) ∣ @k γ ∣ ¬γ ∣ ⋀ Γ ∣ ↓z ⋅ γ ′ ∣ ∀X ⋅ γ ′′where z is a nominal variable, X is a set of variables, and γ ′ , γ ′′ are sentences over theextended signatures ∆[z] and ∆[X], respectively.

D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

10 / 21

Local-satisfaction relation
Definition. Given a Kripke model ⟨W, M ⟩ of a signature ∆ and apossible world w ∈ ∣W ∣, we have, for atomic sentences:● ⟨W, M ⟩ ⊧w k1 = k2

● ⟨W, M ⟩ ⊧w λ(k)● ⟨W, M ⟩ ⊧w t1 =k t2● ⟨W, M ⟩ ⊧ $(t)● ⟨W, M ⟩ ⊧w π(k; t)w

D. Găină and I. Ţuţuiff

Wk1 = Wk2

iff

Wk ∈ Wλiff⟨W, M ⟩t1 = ⟨W, M ⟩t2

iff⟨W, M ⟩t ∈ Mw,$

iff

⟨W, M ⟩t ∈ Mw′ ,π , where w′ = Wk

Hybrid-Dynamic First-Order Logic

11 / 21

Local-satisfaction relation
Definition. Given a Kripke model ⟨W, M ⟩ of a signature ∆ and apossible world w ∈ ∣W ∣, we have, for full sentences:● ⟨W, M ⟩ ⊧w a(k1 , k2 )● ⟨W, M ⟩ ⊧w @k γ

● ⟨W, M ⟩ ⊧w ¬γ● ⟨W, M ⟩ ⊧w ⋀ Γ● ⟨W, M ⟩ ⊧w ↓z ⋅ γ

iff(Wk1 , Wk2 ) ∈ Wa

iff

⟨W, M ⟩ ⊧w γ, where w′ = Wk

iff

⟨W, M ⟩ ⊭w γ

iff

⟨W, M ⟩ ⊧w γ for all γ ∈ Γ

iff⟨W, M ⟩z←w ⊧w γ′

(W ′ , M ′ ) ⊧w γ for all∆[X]-expansions (W ′ , M ′ ) of ⟨W, M ⟩● ⟨W, M ⟩ ⊧w ∀X ⋅ γiff

D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

11 / 21

Expressivity and relationship to other modal logics
Support for conventional modal operators● [a]γ ≜ ↓z ⋅ ∀z ′ ⋅ a(z, z ′ ) ⇒ @z ′ γ● ⟨a⟩γ ≜ ↓z ⋅ ∃z ′ ⋅ a(z, z ′ ) ∧ @z ′ γ

Support for (linear) temporal operators● ◯ γ ≜ ↓z ⋅ @next(z) γ● ρ Until γ ≜ ∃z ⋅ ◊(z ∧ γ) ∧ ◻(◊z ⇒ ρ)
Hybrid (annotated) terms vs ordinary terms● c1 (k) = σ(k; c2 (k)) is equivalent to @k c1 = σ(c2 )● c3 (k) = σ(k; c4 (k0 )) is equivalent to ∃x ⋅ @k0 x = c4 ∧ @k c3 = σ(x)Implicit vs explicit dependence on possible worlds● the nominal sentence k is equivalent to ↓z ⋅ z = k● the store sentence ↓z ⋅ γ is equivalent to ∃z ⋅ (z ∧ γ)

D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

12 / 21

Event-based transition system
submit-pswd2
submit-id3

submit-pswd1 , hint

cancel1

anonymouscheck-credentials
try-again
submit-id1,2

submit-pswd3

cancel2

authorized

Events:● submit-id, submit-pswd,
cancel● try-again, hint
D. Găină and I. Ţuţu

Attributes:● status, uid, attpts,
observations● type-id, type-pswd
random values

Hybrid-Dynamic First-Order Logic

13 / 21

Setting the stage for Birkhoff completenessGoal: syntactic characterization of the satisfiability relations Γ ⊧∆ γ
⟨W, M ⟩ ⊧ γ for all ∆-models ⟨W, M ⟩ such that ⟨W, M ⟩ ⊧ Γ● both Γ and γ belong to the Horn-clause fragment of HDFOLDefinition. By Horn clause, we mean a sentence obtained from atomic
sentences by repeated applications of the following sentence-building
operators, in any order:● retrieve● implication (hypothesis: only atoms or action relations)● store● universal quantification● necessity, next
D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

14 / 21

Setting the stage for Birkhoff completenessGoal: syntactic characterization of the satisfiability relations Γ ⊧∆ γ
⟨W, M ⟩ ⊧ γ for all ∆-models ⟨W, M ⟩ such that ⟨W, M ⟩ ⊧ Γ● both Γ and γ belong to the Horn-clause fragment of HDFOLDefinition. By Horn clause, we mean a sentence obtained from atomic
sentences by repeated applications of the following sentence-building
operators, in any order:● retrieve● implication (hypothesis: only atoms or action relations)● store● universal quantification● necessity, next
D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

14 / 21

A layered approach● develop progressively a series of syntactic entailment relations
Γ⊢γ● where each layer builds on the previous one to allow for more generalantecedents or consequents● three major steps / entailment relations
Atomic completeness: both Γ and γ are atomic
Quasi-completeness: Γ is arbitrary, but γ is atomic
Horn-clause completeness: both Γ and γ are arbitrary● all are sound and complete; only the first two are also compact● atomic completeness is much more difficult to establish than it may
seem at first sight. . .
D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

15 / 21

A layered approach● develop progressively a series of syntactic entailment relations
Γ⊢γ● where each layer builds on the previous one to allow for more generalantecedents or consequents● three major steps / entailment relations
Atomic completeness: both Γ and γ are atomic
Quasi-completeness: Γ is arbitrary, but γ is atomic
Horn-clause completeness: both Γ and γ are arbitrary● all are sound and complete; only the first two are also compact● atomic completeness is much more difficult to establish than it may
seem at first sight. . .
D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

15 / 21

A layered approach● develop progressively a series of syntactic entailment relations
Γ⊢γ● where each layer builds on the previous one to allow for more generalantecedents or consequents● three major steps / entailment relations
Atomic completeness: both Γ and γ are atomic
Quasi-completeness: Γ is arbitrary, but γ is atomic
Horn-clause completeness: both Γ and γ are arbitrary● all are sound and complete; only the first two are also compact● atomic completeness is much more difficult to establish than it may
seem at first sight. . .
D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

15 / 21

Atomic completeness
Proof rules

Lemma. For every set Γ of nominal equations over a signature ∆, there
exists a reachable initial model (W Γ , M Γ ) such thatΓ ⊧ ρ iff(W Γ , M Γ ) ⊧ ρ iffΓ⊢ρ

for all nominal or hybrid equations ρ over ∆.
Theorem (Atomic completeness). Every set Γ of atomic sentences
over a signature ∆ has a reachable initial model (W Γ , M Γ ) such thatΓ ⊧ ρ iff(W Γ , M Γ ) ⊧ ρ iffΓ⊢ρ

for all atomic sentences ρ over ∆.

D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

16 / 21

Quasi-completeness
Proof rules

Theorem (Quasi-completeness). Let:● Γ be a set of clauses over a signature ∆,● Γ0 = {ρ ∈ SenHDCLS (∆) ∣ Γ ⊢ ρ & ρ is atomic},● (W Γ0 , M Γ0 ) a reachable initial model of Γ0 as before.

Then the following statements are equivalent:
1. Γ ⊧ ρ
2. (W Γ0 , M Γ0 ) ⊧ ρ
3. Γ ⊢ ρ

D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

17 / 21

Horn-clause completeness
Proof rules

Theorem (Birkhoff completeness). The entailment relation generated
by the rules presented thus far is sound and complete.
Γ⊧γ

if and only ifΓ⊢γMoreover, in the absence of (StarI ), it is also compact.
Proposition (Lack of compactness). HDCLS does not admit anentailment relation that is sound, complete, and also compact.

D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

18 / 21

Conclusions

To sum up● we have introduced a hybrid-dynamic first-order logic● seen how it relates to modal/temporal/hybrid logics● presented a sound and complete calculus for its Horn fragment● touched upon the limits of compactness
Ongoing work
● decidability properties and support for executable specifications● case studies & a prototype implementation

D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

19 / 21

Conclusions

To sum up● we have introduced a hybrid-dynamic first-order logic● seen how it relates to modal/temporal/hybrid logics● presented a sound and complete calculus for its Horn fragment● touched upon the limits of compactness
Ongoing work
● decidability properties and support for executable specifications● case studies & a prototype implementation

D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

19 / 21

Thank you!

Atomic completeness
Rules for nominal terms

(Rn )

(Tn )

(Fn )

(Sn )

Γ⊢k=k
Γ ⊢ k1 = k2

Γ ⊢ k1 = k2
Γ ⊢ k2 = k1

Γ ⊢ k2 = k3

Γ ⊢ k1 = k3
Γ ⊢ k1 = k2

Γ ⊢ o(k1 ) = o(k2 )Γ ⊢ λ(k1 )Γ ⊢ k1 = k2(Pn )Γ ⊢ λ(k2 )D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

20 / 21

Atomic completeness
Rules for sharing

(Wh )

(Wr )

(Wf )

Γ ⊢ k = k′Γ ⊢ t =k,s δk′ /k (t)Γ ⊢ t1 =k1 ,s t2
Γ ⊢ t1 =k2 ,s t2
Γ ⊢ k = k′where s ∈ S r

where s ∈ S r
Γ ⊢ t1 =k t2

Γ ⊢ δk/k′ (t1 ) =k′ δk/k′ (t2 )D. Găină and I. ŢuţuHybrid-Dynamic First-Order Logic

20 / 21

Atomic completeness
Rules for hybrid terms

(Fr )

(Pr )

(Ph )

Γ ⊢ t1 =k,ar t2Γ ⊢ σ(t1 ) =k,s σ(t2 )Γ ⊢ t1 =k t2 Γ ⊢ π(t1 )Γ ⊢ π(t2 )Γ ⊢ k1 = k2 Γ ⊢ π(k1 ; t1 )Γ ⊢ π(k2 ; δk1 /k2 (t1 ))D. Găină and I. Ţuţu(Ff )Γ ⊢ t1 =k,ar t2Γ ⊢ σ(k; t1 ) =k,s σ(k; t2 )(Pf )(Ret0 )

Γ ⊢ t1 =k t2

Γ ⊢ π(k; t1 )Γ ⊢ π(k; t2 )
Γ ⊢ @k ρ

Hybrid-Dynamic First-Order LogicΓ⊢ρ

20 / 21

Quasi-completeness
Rules for action relations(Comp)(Union)(Refl)

Γ ⊢ a1 (k1 , k2 )Γ ⊢ a2 (k2 , k3 )Γ ⊢ (a1 ; a2 )(k1 , k3 )
Γ ⊢ ai (k1 , k2 )Γ ⊢ (a1 ∪ a2 )(k1 , k2 )Γ ⊢ k1 = k2∗

Γ ⊢ a (k1 , k2 )D. Găină and I. Ţuţu(Star)

Γ ⊢ a(ki , ki+1 ) for 0 ≤ i < nHybrid-Dynamic First-Order LogicΓ ⊢ a∗ (k0 , kn )20 / 21

Quasi-completeness
Rules for Horn clauses(Ret@ )

(ImpE )

(StoreE )Γ ⊢ @k1 @k2 γ(RetI )Γ ⊢ @k2 γΓ⊢γ
Γ ⊢ @k γΓ ⊢ @k (⋀ H ⇒ γ)Γ ∪ H ⊢ @k γΓ ⊢ @k ↓z ⋅ γΓ ⊢ @k θz←k (γ)

D. Găină and I. Ţuţu(Substq )Hybrid-Dynamic First-Order LogicΓ ⊢ @k ∀X ⋅ γΓ ⊢ @k θ(γ)

20 / 21

Horn-clause completeness
Additional rules for Horn clauses(RetE )

(StoreI )Γ ⊢∆[z] @z γ

(ImpI )

Γ ⊢∆ γΓ ⊢ @k θz←k (γ)

D. Găină and I. Ţuţu@k ↓z ⋅ γΓ ∪ H ⊢ @k γΓ ⊢ @k (⋀ H ⇒ γ)

(QuantI )Hybrid-Dynamic First-Order LogicΓ ⊢∆[X] @k γΓ ⊢∆ @k ∀X ⋅ γ

20 / 21

Horn-clause completeness
Additional rules for action relations(CompI )(UnionI )(StarI )D. Găină and I. Ţuţu

E ∪ {a1 (k1 , z), a2 (z, k2 )} ⊢∆[z] e
E ∪ {(a1 ; a2 )(k1 , k2 )} ⊢∆ e
E ∪ {ai (k1 , k2 )} ⊢ e for i ∈ {1, 2}
E ∪ {(a1 ∪ a2 )(k1 , k2 )} ⊢ e

E ∪ {an (k1 , k2 )} ⊢ e for all n ∈ N
E ∪ {a∗ (k1 , k2 )} ⊢ eHybrid-Dynamic First-Order Logic

20 / 21

Generic insulin infusion pump
Pump controller - an abstract
representation of genericinsulin pump software● Main functionality: command
the pump delivery mechanism
to propel insulin stored in the
drug reservoir to the patient
through the drug delivery
interface and the infusion set● Overall responsibility: ensure
correct operation of the modelMore about pump controller functionality:● interacts with the patient through a user interface● it alerts the patient when abnormal conditions arise● recommends appropriate bolus dosages with the help of a bolus calculator and a food
database● manages and checks parameters and programs related to insulin administration;● logs important data and events during pump use to facilitate clinical use analysis andproblem diagnosis