Classical logics for strategic reasoning, such as Coalition Logic and Alternating-time Temporal Logic, formalize absolute strategic reasoning about the unconditional strategic abilities of agents to achieve their goals. Goranko and Ju introduced a logic ConStR for strategic reasoning about conditional strategic abilities. However, its completeness is still an open problem. ConStR has three featured operators, and one of them has the following reading: For some action of A that guarantees the achievement of her goal, B has an action to guarantee the achievement of his goal. The logic about this operator is called CConStR. In this paper, we prove completeness for two fragments of CConStR. The key notions of our proof approach include downward validity lemma, grafted models, and upward derivability lemma. The proof approach has good potential to be applied to the completeness of ConStR and other logics.

翻译：经典策略推理逻辑（如联盟逻辑和交替时态逻辑）形式化了关于主体无条件策略能力以实现其目标的绝对策略推理。Goranko和Ju引入了一种用于条件策略能力推理的逻辑ConStR，但其完备性仍是一个未决问题。ConStR包含三个特色算子，其中之一具有如下含义：存在A的某个行动保证实现其目标，使得B存在一个行动保证实现其目标。关于该算子的逻辑称为CConStR。本文证明了CConStR的两个片段的完备性。我们证明方法的关键概念包括向下有效性引理、嫁接模型和向上可推导性引理。该方法具有良好的潜力，可应用于ConStR及其他逻辑的完备性证明。