6533b830fe1ef96bd12970fb

RESEARCH PRODUCT

Two-variable First-Order Logic with Counting in Forests

Witold CharatonikIan Pratt-hartmannPiotr WitkowskiYegor Guskov

subject

Variable (computer science)general satisfiabilityfinite satisfiabilitylogic and computational complexitydecision proceduresArithmetictwo-variable logic with counting quantifiersunranked trees/forestsMathematicsFirst-order logic

description

We consider an extension of two-variable, first-order logic with counting quantifiers and arbitrarily many unary and binary predicates, in which one distinguished predicate is interpreted as the mother-daughter relation in an unranked forest. We show that both the finite satisfiability and the general satisfiability problems for the extended logic are decidable in NExpTime. We also show that the decision procedure for finite satisfiability can be extended to the logic where two distinguished predicates are interpreted as the mother-daughter relations in two independent forests.

yearjournalcountryeditionlanguage
2018-10-23EPiC Series in Computing
10.29007/24fmhttps://doi.org/10.29007/24fm