Previous Up Next

Appendix A  How to read appendices

Each appendix is a class of logic functors. Then each section describes a different logic functor. The section title gives the name and arity of the logic functor in the form “Name/arity”. In the case of a combinator, the name is equated to a logic functor composition, where the symbol λ introduces each parameter of the combinator, and the symbol μ defines it as a fixpoint (recursive structures). In some cases a logic functor is defined as an extension of a combinator, i.e., some parts of the logics are redefined. In this case, the symbol ⊇ is used instead of = between the name and the combinator definition.

The following section shows the structure and contents of each section describing a functor.

A.1  Name/arity [=/⊇ combinator]

The logic functor is first introduced by a short description of its formulas, interpretations, and main roles in composing logics. The following subsections are always present unless the logic functor is equal to a combinator. Whenever a logic element (e.g., operation, property) is not given, the default definition is assumed (see Chapter 2).

A.1.1  Parameters

The parameters of the functor are given a name and a type. Most often these parameters are sub-logics, but are sometimes non-logical parameters (e.g., an alphabet for strings).

A.1.2  Syntax

The syntax of formulas AS is formally defined. TELL-formulas, and ASK-formulas may be defined as subsets of AS.

A.1.3  Semantics

The interpretation domain I and the satisfaction relation ⊨ are formally defined. In some cases, the semantics can be defined in term of M instead of the satisfaction relation ⊨. The ordering on interpretations ≤ may also be defined.

A.1.4  Operations

Non-default operations are here defined as algorithms. This represents the executable part of a logic functor.

A.1.5  Properties

The behaviour of properties is given in the form of a theorem relating a property and the properties of sub-logics. A theorem is always accompanied by a proof, except when it is trivial given the definition of the property and definitions of the logic functor. Some properties can be considered as true, even if no theorem is given, when it is trivially true: e.g., the conjunction and disjunction are always consistent and complete when totally undefined; or when a property is a weakening of another property that is proved: e.g., sg' is true whenever sg is true.

For the concision of proofs, we assume a good knowledge of the theory of logics and logic functors in the reading of proofs. What is emphasized in proofs is the invocation of properties over sub-logics as these invocations determine the theorems.


Previous Up Next