[logic-ml] Prof. Dieter Spreen at NII Logic Seminar

[Makoto Tatsuta]

	      Prof. Dieter Spreen at NII Logic Seminar


Date: March 22, 2016, 14:00--16:00

Place: National Institute of Informatics, Room 1901 (19th floor)
場所: 国立情報学研究所 19階 1901室
    (半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分)
    (地図 http://www.nii.ac.jp/about/access/)

Speaker: Prof. Dieter Spreen (Siegen University)

Ttile: Information Frames

Abstract: 
In 1982, Dana Scott introduced information systems as a logic-based
approach to domain theory. Here, a domain is a bound-complete
algebraic complete partial order with least element. An information
system consists of a set of tokens to be thought of as atomic
statements about a computational process, a consistency predicate
telling us which finite sets of such statements contain consistent
information, and an entailment relation saying what atomic statements
are entailed by which consistent sets of these. Theories of such a
logic, also called states, i.e. finitely consistent and
entailment-closed sets of atomic statements, form a bounded-complete
algebraic complete partial order with respect to set inclusion, and,
conversely, every such domain can be obtained in this way, up to
isomorphism. This gives Scott's idea that domain elements represent
information about stages of a computation a precise mathematical
meaning.
  The role of bounded completeness becomes also clear in this context:
States represent consistent information. So, any finite collection of
substates must contain consistent infor- mation as well, and this fact
is witnessed by any of its upper bounds.
  Whereas in Scott's approach the consistency witnesses are hidden, in
this paper we present an approach that makes them explicit. This
allows to consider the more general situation in which there is no
longer a uniform global consistency predicate. Instead there a is
consistency predicate for each atomic statement telling us which
finite sets of atomic statements express information that is
consistent with the given statement. As it turns out the theories, or
states, of such a more general information system form an L-domain,
and, up to isomorphism, each L-domain can be obtained in this way.
  Since every token in the just delineated kind of information system
has its own consistency predicate, we can also think of each such
system as a family of logics, or a Kripke frame.

問合せ先:
龍田 真 (国立情報学研究所)
e-mail: tatsuta at nii.ac.jp
http://research.nii.ac.jp/~tatsuta