A Logic of Propositional Variations and Its Application to Case-Based Reasoning

For every knowledge base B of ( Δ L P , ⊨ ) and every φ ∈ Δ L P , B ⊨ alt φ iff B ⊨ φ .

Given I J ∈ Δ Ω , let ω I J ∈ Δ Ω alt be such that, for a ∈ V ,

ω I J ( a ) = { = 1 if I ( a ) = J ( a ) = 1 = 0 if I ( a ) = J ( a ) = 0 + if I ( a ) = 0 and J ( a ) = 1 − if I ( a ) = 1 and J ( a ) = 0 .

I ( a ) = { 0 if ω ( a ) ∈ { = 0 , + } 1 else J ( a ) = { 0 if ω ( a ) ∈ { = 0 , − } 1 else

It is shown then that, for I J ∈ Δ Ω and φ ∈ Δ L P , I J ⊨ φ iff ω I J ⊨ alt φ .

Finally, for a knowledge base B and φ ∈ Δ L P , it is shown that B ⊨ φ iff B ⊨ alt φ using the bijective function introduced above and (2).

Proposition 2

For all a ∈ V , let ℓ ( a ) , m ( a ) ∈ { a , ¬ a , ⊤ } . Then ( ⋀ a ∈ V ℓ ( a ) ) ▹ ( ⋀ a ∈ V m ( a ) ) ≡ ⋀ a ∈ V ℓ ( a ) ▹ m ( a ) .

Proof.

From the definition of the semantics, it yields that, for I , J ∈ Ω :

I J ⊨ ⋀ a ∈ V ℓ ( a ) ▹ m ( a ) iff for all a ∈ V , I J ⊨ ℓ ( a ) ▹ m ( a ) i f f for all a ∈ V , I ⊨ ℓ ( a ) and J ⊨ m ( a ) iff ( for all a ∈ V , I ⊨ ℓ ( a ) ) and ( for all a ∈ V , J ⊨ m ( a ) ) iff I ⊨ ( ⋀ a ∈ V ℓ ( a ) ) and J ⊨ ( ⋀ a ∈ V m ( a ) ) iff I J ⊨ ( ⋀ a ∈ V ℓ ( a ) ) ▹ ( ⋀ a ∈ V m ( a ) )

Some definitions of formulas in the article are given by the set of their models, thus up to equivalence. This kind of definition is acceptable because every subset of Δ Ω is representable in Δ L P :

Proposition 3

For every subset A of Δ Ω , there exists φ ∈ Δ L P such that M ( φ ) = A .

Proof.

Let I J ∈ Δ Ω , and let the formula

ψ I J = ⋀ { a pvs ( I ( a ) , J ( a ) ) | a ∈ V } where pvs : ( 0 , 0 ) ↦ = 0 ( 1 , 1 ) ↦ = 1 ( 0 , 1 ) ↦ + ( 1 , 0 ) ↦ −

(for i and j two Booleans, pvs ( i , j ) is the primitive variation symbol associated with ( i , j ) ). It can be shown first that, for every a ∈ V , I J ⊨ a pvs ( I ( a ) , J ( a ) ) (just consider the four cases). Conversely, if for every a ∈ V , I 1 J 1 ⊨ a pvs ( I ( a ) , J ( a ) ) entails I 1 ( a ) = I ( a ) and J 1 ( a ) = J ( a ) , then I 1 J 1 = I J . Consequently, M ( ψ I J ) = { I J } . Now, with φ = ⋁ { ψ I J | I J ∈ A } , M ( φ ) = A .

3.3.2. Results Borrowed from Propositional Logic

The following results (and their proofs) are easily transposed from results in proposition logics.

Deduction theorem and its corollary (for φ 1 , φ 2 ∈ Δ L P ):

φ 1 ⊨ φ 2 iff ⊨ φ 1 → φ 2 φ 1 ≡ φ 2 iff ⊨ φ 1 ↔ φ 2

Link between tautologies and satisfiable formulas ( φ ∈ Δ L P ):

⊨ φ {{iff}} ¬ φ is unsatisfiable

Proposition 4

Let ConnectiveSet be a set of connectives of propositional logic that is sufficient for defining the syntax of this logic (e.g., for every α ∈ L P , there exists α ′ ∈ L P such that α ′ ≡ α and the connectives of α ′ belong to ConnectiveSet ). Examples for ConnectiveSet are { ¬ , ∧ , ∨ } , { ¬ , ∧ } , and { ¬ , → } . Then, the following syntax restrictions of ( Δ L P , ⊨ ) does not restrict its semantics (every formula φ ∈ Δ L P can be rewritten in an equivalent formula φ ′ with the considered syntax restriction): SR1

Connectives of ConnectiveSet , a v where a ∈ V and v ∈ D 0

(hence no a w , w ∈ D 1 , no α v , α ∈ L P ∖ V , no occurrence of ▹ );

SR2

Connectives of ConnectiveSet , a v where a ∈ V and v ∈ D 1 ;

SR3

Connectives of ConnectiveSet , ℓ ▹ m , where ℓ and m are literals of ( L P , ⊨ ) .

Then, some normal forms can be defined.

Definition 1 (normal forms)

A clause of ( Δ L P , ⊨ ) is a disjunction of literals a v ( a ∈ V , v ∈ D ). A primitive clause is a disjunction of primitive literals a v ( v ∈ D 0 ).

A formula of ( Δ L P , ⊨ ) is under negation free normal form (NFNF) if it is built syntactically with the only connectives are ∧ and ∨ and with the literals a v ( v ∈ D 0 ).

A formula of ( Δ L P , ⊨ ) is under disjunctive normal form (DNF) if it is a disjunction of primitive cubes.

A formula of ( Δ L P , ⊨ ) is under conjunctive normal form (CNF) if it is a conjunction of primitive clauses.

An empty disjunction (resp. conjunction) is assimilated to ⊥ (resp. to ⊤ ): ⋁ ψ ∈ ∅ ψ = ⊥ and ⋀ ψ ∈ ∅ ψ = ⊤ .

Proposition 5

Every φ ∈ Δ L P can be put under NFNF, DNF, and CNF.

Proof Sketch of proof.

First, the following result is proven (for v ∈ D 0 ):

¬ a v ≡ ⋁ w ∈ D 0 ∖ { v } a w

(3)

For I J ∈ Δ Ω , the following sequence of equivalences holds:

I J ⊨ ¬ a v iff I J ⊭ a v iff ( I ( a ) , J ( a ) ) ≠ pvs − 1 ( v ) iff ( I ( a ) , J ( a ) ) ∈ { 0 , 1 } 2 ∖ { pvs − 1 ( v ) } iff I J ⊨ a w f o r s o m e w ∈ D 0 ∖ { v } iff I J ⊨ ⋁ w ∈ D 0 ∖ { v } a w

Let φ ∈ Δ L P . φ is equivalent to a formula φ ′ under SR4 (cf. Proposition 4) with the connectives ¬ , ∧ , and ∨ . Then, ¬ can be removed from φ ′ using De Morgan laws ( ¬ ( φ ∧ ψ ) ≡ ¬ φ ∨ ¬ ψ and ¬ ( φ ∨ ψ ) ≡ ¬ φ ∧ ¬ ψ ) and equivalence (3), from left to right, as long as it is possible. The result of this transformation is a formula φ NFNF equivalent to φ and under NFNF.

Using distributive property of ∧ over ∨ (resp. on ∨ over ∧ ) on φ NFNF as long as it is possible, gives a formula under DNF (resp. under CNF).

Definition 2

For φ ∈ Δ L P , L ( φ ) and R ( φ ) denote propositional formulas (unique up to logical equivalence) such that

M ( L ( φ ) ) = { I | I J ∈ M ( φ ) } M ( R ( φ ) ) = { J | I J ∈ M ( φ ) }

L ( φ ) is called the left part of φ and R ( φ ) its right part.

To compute L ( φ ) and R ( φ ) , a method consists in putting φ into disjunctive normal form (disjunction of cubes) and to apply Proposition 6 below: an example at the end of the section illustrates this. To prove this proposition, the following lemma is used, stating something that may seem obvious but that may deserve to be stated nonetheless.

Lemma 1

Only the variables occurring in formulas of ( Δ L P , ⊨ ) may play a role in a deductive inference:

f o r a n y φ ∈ Δ L P , if I 1 J 1 , I 2 J 2 ∈ Δ Ω satisfy I 1 ( x ) = I 2 ( x ) and J 1 ( x ) = J 2 ( x ) for all x ∈ V ( φ ) then I 1 J 1 ⊨ φ iff I 2 J 2 ⊨ φ

Proof Sketch of proof.

The proof of this lemma can be done by a simple mathematical induction.

Proposition 6

For φ , ψ ∈ Δ L P and α , β ∈ L P ,

L ( φ ∨ ψ ) ≡ L ( φ ) ∨ L ( ψ ) and R ( φ ∨ ψ ) ≡ R ( φ ) ∨ R ( ψ )

(4)

if V ( φ ) ∩ V ( ψ ) = ∅ then L ( φ ∧ ψ ) ≡ L ( φ ) ∧ L ( ψ ) and R ( φ ∧ ψ ) ≡ R ( φ ) ∧ R ( ψ )

(5)

if α and β are both satisfiable then L ( α ▹ β ) ≡ α and R ( α ▹ β ) ≡ β

(6)

else L ( α ▹ β ) ≡ R ( α ▹ β ) ≡ ⊥

(7)

The example below shows the computation of L ( φ ) for φ = ( a − ∨ b = 1 ) ∧ c + :

L ( φ ) ≡ L ( ( a − ∧ c + ) ∨ ( b = 1 ∧ c + ) ) ≡ L ( a − ∧ c + ) ∨ L ( b = 1 ∧ c + ) ≡ ( L ( a − ) ∧ L ( c + ) ) ∨ ( L ( b = 1 ) ∧ L ( c + ) ) ≡ ( L ( a ▹ ¬ a ) ∧ L ( ¬ c ▹ c ) ) ∨ ( L ( b ▹ b ) ∧ L ( ¬ c ▹ c ) ) ≡ ( a ∧ ¬ c ) ∨ ( b ∧ ¬ c ) ≡ ( a ∧ b ) ∨ ¬ c

3.4. Inverse and Composition on Variation Formulas

A formula φ ∈ Δ L P can be seen as a representation of a binary relation on Ω , since M ( φ ) ⊆ Ω × Ω . Therefore, operations on binary relations can be defined on variation formulas, in particular, the inverse of a formula and the composition of two formulas.

3.4.1. Inverse of a Variation Formula

Definition 3

For φ ∈ Δ L P , let φ − 1 ∈ Δ L P semantically defined by

M ( φ − 1 ) = { J I | I J ∈ M ( φ ) }

The following proposition shows how φ − 1 can be syntactically defined, whatever the choice of syntactic constructors of ( Δ L P , ⊨ ) are chosen according to Proposition 4:

Proposition 7

Let α , β ∈ L P , ψ , φ 1 , φ 2 ∈ Δ L P and * ∈ { ∧ , ∨ , → , ↔ } . Then:

⊤ D − 1 ≡ ⊤ D ⊥ D − 1 ≡ ⊥ D ( ¬ φ ) − 1 ≡ ¬ ( φ − 1 ) ( φ 1 * φ 2 ) − 1 ≡ φ 1 − 1 * φ 2 − 1 ( α ▹ β ) − 1 ≡ β ▹ α ( α = 1 ) − 1 ≡ α = 1 ( α = 0 ) − 1 ≡ α = 0 ( α + ) − 1 ≡ α − ( α − ) − 1 ≡ α + ( α = ) − 1 ≡ α = ( α ≠ ≠ ) − 1 ≡ α ≠ ≠ ( α 0 ∙ ) − 1 ≡ α ∙ 0 ( α 1 ∙ ) − 1 ≡ α ∙ 1 ( α ∙ 0 ) − 1 ≡ α 0 ∙ ( α ∙ 1 ) − 1 ≡ α 1 ∙

Proof Sketch of proof.

The proof of each of these equivalences is rather straightforward. As an example, the equivalence ( ¬ φ ) − 1 ≡ ¬ ( φ − 1 ) can be proven as follows (for I J ∈ Δ Ω ):

I J ⊨ ( ¬ φ ) − 1 iff J I ⊨ ¬ φ iff J I ⊭ φ iff I J ⊭ φ − 1 iff I J ⊨ ¬ ( φ − 1 )

3.4.2 Composition of Two Formulas

Definition 4

Let φ , ψ ∈ Δ L P . The composition of φ and ψ is a formula φ ; ψ defined semantically by

M ( φ ; ψ ) = { I K ∈ Δ Ω ~there exists J ∈ Ω such that I J ⊨ φ and J K ⊨ ψ }

In other words, M ( φ ; ψ ) is the composition of the binary relations M ( φ ) and M ( ψ ) on Ω : M ( φ ; ψ ) = M ( ψ ) ∘ M ( φ ) .

The following result is a direct consequence of associativity of binary relation composition:

for φ , ψ , χ ∈ Δ L P , ( φ ; ψ ) ; χ ≡ φ ; ( ψ ; χ )

This allows to omit parentheses in compositions.

The research of a formula equivalent to φ ; ψ is studied via the following propositions, whose proofs are given in Appendix Section A.2.

Let us start with the case where the formulas to be composed are of the form α ▹ β .

Proposition 8

Let α , β , γ , δ ∈ L P . Then:

( α ▹ β ) ; ( γ ▹ δ ) ≡ { ⊥ if β ∧ γ ⊨ ⊥ α ▹ δ otherwise

We focus next on the links between composition and disjunction:

Proposition 9

Let φ , φ 1 , φ 2 , ψ , ψ 1 , ψ 2 ∈ Δ L P . The following equivalences hold:

φ ; ( ψ 1 ∨ ψ 2 ) ≡ ( φ ; ψ 1 ) ∨ ( φ ; ψ 2 )

(8)

( φ 1 ∨ φ 2 ) ; ψ ≡ ( φ 1 ; ψ ) ∨ ( φ 2 ; ψ )

(9)

Definition 5

Two additional variation symbols are introduced: ⊥ D and ⊤ D such that, for all α ∈ L P , α ⊥ D = ⊥ ▹ ⊥ = ⊥ Δ and α ⊤ D = ⊤ ▹ ⊤ = ⊤ Δ .

To a variable x and a cube φ of ( Δ L P , ⊨ ) is associated var ( x , φ ) ∈ D ∪ { ⊤ D } as follows:

var ( x , φ ) = { ⊤ D if x ∉ V ( φ ) v if x v is a term of φ

The following proposition allows to compute the composition of two literals of ( Δ L P , ⊨ ) built on the same variable.

Proposition 10

There exists a binary operation ; over D ∪ { ⊥ D , ⊤ D } such that for a ∈ V and v , w ∈ D ∪ { ⊥ D , ⊤ D } , a v ; a w = a v ; w .

Now, the composition of cubes can be computed thanks to the following proposition:

Proposition 11

Let φ and ψ be two cubes of ( Δ L P , ⊨ ) . Then

φ ; ψ ≡ ⋀ a ∈ V a var ( a , φ ) ; var ( a , ψ )

(10)

To compose two cubes, Proposition 11 is applied and then a simplification is made by remembering that x ⊤ D ≡ ⊤ and x ⊥ D ≡ ⊥ . For example, if the set of variables is { a , b , c , d , e } then, according to Table 2 in Appendix Section A.2:

a + ∧ b = ∧ d = 0 ; a − ∧ c − ∧ d + ≡ a = 0 ∧ b ⊤ D ∧ c ∙ 0 ∧ d + ∧ e ⊤ D ≡ a = 0 ∧ c ∙ 0 ∧ d +

More generally, a way to have a syntactical expression of φ ; ψ consists in putting these two formulas of ( Δ L P , ⊨ ) under DNF, and then applying the equivalences of Proposition 9 as long as it is possible, and finally applying Proposition 11 to eliminate completely the symbol ; .

4. A Sound and Complete Formal System for ( Δ L P , ⊨ )

In this section, S Δ H , a formal system sound and complete for ( Δ L P , ⊨ ) is presented and studied that is strongly inspired by S H , the formal system of Hilbert that is sound and complete for ( L P , ⊨ ) .

4.1. Definition of the Formal System S Δ H

S Δ H , as any Hilbert style formal system, is defined by a triple ( L S Δ H , A S Δ H , I R S Δ H ) where L S Δ H is the set of the well-formed formulas (wffs) of S Δ H , A S Δ H is the set of its axioms and I R S Δ H is the set of its inference rules.

Proposition 4 shows that every formula can be written with some syntactical restrictions. In particular, every formula can be written only with the atoms a v where a ∈ V and v ∈ D 0 , and with the only connectives ¬ and → (the other connectives being defined as abbreviations, e.g., φ ∧ ψ is an abbreviation for ¬ ( φ → ¬ ψ ) ). A wff φ ∈ L S Δ H is a formula of Δ L P with these syntactical restrictions.

The set of axioms, A S Δ H , is a subset of L S Δ H defined by the following axiom schemes:

{(AS1)} φ → ( ψ → φ ) {(AS2)} ( φ → ( ψ → χ ) ) → ( ( φ → ψ ) → ( φ → χ ) ) {(AS3)} ( ¬ φ → ¬ ψ ) → ( ψ → φ ) {(AS4)} a v → ¬ a w {(AS5)} ¬ a v → ( ¬ a w → ( ¬ a x → a y ) )

where φ , ψ , and χ have to be replaced with any wffs, a has to be replaced with any variable, and v , w , x , y have to be replaced by primitive variation symbols that are pairwise distinct. The axioms schemes (AS1), (AS2), and (AS3) are directly taken from Hilbert formal system. The axiom schemes (AS4) and (AS5) translate the fact that { M ( a v ) | v ∈ D 0 } is a partition of Δ Ω .

I R S Δ H = { m p } : the only inference rule of S Δ H is the modus ponens that is also the only inference rule of S H : φ φ → ψ ψ m p .

4.2. Soundness of S Δ H for ( Δ L P , ⊨ )

Let ⊢ Δ be the entailment relation associated with S Δ H whose definition is recalled now. Let B be a subset of L S Δ H and φ ∈ Δ L P . A proof of φ from B is a finite sequence φ 1 , φ 2 , … , φ p such that φ p = φ and, for each k ∈ { 1 , 2 , … , p } , φ k is either an axiom, or an element of B , or is obtained by application of the inference rule on formulas φ ℓ where ℓ < k . Then, B ⊢ Δ φ is defined by the existence of a proof of φ from B .

Proposition 12

The formal system S Δ H is sound for ( Δ L P , ⊨ ) : for every finite set B of wffs of S Δ H and every φ ∈ L S Δ H , if B ⊢ Δ φ then B ⊨ φ .

Proof Sketch of proof.

The soundness is proven in the usual way. First, it is shown that every axiom of S Δ H is a tautology of ( Δ L P , ⊨ ) . Then, the soundness of modus ponens is shown: if I J is a model of φ and of φ → ψ (for φ and ψ , two wffs) then I J is a model of ψ . Using these two results, it is shown by mathematical induction that, if φ 1 , φ 2 , … , φ p is a proof of φ from B and I J ⊨ B then I J ⊨ φ k for each k ∈ { 1 , 2 , … , p } . So, I J ⊨ φ (since φ = φ p ). Therefore, if B ⊢ Δ φ then B ⊨ φ .

4.3. Completeness of S Δ H for ( Δ L P , ⊨ )

Proposition 13

The formal system S Δ H is complete for ( Δ L P , ⊨ ) : for every finite set B of wffs of S Δ H and every φ ∈ L S Δ H , if B ⊨ φ then B ⊢ Δ φ .

The proof of this result is given in Appendix Section A.3.

5. Algorithmic Issues

This section explores two algorithmic aspects of satisfiability in Δ L P . First, it is shown that the problem SAT Δ of satisfiability in Δ L P is NP-complete. Second, a semantic tableaux algorithm to test the satisfiability of a formula is presented.

5.1. Satisfiability Checking in ( Δ L P , ⊨ ) is NP-Complete

Let SAT Δ be the decision problem which, given a formula φ of ( Δ L P , ⊨ ) , determines whether φ is satisfiable. The problem SAT Δ is NP-complete. It is shown by proving that SAT Δ is in NP, then that it is NP-hard. The detailed proof is given in Appendix Section A.4.

5.2. A Semantic Tableaux Algorithm for Satisfiability Checking in ( Δ L P , ⊨ )

Semantic tableaux form a family of methods for satisfiability checking applicable to many logics (e.g., propositional logic and first order logic (Smullyan, 1995), and description logics (Baader & Sattler, 2001)). This section presents a semantic tableaux algorithm for ( Δ L P , ⊨ ) based on an adaptation of a semantic tableaux algorithm for ( L P , ⊨ ) .

5.2.1. Description of the Algorithm

Given a knowledge base B of ( Δ L P , ⊨ ) and φ ∈ Δ L P , the deduction test “ B ⊨ φ ?” is equivalent to the test of unsatisfiability of ⋀ B ∧ ¬ φ . So, deduction amounts to satisfiability checking.

The input of the algorithm is a formula φ of ( Δ L P , ⊨ ) . Its output is the answer to the question “Is φ satisfiable?”

The first step of the algorithm consists in putting φ in NFNF (connectives ∧ and ∨ , connective-free subformulas of the form a v , a ∈ V , v ∈ D 0 ): the result of this step is a formula ψ under NFNF such that φ ≡ ψ .

The second step of the algorithm is the development of a tree T r whose nodes are labeled by ( Δ L P , ⊨ ) formulas. A branch of such a tree is frequently assimilated in the following with the set B of the formulas labeling the nodes of this branch.

The tree T r of formulas is developed in the following way. Initially, T r has only one node labeled by ψ . Then, the following modifications of T r are applied (the algorithm is non-deterministic: the order of application of these modifications changes neither the termination nor the result but has an impact on the computing time):

(A)

If a branch B of T r contains a conjunction χ 1 ∧ … ∧ χ p such that for at least one k ∈ { 1 , … , p } , χ k ∉ B , then the tree is updated by extending B with every χ k ∉ B : the new value of the branch is B ∪ { χ 1 , … , χ p } .

(B)

If a branch B of T r contains a disjunction χ 1 ∨ … ∨ χ p such that for every k ∈ { 1 , … , p } , χ k ∉ B , then the branch is “forked” in p branches B k = B ∪ { χ k } .

The development of a branch B is stopped if B contains two literals a v and a w with v ≠ w , and then B is said to end with the clash { a v , a w } . It is also stopped if neither (A) nor (B) apply to the branch. In both cases, B is said complete.

The algorithm stops when every branch of T r is complete, and returns “ φ is unsatisfiable” if every branch ends with a clash and “ φ is satisfiable” otherwise.

5.2.2. Properties of the Algorithm

This algorithm always terminates (Proposition 14) and returns the expected result (according to Propositions 15 and 16). The proofs of these results are given in Appendix Section A.5.

Proposition 14

The tableau algorithm described in Section 5.2.1 always terminates.

Proposition 15

If the algorithm of Section 5.2.1 ends with a clash in every branch, then φ is unsatisfiable.

Proposition 16

If φ ∈ Δ L P is unsatisfiable then every complete tree T r derived from the algorithm of Section 5.2.1 ends with a clash.

6. Application to CBR

The study of the logic ( Δ L P , ⊨ ) has been motivated by a notation used in CBR, a syntax that has not been associated with a semantics before. Now, this section presents an application of this logic to CBR that is centered on the notion of adaptation rule. Section 6.1 introduces an example of adaptation problem in CBR that can be solved thanks to the application of an adaptation rule. Section 6.2 describes the representation of adaptation rules. Such a rule is based on a formula of ( Δ L P , ⊨ ) and the handling of a rule is based on the notion of application of a variation formula on a propositional formula which is described in Section 6.5. This requires the notion of ceteris paribus which is introduced before, in Section 6.4, and this latter requires the notion of invariant variables of a formula, introduced even before, in Section 6.3. Then, the application of an adaptation rule on the example is described (Section 6.6). From this study, an algorithm for performing CBR (including retrieval and adaptation) based on the notion of adaptation rules is presented (Section 6.7). Finally, an open problem related to the composition of adaptation rules is presented in Section 6.8.

6.1. Introduction of an Example

An example in the cooking domain is considered: a problem represents a query of recipe and a solution, a recipe. The problems and solutions are assumed to be expressed in propositional logic. It is assumed in this example that the domain knowledge is empty: DK = ⊤ . The adaptation problem is ( c s , x tgt ) where

c s is the source case of a salad recipe, with batavia lettuce, duck filet, tomatoes, olive oil, and vinegar:

c s = rSalad ∧ {{i{BataviaLettuce}}} ∧ {{i{DuckFilet}}} ∧ {{i{Tomato}}} ∧ {{i{OliveOil}}} ∧ {{i{Vinegar}}} ∧ n o t h i n g e l s e

where rSalad is read “salad recipe,” iSomething , “recipe with the ingredient ‘something”’ and n o t h i n g e l s e is a notation for the conjunction of negative literals ¬ a such that a cannot be deduced from the start of the formula: α ∧ n o t h i n g e l s e ≡ α ∧ ⋀ { ¬ a | a ∈ V and α ⧸ ⊨ DK a } . In particular, c s ⊨ DK ¬ {{i{Garlic}}} . It can be noticed that c s is a complete cube of propositional logic.

x tgt is the target problem “I want a recipe of salad with tomatoes, lemon juice but no garlic.”:

x tgt = rSalad ∧ {{i{Tomato}}} ∧ {{i{LemonJuice}}} ∧ ¬ {{i{Garlic}}}

Knowing the adaptation problem ( c s , x tgt ) makes it possible to partition V in { V P , V S } : V P = V ( x tgt ) = { rSalad , {{i{Tomato}}} , {{i{LemonJuice}}} , {{i{Garlic}}} } and V S = V ∖ V P . Therefore, c s can be written c s = x s ∧ y s with

x s = rSalad ∧ {{i{Tomato}}} ∧ ¬ {{i{LemonJuice}}} ∧ ¬ {{i{Garlic}}} y s = {{i{BataviaLettuce}}} ∧ {{i{DuckFilet}}} ∧ {{i{OliveOil}}} ∧ {{i{Vinegar}}} ∧ …

(“ … ” corresponds to the conjunction of literals ¬ a where a ∈ V S and a is not a positive literal of y s ).

An itemset I is also considered, that is obtained by an itemset extraction system (e.g., a frequent closed itemset system, see, e.g., Zaki and Hsiao (2002)) for the adaptation knowledge learning. Such an itemset contains a finite set of literals a v indicating “simultaneous” variations between cases and is interpreted by the conjunction φ of its elements. φ can be written as a cube of ( Δ L P , ⊨ ) : if there are several literals a v 1 , a v 2 , …built with the same variable a that occur in φ , it can be shown that they can be replaced with a sole a v (e.g., a + ∧ a ≠ ≠ ∧ b 1 ∙ ∧ b = ≡ a + ∧ b = 1 ). In the example, the following formula is considered:

φ = rSalad = 1 ∧ {{i{Vinegar}}} − ∧ {{i{LemonJuice}}} + ∧ {{i{Salt}}} +

The itemset I from which φ is built reflects the fact that there is a sufficient number of ordered pairs of salad recipes with vinegar in the first recipe but not in the second one, and lemon juice and salt in the second one but not in the first one. Therefore, if φ is interpreted as an adaptation rule, then applicability and application of φ on the adaptation problem ( ( x s , y s ) , x tgt ) have to be studied.

6.2. Representing an Adaptation Rule

An adaptation rule is defined as a pair AR = ( φ , C ) where φ ∈ Δ L P and C is a nonnegative real number called cost of AR .

What does it mean that AR is applicable to an adaptation problem ( ( x s , y s ) , x tgt ) and how can the result of this application be defined? To answer these questions, a mapping is considered that associates to ( α , φ , γ ) ∈ L P × Δ L P × L P a formula appl ( α , φ , γ ) ∈ L P , the application on α of φ under constraint γ . This mapping is defined and studied further. Since the source cases and the target problem have to be considered with the domain knowledge DK , the following formula will be computed:

β = appl ( DK ∧ x s ∧ y s , φ , DK ∧ x tgt )

(11)

If β ⊨ ⊥ then AR is said to be non-applicable to the adaptation problem. Else, this result can be written β ≡ DK ∧ x tgt ∧ y tgt where y tgt is the solution proposed for x tgt by application of AR for this adaptation problem.

CBR is usually a hypothetical inference and adaptation does not necessarily produce a correct solution to the target problem. In particular, the application of an adaptation rule AR = ( φ , C ) may output an incorrect solution. In order to make a selection among a set of adaptation rules applicable to the same adaptation problem, C is used: the cost associated with a rule is indicative of the plausibility of the application of this rule. The higher the C is, the least the confidence on the application of the rule will be. For instance, this can be interpreted in a probabilistic setting: if P estimates the probability that a rule produces a correct result (under some given probability distribution), then C = − log P could be a reasonable choice.

Thus, the representation of an adaptation rule amounts to the definition of the appl mapping, which requires preliminary definitions presented in the next two sections.

Before that, a preliminary remark on the representation of source cases ( x s , y s ) and on adaptation rules ( φ , C ) is made: although the study that follows makes no theoretical restriction on the form of source cases and adaptation rules, a reasonable assumption is that x s , y s , and φ are cubes, and that justifies that these situations are considered with some importance. Since a source case ( x s , y s ) usually represents a specific problem-solving episode, it means that every (problem or solution) variable a is assigned a Boolean value for this case: either x s ∧ y s ⊨ a or x s ∧ y s ⊨ ¬ a , so x s and y s can both be written as cubes. For φ , if it is obtained by a frequent itemset extraction system, then φ = ⋀ I for an itemset I which is a set of literals a v , and so, φ is a cube.

6.3. Invariant Variables of a Variation Formula

In this section, the variables that leave a formula unchanged are defined. The subset Inv ( φ ) of V is defined using the alternative definition of the semantics of ( Δ L P , ⊨ ) introduced in Section 3.2.2. The idea is that a ∈ Inv ( φ ) means that the value of ω ( a ) does not influence the satisfiability of φ by ω , for any ω ∈ Δ Ω alt . Formally, this leads to the following definition:

Definition 6

For ω ∈ Δ Ω alt , a ∈ V and v ∈ D 0 , ω [ a v ] ∈ Δ Ω alt is defined by ω [ a v ] : x ∈ V ↦ { v if x = a ω ( x ) else .

For φ ∈ Δ L P , the set of invariant variables of φ is

Inv ( φ ) = { a ∈ V | forevery ω ∈ M alt ( φ ) and every v ∈ D 0 , ω [ a v ] ⊨ alt φ }

For example,

if V = { a , b , c } and φ = ( a + ∧ b = ) ∨ ( a + ∧ b + ) ∨ ( a + ∧ b − ) then Inv ( φ ) = { b , c }

(12)

This notion is independent from syntax: if φ ≡ ψ then Inv ( φ ) = Inv ( ψ ) . It can be shown, using Lemma 1, that if a variable x does not occur in φ then it is invariant. Thus:

V ∖ V ( φ ) ⊆ Inv ( φ ) ⊆ V

(13)

As example (12) shows, a variable occurring in φ can be invariant for φ . The following proposition shows that a formula transformation makes it possible to link more tightly non-occurrences of variables to Inv ( φ ) .

Proposition 17

For every φ ∈ Δ L P , there exists φ ′ ∈ Δ L P such that φ ≡ φ ′ and Inv ( φ ) = V ∖ V ( φ ′ ) .

Proof.

First, the case where Inv ( φ ) = ∅ is considered. In this case, the result is immediately verified with φ ′ = φ as an immediate consequence of (13).

Then, the case where Inv ( φ ) = { a 1 } is considered. φ can be put under the form of a disjunction of complete cubes: φ ≡ φ 0 with φ 0 = ⋁ ω ∈ M alt ( φ ) φ ω where φ ω = ⋀ x ∈ V x ω ( x ) . Let ω ∈ M alt ( φ ) . By definition of Inv ( φ ) , ω [ a 1 v ] ∈ M alt ( φ ) , for all v ∈ D 0 . Therefore, as soon as a φ ω occurs in the disjunction φ 0 , every φ ω [ a 1 v ] for v ∈ D 0 occur in φ 0 . Then, by repeating and gathering elements in the disjunction (which is possible since ∨ is associative and commutative modulo logical equivalence and ψ ≡ ψ ∨ ψ for every formula ψ ), it yields that:

φ 0 ≡ ⋁ ω ∈ M alt ( φ ) ⋁ v ∈ D 0 ⋀ x ∈ V x ω [ a 1 v ] ( x ) ≡ ⋁ ω ∈ M alt ( φ ) ⋁ v ∈ D 0 [ a 1 ω [ a 1 v ] ( a 1 ) ∧ ⋀ x ∈ V ∖ { a 1 } x ω [ a 1 v ] ( x ) ] ≡ ⋁ ω ∈ M alt ( φ ) ⋁ v ∈ D 0 [ a 1 v ∧ ⋀ x ∈ V ∖ { a 1 } x ω ( x ) ] ≡ ⋁ ω ∈ M alt ( φ ) [ ⋀ x ∈ V ∖ { a 1 } x ω ( x ) ] ∧ ⋁ v ∈ D 0 a 1 v ≡ ⋁ ω ∈ M alt ( φ ) [ ⋀ x ∈ V ∖ { a 1 } x ω ( x ) ] since ⋁ v ∈ D 0 a 1 v ≡ ⊤

Let φ 1 be the last formula of the equivalence sequence above. Because a 1 ∉ V ( φ 1 ) and φ 1 ≡ φ , the proposition is proven with φ ′ = φ 1 .

In the case where Inv ( φ ) = { a 1 , a 2 , … , a p } , the process above can be applied on φ in order to obtain φ 1 such that a 1 does not occur in φ 1 , then, by repeating it with the set of variables V ∖ { a 1 } on φ 1 , the formula φ 2 is obtained, φ 2 being a formula equivalent to φ with no occurrence neither of a 1 nor of a 2 . Then, the process is repeated to result in a formula φ p equivalent to φ with no occurrence in Inv ( φ ) . With φ ′ = φ p , this concludes the proof of the proposition.

The particular case of the following proposition will be useful in the remainder of the article.

Proposition 18

If φ is a cube of ( Δ L P , ⊨ ) then Inv ( φ ) = V ∖ V ( φ ) .

Proof.

In this proof, for a cube φ , φ [ a v ] is a cube such that if a ∉ V ( φ ) then φ [ a v ] = φ ∧ a v , else, φ [ a v ] is obtained by replacing the conjunct a w of φ by a v . Since Inv ( φ ) ⊇ V ∖ V ( φ ) (cf. (13)), it is sufficient to show that if a ∈ Inv ( φ ) then a ∉ V ( φ ) , which will be proven by contraposition. Let a ∈ V ( φ ) . Let v ∈ D be such that a v is a literal of φ having a as variable. Let v 0 ∈ D 0 be such that a v 0 ⊨ a v (if v is a primitive variation symbol, v 0 = v , else, there are several possible choices for v 0 , e.g., if v = ≠ ≠ then v 0 = + ou v 0 = − can be chosen). Let w ∈ D 0 ∖ { v 0 } . Then φ [ a v 0 ] ⊨ a v 0 and φ [ a w ] ⊭ a v 0 (because, by hypothesis on the cubes, a variable occurs at most once in a cube which involves that cubes are satisfiable). Therefore, φ [ a v 0 ] ≢ φ [ a w ] and so a ∉ Inv ( φ ) .

6.4. Operator Ceteris Paribus

Consider the formula a + : it indicates that a “goes” from 0 to 1 , the other variables being free to vary in any way. So, if V = { a , b } then M ( a + ) = { ( a ¯ b ¯ , a b ¯ ) , ( a ¯ b ¯ , a b ) , ( a ¯ b , a b ¯ ) , ( a ¯ b , a b ) } . It appears useful in some cases to express for example that a goes from 0 to 1 , the other variables remaining unchanged. For this purpose, this will be expressed by a formula cp ( a + ) that, with the example with two variables, gives M ( cp ( a + ) ) = { ( a ¯ b ¯ , a b ¯ ) , ( a ¯ b , a b ) } : in the models of this formula, b “stays” at 0 or “stays” at 1 ( cp stands for ceteris paribus, i.e., “All things being equal”), in other terms, cp ( a + ) ⊨ b = . In this example, b is a variable whose interpretation does not change the interpretation of φ : b ∈ Inv ( φ ) .

More generally, an operator cp is searched for such that, for φ , ψ ∈ Δ L P :

cp ( φ ) ⊨ φ

(14)

for all x ∈ Inv ( φ ) , cp ( φ ) ⊨ x =

(15)

if φ ≡ ψ then cp ( φ ) ≡ cp ( ψ )

(16)

if φ is satisfiable then cp ( φ ) is also satisfiable

(17)

The following definition of cp is proposed and then, it is proven that it satisfies these properties and that cp ( φ ) is the most general formula (according to ⊨ ) satisfying these properties.

Definition 7

cp is the mapping from Δ L P to Δ L P defined, for φ ∈ Δ L P by

cp ( φ ) = φ ∧ ⋀ { x = | x ∈ Inv ( φ ) }

Proposition 19

cp satisfies (14), (15), (16), and (17). Moreover, if φ ′ satisfies these properties then φ ′ ⊨ cp ( φ ) .

Proof.

Equations (14), (15), and (16) follow immediately from the definition.

Equation (17) can be proven in the following way. Suppose φ is satisfiable. Then it is also satisfiable according to the alternative definition of the semantics: there exists ω ∈ Δ Ω alt such that ω ⊨ alt φ . Let a 1 , a 2 ,…, a p be such that Inv ( φ ) = { a 1 , a 2 , … , a p } . Let ω ′ = ω [ a 1 = 1 ] [ a 2 = 1 ] … [ a p = 1 ] . By definition of Inv ( φ ) , ω ′ ⊨ alt φ . Besides, ω ′ ⊨ alt a k = 1 for all k ∈ { 1 , 2 , … , p } and so ω ′ ⊨ alt ⋀ { x = 1 | x ∈ Inv ( φ ) } . Now, for every variable a , a = 1 ⊨ a = . Therefore, ω ′ ⊨ alt ⋀ { x = | x ∈ Inv ( φ ) } . So, ω ′ ⊨ alt cp ( φ ) and so, cp ( φ ) is satisfiable.

Now, let φ ′ ∈ Δ L P verifying the properties (14), (15), (16), and (17) of cp ( φ ) . Then, according to (14) and (15), φ ′ ⊨ φ ∧ ⋀ { x = | x ∈ Inv ( φ ) } = cp ( φ ) .

An immediate consequence of Proposition 18 is:

if φ is a cube then cp ( φ ) = φ ∧ ⋀ x ∈ V ∖ V ( φ ) x =

(18)

Moreover, the models of cp ( ⊤ ) are the I I for I ∈ Ω .

It can be noted that cp is non-monotonic in the sense that for some φ , φ ⊨ ψ and cp ( φ ) ⊭ cp ( ψ ) . For example, a + ⊨ ⊤ and cp ( a + ) ⊭ cp ( ⊤ ) .

A practical issue is raised with this operator: for φ ∈ Δ L P , | cp ( φ ) | is in O ( | φ | + n ) where n = | V | and this may involve a long computing time. This problem turns theoretical if the logical framework is extended to an infinite set of variables: the definition of cp given above cannot be applied, formulas being necessarily of finite sizes. A future work to address this issue will be the study of a possible extension of the logic by a connective cp (rather than an operator cp ).

It is sometimes useful to restrain the ceteris paribus to a predefined set of variables, hence the following definition.

Definition 8

Let W ⊆ V and φ ∈ Δ L P . The ceteris paribus of φ restrained to the set of variables W is:

cp W ( φ ) = φ ∧ ⋀ { x = | x ∈ Inv ( φ ) ∩ W }

And, of course, cp V ( φ ) = cp ( φ ) .

6.5. Applying a Variation Formula to a Propositional Formula

This section aims at defining a notion of application of a formula φ ∈ Δ L P to a formula α ∈ L P , given an integrity constraint γ ∈ L P on the result.

The application of φ on α under constraint γ is denoted appl ( α , φ , γ ) in the following (as mentioned in Section 6.2). In order to reach its definition, first, a formula transf ( α , φ , γ ) ∈ Δ L P is considered, called the transformation of α by φ under constraint γ , and whose result (its right part, obtained by application of the operator R ) will be appl ( α , φ , γ ) = R ( transf ( α , φ , γ ) ) .

The three following conditions are proposed for an I J ∈ Δ Ω to be a model of transf ( α , φ , γ ) : I ⊨ α , I J ⊨ φ and J ⊨ γ . These three conditions can be written as one:

I J ⊨ ( α ▹ γ ) ∧ φ

(19)

Is this condition sufficient? To answer this question, let us consider the following example: α = a ∧ ¬ b ∧ c , φ = a − ∧ b + , and γ = ⊤ . If (19) was a necessary and sufficient condition for I J ⊨ transf ( α , φ , γ ) then appl ( α , φ , γ ) would be equivalent to R ( φ ) , that is, to ¬ a ∧ b . So, whether α ⊨ c or α ⊨ ¬ c would not change the application of φ on α . On the contrary, it is assumed that if a variable (in this example c ) is invariant in φ , its value should not be changed by the transformation, hence the use of the ceteris paribus (and an a posteriori justification of its study): so, it is assumed that I J ⊨ cp ( φ ) . The idea is that the formula φ represents in a compact manner a transformation and that when it expresses nothing about a variable x , this latter is unchanged by the transformation: if x ∈ Inv ( φ ) and α ⊨ x (resp. α ⊨ ¬ x ) then, with β = appl ( α , φ , γ ) , β ⊨ x (resp. β ⊨ ¬ x ). This leads to the following definition:

Definition 9

For φ ∈ Δ L P and α , γ ∈ L P , the transformation of α by φ under constraint γ is defined by:

transf ( α , φ , γ ) = ( α ▹ γ ) ∧ cp ( φ )

The application of φ on α under constraint γ is the result of this transformation:

appl ( α , φ , γ ) = R ( transf ( α , φ , γ ) )

φ is said to be applicable on α under constraint γ if appl ( α , φ , γ ) ⊭ ⊥ . Two necessary (but not sufficient) conditions of applicability are α ∧ L ( φ ) ⊭ ⊥ and R ( φ ) ∧ γ ⊭ ⊥ .

Despite the use of the ceteris paribus, if α , φ , and γ contain few variables (wrt to | V | ), the computation of appl ( α , φ , γ ) can be performed without considering all the variables of V , as shown in the following proposition:

Proposition 20

Let α , γ ∈ L P and φ ∈ Δ L P , and let W = V ( α ) ∪ V ( φ ) ∪ V ( γ ) . Then

appl ( α , φ , γ ) ≡ R ( ( α ▹ γ ) ∧ cp W ( φ ) )

Proof.

Let β 1 = appl ( α , φ , γ ) = R ( ( α ▹ γ ) ∧ cp ( φ ) ) and β 2 = R ( ( α ▹ γ ) ∧ cp W ( φ ) ) . The goal is to prove that β 1 ≡ β 2 .

Since cp ( φ ) ⊨ cp W ( φ ) , it can be deduced that β 1 ⊨ β 2 (in particular because if ψ ⊨ ψ ′ then R ( ψ ) ⊨ R ( ψ ′ ) for every ψ ∈ Δ L P ).

Let us show that β 2 ⊨ β 1 . Let J ∈ M ( β 2 ) : what remains to be shown is that J ⊨ β 1 . By definition of β 2 , there exists I ∈ Ω such that I J ⊨ ( α ▹ γ ) ∧ cp W ( φ ) . Then, let I ′ ∈ Ω defined (for x ∈ V ) by I ′ ( x ) = { I ( x ) if x ∈ W J ( x ) else . It will be shown that I ′ J ⊨ ( α ▹ γ ) ∧ cp ( φ ) , which implies that J ⊨ β 2 . For this purpose, it is sufficient to show the following assertions: (A1)

I ′ J ⊨ α ▹ γ ;

(A2)

I ′ J ⊨ φ ;

(A3)

For all x ∈ Inv ( φ ) , I ′ J ⊨ x = .

Because the only difference between I and I ′ concerns variables that are not in V ( α ) (since they are not in W ) and because I ⊨ α , it yields that I ′ ⊨ α . As J ⊨ γ , (A1) holds.

Similarly, the only difference between I J and I ′ J concerns variables that are not in V ( φ ) (since they are not in W ) and because I J ⊨ φ , it yields that I ′ J ⊨ φ , hence (A2).

Let x ∈ Inv ( φ ) . To prove (A3), it is sufficient to prove that I ′ ( x ) = J ( x ) . If x ∉ W , by definition of I ′ , this holds. If x ∈ W , x ∈ Inv ( φ ) ∩ W , so cp W ( φ ) ⊨ x = (according to Definition 8). As I J ⊨ cp W ( φ ) , I J ⊨ x = , that is, I ( x ) = J ( x ) . Now, I ′ ( x ) = I ( x ) since x ∈ W . Therefore, I ′ ( x ) = J ( x ) , which proves (A3) and finishes the proof.

The following proposition gives a way to compute in O ( | V ( α ) | + | V ( φ ) | + | V ( γ ) | ) the application of φ on α under constraint γ when α and γ are cubes and φ is a primitive cube.

Proposition 21

Let α and γ be two cubes of ( L P , ⊨ ) and φ be a primitive cube of ( Δ L P , ⊨ ) . Let W = V ( α ) ∪ V ( φ ) ∪ V ( γ ) . Thus, it is possible to write α ≡ ⋀ a ∈ W ℓ ( a ) , γ ≡ ⋀ a ∈ W p ( a ) , and φ ≡ ⋀ a ∈ W m ( a ) ▹ n ( a ) , where ℓ ( a ) , m ( a ) , n ( a ) and p ( a ) belong to { a , ¬ a , ⊤ } , for every a ∈ W . It can be noted that a ∈ V ( α ) iff ℓ ( a ) ≠ ⊤ , a ∈ V ( γ ) iff p ( a ) ≠ ⊤ and a ∈ V ( φ ) iff m ( a ) ≠ ⊤ or (equivalently) n ( a ) ≠ ⊤ (since φ is a primitive cube).

For a ∈ W , f ( a ) ∈ { a , ¬ a , ⊥ } is defined in the following way:

If ℓ ( a ) ∧ m ( a ) ⊨ ⊥ , n ( a ) ∧ p ( a ) ⊨ ⊥ or ( ℓ ( a ) ∧ p ( a ) ⊨ ⊥ and m ( a ) = n ( a ) = ⊤ ) then f ( a ) = ⊥ . Otherwise, f ( a ) = { ℓ ( a ) if ℓ ( a ) ≠ ⊤ and m ( a ) = n ( a ) = ⊤ p ( a ) if ℓ ( a ) = ⊤ and m ( a ) = n ( a ) = ⊤ n ( a ) else

Then appl ( α , φ , γ ) ≡ ⋀ a ∈ W f ( a ) .

Therefore, φ is applicable on α under constraint γ iff for all a ∈ W , f ( a ) ≠ ⊥ .

Proof Sketch of proof.

The idea of the proof consists in computing appl ( α , φ , γ ) for every variable a ∈ W . Indeed, transf ( α , φ , γ ) can be written as a conjunction over a ∈ W as shown below:

transf ( α , φ , γ ) = ( α ▹ γ ) ∧ cp ( φ ) ≡ ⋀ a ∈ W ( ℓ ( a ) ▹ p ( a ) ) ∧ φ ( a ) where φ ( a ) = { m ( a ) ▹ n ( a ) if a ∈ V ( φ ) a = else

The complete proof consists in considering all the possibilities for a variable a ∈ W , depending on whether a belongs or not to V ( α ) , to V ( φ ) and to V ( γ ) . So, there are 2 3 = 8 cases to consider, but since a ∈ W , one of these cases is removed. Below, only two cases are detailed:

Case 1:

a ∈ V ( α ) , a ∉ V ( φ ) and a ∉ V ( γ ) . Then ℓ ( a ) ≠ ⊤ and m ( a ) = n ( a ) = p ( a ) = ⊤ . So:

( ℓ ( a ) ▹ p ( a ) ) ∧ φ ( a ) = ( ℓ ( a ) ▹ ⊤ ) ∧ a = ≡ ℓ ( a ) ▹ ℓ ( a )

Case 2:

a ∈ V ( α ) ∩ V ( γ ) ∩ V ( φ ) . Then ⊤ ∉ { ℓ ( a ) , m ( a ) , n ( a ) , p ( a ) } , so:

( ℓ ( a ) ▹ p ( a ) ) ∧ φ ( a ) = ( ℓ ( a ) ▹ p ( a ) ) ∧ ( m ( a ) ▹ n ( a ) ) ≡ { ℓ ( a ) ▹ n ( a ) if ℓ ( a ) = m ( a ) and p ( a ) = n ( a ) ⊥ else

The five remaining cases are studied similarly and this leads to the conclusion of the proposition.

Finally, the following proposition makes it possible to compute appl ( α , φ , γ ) where φ is a primitive cube but where α and γ are any propositional formulas, using transformations under disjunctive normal form of α and γ and Proposition 21.

Proposition 22

Let α , α 1 , α 2 , β , β 1 , β 2 ∈ L P and φ ∈ Δ L P . The following equivalences apply:

appl ( α 1 ∨ α 2 , φ , γ ) ≡ appl ( α 1 , φ , γ ) ∨ appl ( α 2 , φ , γ )

(20)

appl ( α , φ , γ 1 ∨ γ 2 ) ≡ appl ( α , φ , γ 1 ) ∨ appl ( α , φ , γ 2 )

(21)

Proof.

Equivalence (20) can be proven using Proposition 6(4), Section 3.3.4, and the following sequence of equivalences:

transf ( α 1 ∨ α 2 , φ , γ ) = ( ( α 1 ∨ α 2 ) ▹ γ ) ∧ cp ( φ ) ≡ ( ( α 1 ▹ γ ) ∧ cp ( φ ) ) ∨ ( ( α 2 ▹ γ ) ∧ cp ( φ ) ) ≡ transf ( α 1 , φ , γ ) ∨ transf ( α 2 , φ , γ )

Equivalence (21) can be proven in a similar way.

6.6. Application of an Adaptation Rule to the Example

Consider the adaptation problem ( ( x s , y s ) , x tgt ) and the formula φ of Section 6.1, along with the adaptation rule AR = ( φ , C ) where C is chosen arbitrarily. By applying (11) to this example, a satisfiable β ∈ L P is obtained, and verifies β ≡ DK ∧ x tgt ∧ y tgt with

y tgt = {{i{BataviaLettuce}}} ∧ {{i{DuckFilet}}} ∧ {{i{OliveOil}}} ∧ {{i{LemonJuice}}} ∧ {{i{Salt}}} ∧ …

which is the expected result on this example (“ … ” represents a conjunction of negative literals).

6.7. An Algorithm for CBR

An approach to CBR used in particular in the system Taaable (Cordier et al., 2014), consists in performing a retrieval relying on a minimal transformation of the target problem, such that it corresponds exactly to at least one source case, then using an “inverse transformation” on a retrieved case to obtain a solution.

In the representation setting of this article, the transformation of the target problem is built thanks to adaptation rules. Assume the adaptation knowledge of a CBR system is represented by the set AK of available adaptation rules ( φ , C ) . AK may also contain the rules ( a ≠ ≠ , C ) for each problem variable a : such a rule states that, given an adaptation problem ( ( x s , y s ) , x tgt ) such that the only difference between the two problems x s and x tgt is related to the value of a , the solution y s is reused as such. The role of these additional adaptation rules ( a ≠ ≠ , C ) is to ensure that the system proposes a solution (possibly with a high adaptation cost).

In order to implement the proposed algorithm, the transformations considered apply to the target problem, so are based on the rule AR − 1 = ( φ − 1 , C ) for each AR = ( φ , C ) ∈ AK (where φ − 1 is the inverse of φ , as defined in Definition 3). Assuming that costs are additive, the retrieval returns not only an ( x s , y s ) ∈ CB but also a sequence of rules AR 1 − 1 , AR 2 − 1 , … , AR q − 1 that relates the target problem to this retrieved case. Formally, let x 0 , x 1 , …, x q defined by x 0 = DK ∧ x tgt and x i = appl ( x i − 1 , φ i − 1 , ⊤ ) , for i ∈ { 1 , 2 , … , q } and AR i = ( φ i , C i ) . Then, the retrieved case is such that x s ∧ y s ⊨ DK x q and such that the transformation cost ∑ i = 1 q C i is minimal. Algorithmically, it amounts to a best-first search in a state space where states are propositional formulas, x 0 is the initial state, the goal is to have a state that matches at least one source case (which can be done efficiently if source cases are specific), the successors of a state being obtained by inverse adaptation rules AR − 1 , and the search being controlled by the cost.

Once a source case ( x s , y s ) retrieved with an associated sequence of adaptation rules AR 1 − 1 , AR 2 − 1 ,…, AR q − 1 the idea is to apply the inverse sequence of these rules to x s ∧ y s to solve x tgt : with y q such that x s ∧ y s ≡ x q ∧ y q , y q − 1 ,…, y 0 , are computed successively: for i ∈ { q − 1 , q − 2 , … , 0 } , x i ∧ y i ≡ appl ( x i + 1 ∧ y i + 1 , φ i + 1 , x i ) . Then y tgt such that DK ∧ x tgt ∧ y tgt ≡ x 0 ∧ y 0 is a proposition of solution of x tgt , adapted in q steps from the retrieved case. It can be noted that above, the x i (resp., the y i ) are not necessarily problems (resp. solutions). For example, V ( x 0 ) ⊇ V ( DK ) and DK may contain variables from V S .

For such an adaptation to give a consistent result, the adaptation rules AR i must be applicable. This is ensured by the following proposition, in the case where x s ∧ y s , x tgt and φ i are cubes:

Proposition 23

Let α and γ be two cubes of ( L P , ⊨ ) and φ be a cube of ( Δ L P , ⊨ ) . Then:

appl ( α , φ , γ ) ⊭ ⊥ iff appl ( γ , φ − 1 , ⊤ ) ∧ α ⊭ ⊥

Proof Sketch of proof.

The conditions for the direct computation have already been seen in Proposition 21.

For the “inverse” computation, it yields that:

transf ( γ , φ − 1 , ⊤ ) ≡ ⋀ a ∈ V ( p ( a ) ▹ ⊤ ) ∧ cp ( φ − 1 ) ( a ) ⏟ τ γ , φ ( a ) where cp ( φ − 1 ) ( a ) = { n ( a ) ▹ m ( a ) if a ∈ V ( φ ) a = else

The computation of the right part of τ γ , φ ( a ) , and its conjunction with α , are done the same way it was done in the proof of Proposition 21, partitioning the set of variables according to V ( α ) , V ( φ ) and V ( γ ) .

For example, if a ∈ V ( α ) ∩ V ( φ ) ∩ V ( γ ) , ( p ( a ) ▹ ⊤ ) ∧ cp ( φ − 1 ) ( a ) = ( p ( a ) ▹ ⊤ ) ∧ ( n ( a ) ▹ m ( a ) ) .

The compatibility condition of this conjunction is n ( a ) ∧ p ( a ) ⊭ ⊥ . The right part of this term is then m ( a ) , and the compatibility condition with α is ℓ ( a ) ∧ m ( a ) ⊭ ⊥ . The same conditions are met in the direct computation.

This computation is done the same way in the six other cases, and it is easy (but tedious!) to check the equivalence: appl ( γ , φ − 1 , ⊤ ) ∧ α ⊭ ⊥ iff appl ( α , φ , γ ) ⊭ ⊥ .

It can be shown that x i ∧ y i is satisfiable for all i ∈ { 0 , 1 , … , q } by starting from the end:

( i = q )

Since, by definition, x q ∧ y q is equivalent to the complete cube x s ∧ y s and cubes are satisfiable, x q ∧ y q ⊭ ⊥ .

( i = q − 1 )

x q − 1 ∧ y q − 1 ≡ appl ( x q ∧ y q , φ q , x q − 1 ) that, according to Proposition 23, is satisfiable iff β is satisfiable, with β = appl ( x q − 1 , φ q − 1 , ⊤ ) ∧ x q ∧ y q . Now, by definition of x q , β ≡ x q ∧ x q ∧ y q ≡ x q ∧ y q , which is satisfiable (cf. case ( i = q ) ), thus β is satisfiable and hence x q − 1 ∧ y q − 1 ⊭ ⊥ .

( i = q − 2 )

x q − 2 ∧ y q − 2 ≡ appl ( x q − 1 ∧ y q − 1 , φ q − 1 , x q − 2 ) that, according to Proposition 23, is satisfiable iff β is satisfiable, with β = appl ( x q − 2 , φ q − 1 − 1 , ⊤ ) ∧ x q − 1 ∧ y q − 1 . Now, by definition of x q − 1 , β ≡ x q − 1 ∧ x q − 1 ∧ y q − 1 ≡ x q − 1 ∧ y q − 1 which is satisfiable (cf. case ( i = q − 1 ) ), thus β is satisfiable and hence x q − 2 ∧ y q − 2 ⊭ ⊥ .

( … )

( i = 0 )

x 0 ∧ y 0 ≡ appl ( x 1 ∧ y 1 , φ 1 , x 0 ) that, according to Proposition 23, is satisfiable iff β is satisfiable, with β = appl ( x 0 , φ 1 − 1 , ⊤ ) ∧ x 1 ∧ y 1 . Now, by definition of x 1 , β ≡ x 1 ∧ x 1 ∧ y 1 ≡ x 1 ∧ y 1 which is satisfiable (cf. case ( i = 1 ) ), thus β is satisfiable and hence x 0 ∧ y 0 ⊭ ⊥ .

Since DK ∧ x tgt ∧ y tgt ≡ x 0 ∧ y 0 , DK ∧ x tgt ∧ y tgt is satisfiable: adaptation gives a consistent result.

It can be noted that this algorithm can be used to solve an adaptation problem ( ( x s , y s ) , x tgt ) (when a case ( x s , y s ) has already been chosen). For this purpose, it only requires to apply the algorithm to the singleton case base CB = { ( x s , y s ) } .

A final but important remark has to be made. In the system Taaable , retrieval was based only on a minimum generalization of the literals of the target problem according to a taxonomy, that is a set of formulas a → b ( a , b ∈ V ). Such generalization, expressed with the logic developed in this article, corresponds to adaptation rules ( a − ∧ b = 1 , C ) . After that, a first raw adaptation was proposed (following the inverse of these taxonomy-based adaptation rules). Then, a rule-based adaptation using more sophisticated rules was performed. With the algorithm presented above, retrieval and adaptation are more tightly linked: once retrieval is done, adaptation just follows backward the adaptation rule chain. Therefore, the retrieval of this algorithm follows a strong version of the adaptation-guided retrieval principle (AGR; Smyth & Keane, 1996). In the usual version of AGR, the retrieved case has to be adaptable. Here, not only is it adapted, but the retrieved case is the source case that requires the least adaptation effort (measured by the costs of adaptation rules) to solve the target problem. Moreover, for this algorithm, retrieval knowledge and adaptation knowledge coincide: the rules ( φ , C ) are used both for retrieval and for adaptation.

6.8. Toward a Composition of Adaptation Rules

The algorithm of Section 6.7 relies on a sequence of applications of adaptation rules. The open issue that is raised here is the computation of a composition of adaptation rules: given two rules AR 1 and AR 2 , can a rule AR be defined such that the application of AR corresponds to the successive applications of AR 1 and AR 2 ? The composition of formulas introduced in Section 3.4 should be useful here, but no definitive answer to this question has been found at this time.

The interest in defining such a composition of rules would be to use it during the post-treatment of learning these rules. If, for example, a frequent closed itemset extraction system is used, a large number of itemsets I that can be interpreted as adaptation rules AR may be produced. If it was possible to find a minimal generating family for the composition of these rules, it would lower their number (and computing time) without changing the algorithm.

7. Discussion and Related Works

This section discusses some formalisms with connections with the logic of propositional variables presented in this article. Section 7.1 considers briefly several of these formalisms. Dynamic logics are considered separately, since they have stronger similarities with ( Δ L P , ⊨ ) . For discussing these similarities (and differences), two types of inferences are highlighted first, in Section 7.2, namely observations and actions. Then, on this basis, ( Δ L P , ⊨ ) is related with DL-PA, a dynamic logic with propositional variables (Section 7.3).

7.1. A Few Related Formalisms and Other Studies

The notion of propositional variation may evoke the notion of differences between Boolean functions that have been studied in the work of Thayse (1981). Indeed, a formula ( L P , ⊨ ) can be seen as a representation of a function from { 0 , 1 } | V | to { 0 , 1 } . In Thayse work, the differences between two Boolean variables is calculated by an exclusive or and this work leads to a differential calculus on Boolean functions inspired from studies in analysis on real numbers (Taylor developments, etc.). However, considering the original goal of this work described in this article, that is, representing variations, useful in particular for CBR, the sole use of exclusive or appears insufficient. In particular, the symmetry of ⊕ ( α ⊕ β ≡ β ⊕ α ) does not make it possible to express directed variations, for example, to distinguish going from 0 to 1 and going from 1 to 0 , whereas the variation symbols + and − makes this distinction.

The alternative definition of the semantics of ( Δ L P , ⊨ ) (Section 3.2.2) is based on the set of truth values D 0 . This motivates to study the relationships between ( Δ L P , ⊨ ) and the logic of Belnap (2019) which is also based on four truth values which are often represented by ordered pairs of Booleans. From a semantic viewpoint, the link is not straightforward since ( Δ L P , ⊨ ) is most of the time considered as a logic with two truth values (the alternative definition of the semantics has mainly been introduced for practical purpose). Moreover, the number 4 of truth values is at the basis of Belnap–Dunn logic whereas, for variation logic, it appears only as a consequence of choosing propositional logic as a starting point to build this logic: other choices could have been made, which would have led to a set of primitive variations of cardinal different from four. Now, relations between these two logics could be investigated, in particular, at an algorithmic level. This study has not been carried out and constitutes a potential future work.

7.2. Observations and Actions

The mechanisms linked to adaptation presented in Section 6 can be divided into observations and actions. The observations occur during the adaptation knowledge learning process (described in Section 2.2) during which are observed variations between source cases. Given an adaptation rule AR = ( φ , C ) and an adaptation problem ( ( x s , y s ) , x tgt ) , the application of AR on ( ( x s , y s ) , x tgt ) can be seen as an action mechanism: a plausible solution y tgt of x tgt is created, starting from ( x s , y s ) . So, assimilating a case to a state and an adaptation rule to an action, an adaptation rule can be considered as the application of an action on a state, to reach a new state (knowing that this new state is constrained by x tgt ). The application of adaptation rules is an invitation to study action-related formalisms and inferences (cf. the synthesis Dupin de Saint-Cyr et al., 2020). In this framework, the actions are considered as deterministic: if an action is applicable on a state, it generates exactly one state. The next section studies the links between a dynamic logic and ( Δ L P , ⊨ ) .

A last remark can be done. A link between observations and epistemic actions (also studied in Dupin de Saint-Cyr et al., 2020) could be considered. However, the study of the links between observations as considered here (observing variations between cases) and the epistemic actions (acting for observing and acquiring/modifying knowledge about the current state) has not appear fruitful (or not yet).

7.3. ( Δ L P , ⊨ ) and DL-PA

DL-PA (dynamic logic of propositional assignments) is a dynamic logic whose atomic programs are assignments of propositional variables, that is, expressions + a and − a for a ∈ V , corresponding to assignment of a by, respectively, 1 and 0 (Balbiani et al., 2013). Formulas of DL-PA are the propositional variables, formulas build with other formulas using the connectives of propositional logic, and the formulas of the form ⟨ π ⟩ α where π is a program and α is a formula. Programs are either atomic programs, or of one of the forms π 1 ; ; π 2 , π 1 ∪ ∪ π 2 , π * , and α ? (where π , π 1 , and π 2 are programs and α is a formula).

The semantics of a formula α is given by a subset M ( α ) of Ω and the semantics of a program π by a subset M ( π ) of Ω × Ω = Δ Ω , which suggests to study the link between DL-PA programs and ( Δ L P , ⊨ ) formulas. This semantics is defined in an usual way for propositional variables and formulas build on connectives, and for the other formulas and for the programs, in the following way (for a ∈ V , α , a formula, π , π 1 and π 2 , programs):

M ( ⟨ π ⟩ α ) = { I ∈ Ω there exists J ∈ Ω such that I J ⊨ π and J ⊨ α } M ( + a ) = { I J ∈ Δ Ω J ⊨ a and, for all b ∈ V ∖ { a } , I ( b ) = J ( b ) } M ( − a ) = { I J ∈ Δ Ω J ⊨ ¬ a and, for all b ∈ V ∖ { a } , I ( b ) = J ( b ) } M ( π 1 ; ; π 2 ) = { I K ∈ Δ Ω there exists J ∈ Ω such that I J ⊨ π 1 and J K ⊨ π 2 } M ( π 1 ∪ ∪ π 2 ) = M ( π 1 ) ∪ M ( π 2 ) M ( α ? ) = { I I | I ∈ M ( α ) }

Finally, I J ⊨ π * if there exists a sequence I 0 , I 1 , … , I p ( p ≥ 0 ) such that I 0 = I , I p = J and I k I k + 1 ⊨ π for all k ≥ 0 and k < p .

Ceteris paribus on ( Δ L P , ⊨ ) formulas is useful to establish a relationship from formulas of this logic to DL-PA programs. An operation on DL-PA programs can also be defined to establish a link in the other direction. For this purpose, it will be assumed in the remainder of this section that the set of propositional variables is finite, contrary to the assumption of a countable set of variables made in Balbiani et al. (2013).

It can be remarked that the program + a ∪ ∪ − a (for a ∈ V ) does the opposite of an assignment: even if a is assigned to a value ( 0 or 1 ) in the state preceding the application of this program, the execution of this program has for effect that a does not have any assignment after this execution. This can be generalized to a set W = { a 1 , … , a p } of variables:

unassign ( { a 1 , … , a p } ) = ( + a 1 ∪ ∪ − a 1 ) ; ; … ; ; ( + a p ∪ ∪ − a p )

The execution of unassign ( W ) has for effect that it reaches a state in which no variable of W has an assignment (so this state is a formula having at least 2 | W | models).

Table 1 gives equalities between sets of models of some formulas of ( Δ L P , ⊨ ) and set of models of some programs of DL-PA. It can be noted that, in this table, some operations of ( Δ L P , ⊨ ) correspond to constructors (syntactical elements) of DL-PA; for example, in π 1 ; ; π 2 the symbol ; ; belongs to the syntax of the logic whereas in φ 1 ; φ 2 , ; is an operator. Moreover, for α ∈ L P (which is also a formula of DL-PA), M ( α ? ) = M ( α ^ ) where α ^ is defined in Appendix Section A.4, related to the proof of the NP-completeness of SAT Δ . Finally, for α ∈ L P , φ ∈ Δ L P , and a DL-PA program π such that M ( φ ) = M ( π ) , M ( ⟨ π ⟩ α ) = L ( φ ∧ α ∙ 1 ) .

OPEN IN VIEWER

Table 1.

Relations Between Formulas of ( Δ L P , ⊨ ) and DL-PA Programs.

Let a ∈ V , φ 1 , φ 2 ∈ Δ L P , and π 1 and π 2 DL-PA programs such that M ( φ 1 ) = M ( π 1 ) and M ( φ 2 ) = M ( π 2 ) .
For each line ( φ , π ) of the following tables, M ( φ ) = M ( π ) :
φ ∈ Δ L P π : DL-PA program cp ( a ∙ 1 ) + a cp ( a ∙ 0 ) − a φ 1 ∨ φ 2 π 1 ∪ ∪ π 2 φ 1 ; φ 2 π 1 ; ; π 2	φ ∈ Δ L P π : DL-PA program a = 1 a ? ; ; + a ; ; unassign ( V ∖ { a } ) a = 0 ¬ a ? ; ; − a ; ; unassign ( V ∖ { a } ) a + ¬ a ? ; ; + a ; ; unassign ( V ∖ { a } ) a − a ? ; ; − a ; ; unassign ( V ∖ { a } )

DL-PA = dynamic logic of propositional assignments.

OPEN IN VIEWER

Table A.1.

Composition of Variations for the Computation of the Composition of Cubes.

;	⊥ D	= 0	+	−	= 1	0 ∙	∙ 0	1 ∙	∙ 1	=	≠ ≠	¬ = 0	¬ +	¬ −	¬ = 1	⊤ D
⊥ D	⊥ D	⊥ D	⊥ D	⊥ D	⊥ D	⊥ D	⊥ D	⊥ D	⊥ D	⊥ D	⊥ D	⊥ D	⊥ D	⊥ D	⊥ D	⊥ D
= 0	⊥ D	= 0	+	⊥ D	⊥ D	0 ∙	= 0	⊥ D	+	= 0	+	+	= 0	0 ∙	0 ∙	0 ∙
+	⊥ D	⊥ D	⊥ D	= 0	+	⊥ D	= 0	0 ∙	+	+	= 0	0 ∙	0 ∙	+	= 0	0 ∙
−	⊥ D	−	= 1	⊥ D	⊥ D	1 ∙	−	⊥ D	= 1	−	= 1	= 1	−	1 ∙	1 ∙	1 ∙
= 1	⊥ D	⊥ D	⊥ D	−	= 1	⊥ D	−	1 ∙	= 1	= 1	−	1 ∙	1 ∙	= 1	−	1 ∙
0 ∙	⊥ D	= 0	+	= 0	+	0 ∙	= 0	0 ∙	+	0 ∙	0 ∙	0 ∙	0 ∙	0 ∙	0 ∙	0 ∙
∙ 0	⊥ D	∙ 0	∙ 1	⊥ D	⊥ D	⊤ D	∙ 0	⊥ D	∙ 1	∙ 0	∙ 1	∙ 1	∙ 0	⊤ D	⊤ D	⊤ D
1 ∙	⊥ D	−	= 1	−	= 1	1 ∙	−	1 ∙	= 1	1 ∙	1 ∙	1 ∙	1 ∙	1 ∙	1 ∙	1 ∙
∙ 1	⊥ D	⊥ D	⊥ D	∙ 0	∙ 1	⊥ D	∙ 0	⊤ D	∙ 1	∙ 1	∙ 0	⊤ D	⊤ D	∙ 1	∙ 0	⊤ D
=	⊥ D	= 0	+	−	= 1	0 ∙	∙ 0	1 ∙	∙ 1	=	≠ ≠	¬ = 0	¬ +	¬ −	¬ = 1	⊤ D
≠ ≠	⊥ D	−	= 1	= 0	+	1 ∙	∙ 0	0 ∙	∙ 1	≠ ≠	=	¬ −	¬ = 1	¬ = 0	¬ +	⊤ D
¬ = 0	⊥ D	−	= 1	∙ 0	∙ 1	1 ∙	∙ 0	⊤ D	∙ 1	¬ = 0	¬ +	⊤ D	⊤ D	¬ = 0	¬ +	⊤ D
¬ +	⊥ D	∙ 0	∙ 1	−	= 1	⊤ D	∙ 0	1 ∙	∙ 1	¬ +	¬ = 0	¬ = 0	¬ +	⊤ D	⊤ D	⊤ D
¬ −	⊥ D	= 0	+	∙ 0	∙ 1	0 ∙	∙ 0	⊤ D	∙ 1	¬ −	¬ = 1	⊤ D	⊤ D	¬ −	¬ = 1	⊤ D
¬ = 1	⊥ D	∙ 0	∙ 1	= 0	+	⊤ D	∙ 0	0 ∙	∙ 1	¬ = 1	¬ −	¬ −	¬ = 1	⊤ D	⊤ D	⊤ D
⊤ D	⊥ D	∙ 0	∙ 1	∙ 0	∙ 1	⊤ D	∙ 0	⊤ D	∙ 1	⊤ D	⊤ D	⊤ D	⊤ D	⊤ D	⊤ D	⊤ D

Note. The box on line v and column w contains the value v ; w .

In general, every φ ∈ Δ L P can be translated into a DL-PA program π so that M ( φ ) = M ( π ) , as explained below, at least under the assumption of a finite set of variables. It must be noticed however that the proposed translation is not efficient and that there is little hope to find one that is, since the satisfiability in ( Δ L P , ⊨ ) is NP-complete whereas the satisfiability of formulas in DL-PA is EXPTIME-hard (even if this complexity is about DL-PA formulas and not programs, this is an indication of the relative complexity of inferences of the two logics).

A simple proof that φ ∈ Δ L P can be translated into π is linked to the fact that every subset of Δ Ω is representable by a program π (still under the assumption of a finite set of variables). A more constructive proof associates first to each complete cube of ( Δ L P , ⊨ ) a DL-PA program. Let ψ be a complete cube of ( Δ L P , ⊨ ) : ψ = ⋀ a ∈ V a ω ( a ) for an ω ∈ Δ Ω alt . For a ∈ V , let π a be the program

π a = { a ? ; ; + a if ω ( a ) = = 1 ¬ a ? ; ; − a if ω ( a ) = = 0 ¬ a ? ; ; + a if ω ( a ) = + a ? ; ; − a if ω ( a ) = −

With V = { a 1 , a 2 , … , a n } , let π = π a 1 ; ; π a 2 ; ; … ; ; π a n . It can be shown that M ( π ) = M ( ψ ) . More generally, every φ ∈ Δ L P can be written as a disjunction of complete cubes: φ = ψ 1 ∨ ψ 2 ∨ … ∨ ψ p . By associating to each cube ψ k a program π k as described above, it is possible to build the program π = π 1 ∪ ∪ π 2 ∪ ∪ … ∪ ∪ π p . Then M ( π ) = ⋃ k = 1 p M ( π k ) = ⋃ k = 1 p M ( ψ k ) = M ( φ ) .

So, there are strong links between ( Δ L P , ⊨ ) and DL-PA that should be studied further. It seems that ( Δ L P , ⊨ ) is more useful for observing variations (and that is why this logic has been initially defined) whereas DL-PA which, in a sense, integrates naturally the ceteris paribus, is more appropriate for acting with these variations (considering the application of an adaptation rule as the execution of a program). So, reasoning with adaptation rules could be done in ( Δ L P , ⊨ ) for their learning and with DL-PA (or one of its fragments) for their application.

8. Conclusion

CBR uses two types of knowledge. The knowledge of what holds (in a particular state) is represented by the source cases and by the domain knowledge. The knowledge of what changes is represented by retrieval and adaptation knowledge. The former type of knowledge can be expressed in well-studied formalisms, such as propositional logic. The study of formalisms for the second type of knowledge has received less attention, particularly when the tight relation between knowledge representation and reasoning is considered. The first goal of this article has been the systematic study of one of these formalisms, the logic of propositional variations which is suited when cases and domain knowledge can be represented in propositional logic. Although the logics for representing variations (such as ( Δ L P , ⊨ ) ) and dynamic logics are related, the objectives of their studies are different. For logics of variations, our first objective has been to represent this notion of variations in order to study how to draw inferences with them: starting from a notation introduced for some studies on adaptation knowledge learning, a semantics has been added to it, which has made possible to reason on variations. The second objective of this article has been to “go back” to CBR, to study the potential impact of this logic of variations, beyond its mere notation. The logic ( Δ L P , ⊨ ) has been used for representing adaptation rules for CBR and a CBR algorithm based on adaptation rules has been designed. This algorithm has the property that it retrieves the best source case, that is, the one that minimizes the adaptation effort and it is our claim that it should be quite efficient. Indeed, it is rather similar to an implementation of a CBR algorithm for the Taaable system (which does not have this property of optimal retrieval though) and that was efficient, with a case base of about 1 , 500 cases.

There are many potential future studies following this work, including the ones that are mentioned all along the paper, such as the use of the logic of propositional variations for generative adaptation. However, we will limit ourselves here to describe three directions of research that are of particular interest for us.

The first direction of research is quite obvious: it consists in studying other logics of variations, based on other formalisms than propositional logic. In particular, we are interested in using as base logic a logic of propositional closure on linear constraints (on integer and real variables), a logic studied on another (and complementary) line of work on CBR (Diebold et al., 2024). So, a variation logic based on this logic would, in particular, represent variations between two constraints. An important difference with the study presented in this article is that the set of variation symbols would not be finite, but defined by a language.

A second direction of work is the study of the implementation of ( Δ L P , ⊨ ) and its practical application to a CBR system. The complexity of the inference may be an issue here, since SAT Δ is NP-complete. One way to address this difficulty is to define a translation mechanism from SAT Δ to SAT solver and using an efficient solver for SAT (it could also be for another well-studied decision problem than SAT). Another way to address this difficulty is to consider polynomial fragments of ( Δ L P , ⊨ ) . For example, it is easy to define a Horn fragment of this variation logic and to reuse the backward chaining algorithm for the Horn fragment of propositional logic, but it remains to be proven that this algorithm remains complete.

A third direction of work is the study of links existing with proportional analogies, that is, quaternary relations between four objects a , b , c , and d that are read “ a is to b as c is to d ” and that are bound by some set of postulates (see, e.g., Prade & Richard, 2013). In the past few years, several studies have made connections between CBR and proportional analogies (e.g., Lepage & Lieber, 2018; Lieber et al., 2021), thus this may have an impact on CBR as well. An intuition behind proportional analogies is that if a quadruplet ( a , b , c , d ) is in an analogical proportion then some well-chosen transformation from a to b coincides with some well-chosen transformation from c to d . Such transformations could be represented by variation formulas, hence the link with the current study. In particular, one question that can be raised is what are the mappings τ : ( α , β ) ∈ L P 2 ↦ τ ( α , β ) ∈ Δ L P such that the quaternary relation τ ( α , β ) ≡ τ ( γ , δ ) , for α , β , γ , δ ∈ L P would define proportional analogies on ( L P , ⊨ ) ?