A Logic for Incomplete Sequential Information

Describing incomplete sequential information is of growing importance in Knowledge Representation in Artificial Intelligence and Computer Science. To obtain logical foundations for representing incomplete sequential information, a new logic, called sequence-indexed constructive propositional logic (SLJ), is introduced as a Gentzen-type sequent calculus by extending Gentzen's LJ for intuitionistic logic. The system LJ is known as useful for representing incomplete information, and SLJ is obtained from LJ by adding a sequence modal operator which can represent sequential information. The cut-elimination and decidability theorems for SLJ are proved. A sequence-indexed Kripke semantics is introduced for SLJ, and the completeness theorem with respect to this semantics is proved. A logic programming framework can be developed based on SLJ.