2003 Kluwer Academic Publishers. Printed in the Netherlands. Some Fragments of FTL of knowledge with interaction

Deduction based semi-decision procedure KISat, and decision procedures K∗ISat and K+ISat for new fragments of a first-order linear temporal logic with knowledge and inter-action (FTLKI) are presented. As temporal operators we consider Next and Always. For knowledge we assume a set of agents Ag = {1,..., n} and introduce a set of unary modal connectives Ki for i ∈ Ag, where a formula of the shape KiA is read as "agent i knows A". The modal connectives Ki satisfy analogues of the axioms of the modal logic S5 which is widely recognized as a logic of idealized knowledge. An interaction considered captures syn-chronous systems with perfect recall. The perfect recall (or no forgetting) means that knowl-edge of agents grows over time. The object of consideration in this paper is positive sequents, i.e. sequents not containing negation symbol. The considered fragments of FTLKI allow epistemic part (i.e. logic which contains logical and knowledge operators but does not contain temporal ones) to separate from temporal part effectively. In turn in temporal part the proposed procedures separate sequents not containing positive occurrences of temporal operator Always from sequents containing such occurrences. The latter are related with an inductive reason-ing in FTLKI. The complexity of presented procedures mainly depends on a complexity of epistemic part of fragments under consideration. The language of KISat and K∗ISat satis-fies some epistemic succedent restriction. The decision procedure K∗ISat is obtained from KISat by adding some epistemic decision condition. The decision procedure K+ISat is obtained from K∗ISat by dropping the epistemic succedent restriction. The presented proce-dures are sound and complete. The presented procedures can be used for verification of agent declarative programming language based on the considered fragments of FTLKI