Two-variable logic with counting is decidable

被引：74

作者：

Gradel, E

Otto, M

Rosen, E

机构：

来源：

12TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS | 1997年

关键词：

D O I：

10.1109/LICS.1997.614957

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We prove that the satisfiability and the finite satisfiability problems for C-2 are decidable. C-2 is first-order logic with only two variables in the presence of arbitrary counting quantifiers There Exists(greater than or equal to m), m greater than or equal to 1. It considerably extends L-2, plain first-order with only two variables, which is known to be decidable by a result of Mortimer's. Unlike L-2, C-2 does not have the finite model property.

引用

页码：306 / 317

页数：12