Professor Satoshi Kobayashi

Area and Subject Taught Mathematical Logic
Research Theme(s) Non-Classical Logics and Their Application to Computer Science
Academic Degrees Doctor of Science, University of Tokyo
Keywords for Research Field Theoretical Computer Science, Foundations of Software, Non-Classical Logics, Constructive Logic
Office Phone Number Not Public

Research Overview

The logic ordinarily used in mathematics is called classical logic. This logic posits a world where the truth value (truth or falsity) of propositions is, in principle, completely determined. In computer science (CS), however, it is not enough for a truth value to be determined in principle; the problem is whether there is an algorithm to determine that truth value. Furthermore, "existence" in traditional logic simply means that "there is a solution," but in CS, the issue becomes algorithms for finding that solution. A logic called constructive logic, where the specific method for constructing a solution is always the issue, becomes useful here. In classical logic, a truth value never changes once it has been determined, but in the world of computers, we consider cases where truth values do change, due to the changing states of machines, and cases where unknown truth values become known due to the transmission of information. Such situations can be nicely expressed using a logic called modal logic. My research concerns these unusual logics (called non-classical logics), and their applications to CS. My specific interests include the logic of types in programs, theorem-proving using computers, program semantics, verification of program correctness, program derivation, and applications in intelligent information processing.

Notable Publications and Works in the Last Three Years

  1. Satoshi Kobayashi, "A New Translation for Semi-classical Theories | Backtracking without CPS", FLOPS 2008, 2008 年4 月
  2. "Iwanami Encyclopaedic Dictionary of Mathematics, 4th edition" (in Japanese), Japan Math. Soc. (ed), Iwanami Shoten (2007)