2010 | OriginalPaper | Chapter
A Logic for Incomplete Sequential Information
Author : Norihiro Kamide
Published in: Knowledge-Based and Intelligent Information and Engineering Systems
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.