论文部分内容阅读
本文针对一种典型的直觉主义模态逻辑系统IS4引进了一种基于标记迁移系统的操作语义，将模态逻辑系统IS4的推理规则与过程可视化。由模态逻辑系统IS4出发，详细地构造出一个标记迁移系统LTSIS，在该系统中，系统IS4中公式之间的形式可推演关系可以表示为系统LTSIS中的状态迁移图。对于任意一个系统IS4的公式A，可以把它看作一个状态E(A)。然后，本文由系统IS4中公式之间的形式推演规则出发，构造标记迁移系统LTSIS的动作集合、迁移集合和迁移模式。这样，可以应用系统LTSIS的迁移模式来描述系统IS4公式之间的形式可推演关系。对于任意系统IS4公式之间的形式可推演关系，可以构造系统LTSIS中的状态迁移图。