A Logical Study of Interactive Computational Problems Understood as Games

点击翻译按钮获取中文摘要

The goal of this research is to elaborate an elegant and comprehensive specification language and semantics for interactive computational problems and explore the corresponding logic, --- the set of valid principles of interactive computability expressible in that language. Such a logic provides us with a powerful tool for systematically studying computational tasks and automatically generating solutions to new problems from known solutions to old problems. Other applications include the possibility to base on this logic knowledge- and resource-oriented automatic reasoning systems. The intuitive notion of interactive computational problem is formalized as a game between two players: the machine and the environment (user). Moves of the game represent actions/choices by these agents, and positions represent states/situations that emerge in the course of interaction. A game is considered winnable (and hence the corresponding problem solvable), if there is a computer program that wins it against any possible environment. The language of the logic of interactive computational problems suggested by the investigator is a non-disjoint union of the languages of classical, intuitionistic and linear logics, with logical operators interpreted as certain, --- most basic and natural, --- operations on games. Validity of a formula is understood as winnability for every game/problem interpretation of its atoms. The restriction of winnability to the classical fragment of the language turns out to be equivalent to the classical concept of truth, which makes classical logic a natural syntactic fragment of the logic of interactive computational problems. The same is conjectured to be the case for the intuitionistic logic and (a version of) linear logic. This way, the logic of interactive computational problems can unify, within the framework of one general semantics, the classical, intuitionistic and linear logics, with their seemingly unrelated or even antagonistic philosophies. Verifying this conjecture, along with finding an axiomatization for the logic of interactive computational problems, is among the main technical objectives of this research.