NO.042 Logical analysis of descriptions and their presentations – a computational logic approach

Shonan Village Center

January 26 - 29, 2015 (Check-in: January 25, 2015 )


  • Yoshiki Kinoshita
    • Kanagawa University, Japan
  • Bengt Nordström
    • Chalmers University of Technology, Sweden


Aim of the workshop

Our aim is to investigate whether logical methods are applicable to analysis of descriptions in, for instance,

● system specification,
● formal mathematics,
● system assurance,
● juris-informatics (law) and
● industrial standardisation.

In these areas, we have descriptions of some objects and relations between them. These descriptions are either formal or informal (in English or some graph language without precise semantics). We want to conduct logical, computational and mathematical studies that clarify the structure of such descriptions. Aspects of this has been studied in discourse representation theory, constructive type theory and informal logic. Results of earlier studies include object role modelling (ORM), state charts, Toulmin diagrams, goal structuring notation (GSN), grammatical frameworks (GF) and proof assistants. Some applications may be found in the above areas.

There has been an emphasis on reasoning aspects when applying mathematical logic in Computer Science and Informatics. In this workshop, we want to investigate the importance of ontological¹ aspects of mathematical logic. These are more important than deductive aspects in, for instance, validation of information systems. We are interested in description languages of varying level of formality, where the formal part makes some mechanical checking and manipulation possible.

The combination of deduction and ontology can also be found in mathematics where the concepts have matured during hundreds of years. Nowadays, a similar combination of ontological and deductive aspects can be found in descriptions of information systems, laws and rules, etc. We are convinced that studies of informal mathematics will be an important contribution to a deeper understanding of these issues.

This is an attempt to put together people from different fields to find a common analysis of Logical Description Languages. We need to agree about the major research issues. The time is not yet ripe to agree about techniques. The invited people are rather few, which is necessary to make progress towards a common understanding.

¹ Here we use the word ontology as a description of a domain with objects and relations and properties of these.

Study area

● Constructive Type Theory
● Informal logic
● Discourse Representation Theory
● Ontology in information science

Possible application area

● System specification
● Formal mathematics
● System assurance (verification and validation)
● Juris-informatics
● Industrial standardisation

Related Methods

● Proof assistants: editors for formal proofs like COQ, HOL, Agda.
● Toulmin model of argument
● Goal Structuring Notation
● Grammatical frameworks
● Object Role Modelling
● State charts

Research questions

● How to describe a modeling language (syntax, semantics, well formedness)
● How to use a modeling language
● Analysis of how models are evolved
● Examples of models
● General requirement of modeling languages
● Different persons want to have different knowledge/perspective of the same object
● One description can have many presentations (different natural languages, graphs, pictures)