First-order logic is a widely used relational language of reasoning. Due to the fact that it is algorithmically impossible to determine whether a given sentence of first-order logic is valid or not, various restrictions of first-order logic have been devised to obtain languages that are less expressive but can be reasoned about by computers more easily. One of such prominent fragments of first-order logic is the two-variable frag- ment. Not only is it possible to check the validity of the sentences of this logic in a bounded amount of time, it is also the case that adding various useful reason- ing capabilities to two-variable first-order logic often preserves the time-bounded validity check. This thesis addresses the problem of the complexity of decidability of var- ious extensions of two-variable first-order logic on a broad scale by offering a systematic overview and comparison of the available results in the field. In addition to that the thesis gives the proof of decidability of the extension of two-variable first-order logic with counting quantifiers and the relation that models parent/child relations in a tree graph. The NEXPTIME upper complexity bound is established for the problem of finite satisfiability of this logic.
DECIDABILITY OF FINITE SATISFIABILITY OF TWO-VARIABLE FIRST-ORDER LOGIC WITH COUNTING AND LOCAL NAVIGATION IN UNORDERED UNRANKED TREES
Guskov, Y. (Author). 1 Aug 2018
Student thesis: Phd