Logic

2 Logic

In simple terms, a logic is a language of formulas equiped with an generalization ordering called subsumption. Almost everything in Camelis is represented by formulas so that the various operations on a context can be expressed in a very uniform way. Formulas are used to describe the properties of an object, the features common to a set of objects, complex boolean queries, and updates.

Each Camelis application is given a custom logic L upon which are defined the various kinds of formulas. Each logic comes with the following elements:

a sub-language L_D of object descriptors,
a sub-language L_F of features,
a generalization ordering, the subsumption, over formulas, where f ⊑ g means that formula g is more general than formula f,
two update operations add (resp. sub) to make an object descriptor be subsumed (resp. not be subsumed) by some object descriptor (resp. by some formula).

L_D and L_F may be equal to L. The subsumption is assumed to be consistent, complete between object descriptors and features, but not necessarily fully complete. This is necessary and sufficient to ensure that no object is misclassified. The update operations may be only partially defined.

From this low-level logic, top-level formulas can be defined as follows:

an object description is a set of object descriptors, and is interpreted under the Closed World Assumption, i.e., everything not said is considered as false,
a feature is simply a feature,
a query is a boolean combination of features, where connectors are and, or, not, except, and all,
an update is a conjunction of object descriptors, negations of object descriptors, and negations of features.

Then the subsumption ordering is extended as follows:

an object description D is subsumed by a feature f if there exists an object descriptor d ∈ D such that d ⊑ f,
the subsumption of an object description D by a query q is defined according to the usual semantics of boolean connectors (e.g., D ⊑ q₁ and q₂ iff D ⊑ q₁ and D ⊑ q₂, and D ⊑ not q iff D ¬ ⊑q),
let F and G be two disjunctions of formulas, F is subsumed by G if for every f ∈ F, there exists g ∈ G such that f ⊑ g,
let F and G be two conjunctions of formulas, F is subsumed by G if for every g ∈ G, there exists f ∈ F such that f ⊑ g,
let f and g be two formulas, the negation not f is subsumed by the negation not g if g ⊑ f.

Finally the update operation is extended as follows:

the update of D by (u₁ and u₂) is equal to the successive update of D by u₁ and u₂,
the update of D by d is obtained by applying the update add(d',d) to each descriptor d' in D when defined, and by adding the descriptor d to D when no addition was defined,
the update of D by f is obtained by applying the update sub(d',f) to each descriptor d' in D when defined, and by removing it from D otherwise.

Logics may also be equipped with the operation axiom that takes two features f,g, and makes sure that f ⊑ g. This enables some customization of the logic after it has been defined and linked with Camelis. Depending on the semantics of the logic, the introduction of one axiom may produce several subsumption relations or none.