back next next
Table of Contents
Index
Glossary










































Table of Contents
Index
Glossary
back next next

Next: Glossary Up: Appendix: modularisation in other Previous: Empirical research in the

  
Abstract research: logic for artificial intelligence

As an example of a publication in an abstract domain, we consider a contribution to a book published in consequence of a conference about game theory and epistemic logic, in the domain of logic for artificial intelligence [Van der Hoek and Meyer, 1997].

The objects of study in this domain are `logics'. In the broad definition of the word, a logic consists of: 1) a language (determining what are well-formed formulas), 2) a model (a slice of a `universe' in which formulas are interpreted (as true or false), and 3) a deductive or axiomatic system (for proving formulas). The main goal of the research in this area is to find a combination of a deductive system and a class of models for which all formulas that can be proven in the deductive system are true in the models (this is called `soundness') and for which all formulas true in the models can be proven by the deductive system (`completeness'). The soundness and completeness of a deductive system with respect to a class of models must be proven. Consequently, [Van der Hoek and Meyer, 1997] might be modularised as follows.

Positioning
  In [Van der Hoek and Meyer, 1997], the main goal was to prove the soundness and completeness of an epistemic logic called S5m(CDE) , with respect to a particular class of models. This logic forms (according to the abstract) ``one overall system for describing the knowledge in a group of m agents, in which distributed knowledge, everybody's knowledge and common knowledge can be dealt with at the same time.''

The situation was as follows: separate logics already existed for individual distributed knowledge, and for common knowledge and everybody's knowledge. For the combination of these types of knowledge, however, only conjectures about completeness of this logic with respect to some intended class of models had been found. Applying standard techniques to obtain completeness, the obtained class of models was too general, and a justification was needed to specialise this class to the desired class. This information, that was presented in the 1.Introduction, can be recast in a module Positioning, consisting of the constituent modules Situation and Central problem, in a straightforward way.

Description of the logic
In section 2.A system for knowledge of M agents, the deductive system and the language are defined. The class of models is described in section 3.Semantics. The desired class of models for this deductive system and language could be formulated intuitively and was already conjectured to be the `proper' class in the literature. The problem was to prove that the deductive system was sound and complete with respect to that class of models.

The logic under consideration, i.e. the deductive system, the language and the model, is a key element in the publications. In a modular environment, the logic could therefore be given in a module Description of the logic, with constituent modules Description of the deductive system and Description of the model. The definition of the language is very brief here, but it could be presented in a third constituent module.

In the original publication, it is explicitly stated that the definition of the general logic for knowledge of a group of m agents is part of the background. In a modular environment, the information could be presented in a separate module for multiple use, and then it could be linked to this publication.

Proving
In section 4.Transferring truth, the soundness and completeness of the deductive system with respect to the desired class of models are proven. The method consists, in essence, of the application of two standard techniques and a more novel one, which has been developed by the authors in a previous publication. In experimental science, the main activities are measuring, using experimental methods, and calculating, using numerical and theoretical methods. In the domain of logic, the main activity is proving, and the techniques that are used are proof techniques.

A modular version of this article might, therefore, contain a module Proving, consisting of two constituent modules. In the constituent module, Proof techniques, a brief summary might be give of the techniques, in addition to a link to three separate, wide-range Proof techniques modules that are designed for multiple use. In the second constituent module, Proofs, the actual proofs are given. The fact that the proofs can be isolated from the rest of the discourse is indicated by the fact that, in linear articles, the proofs are often presented in an appendix. This constituent module could be a compound module, with the proofs of key theorems, which form the main steps in the procedure. The summary of the subsequent steps of the proof given in section 3, could serve as the module summary of the module Proof.

Theorems
The `results' are several proven theorems. The difference between a lemma and a theorem is that a theorem is an important result that is likely to be used by others, whereas a lemma is only used within the context of the proof of a theorem (as an intermediary result). In order to allow receivers to locate and consult a theorem separately, the theorems could be presented in a separate module.

Outcome
  The following findings are summarised in the section 5.Conclusions. It is proven that the overall logic is sound and complete with respect to the desired class of models, the standard techniques can indeed be applied to this proof, and, in passing, another relevant property of the epistemic system has been proven. At the end of section 4, some open problems are stated. It is would be easy to create a module Outcome for this publication, consisting of Findings and Leads for further research.

Thus, the following modules might be distinguished by the conceptual function in the domain of logic for artificial intelligence:

1.
Meta-information, as in our modular model, including the standard constituent modules;
2.
Positioning, as in our modular model:
(a)
Situation;
(b)
Central problem;
3.
Description of the logic, a domain-specific module in which the main objects of the research can be grouped:
(a)
Description of the deductive system;
(b)
Description of the model;
(c)
Description of the language.
Because the same deductive system, model or language can be examined in more than one publication, these modules are suitable for multiple use;
4.
Proving, a domain-specific module in which the `action' takes place:
(a)
Proof techniques, with a description of the techniques. These techniques can be standard, so that this module is suitable for multiple use.
(b)
Proofs in these techniques are used to give the actual proofs.
5.
Theorems, a domain-specific module providing the result of the research in terms of proven theorems in the module.
6.
Outcome, as in our model
(a)
Findings
(b)
Leads for further research. In this domain, this module is optional, as the research can be considered to be complete if the theorems are proven.

back next next
Table of Contents
Index
Glossary










































Table of Contents
Index
Glossary
back next next

Next: Glossary Up: Appendix: modularisation in other Previous: Empirical research in the