Boolean unification with predicates
In this article, we deal with the following problem which we call Boolean unification with predicates: For a given formula [Formula] in first-order logic with equality containing an [Formula]-ary predicate variable [Formula], is there a quantifier-free formula [Formula] such that the formula [Formula] is valid in first-order logic with equality? We obtain the following results. Boolean unification with predicates for quantifier-free [Formula] is [Formula]-complete. In addition, there exists an EXPTIME algorithm which for an input formula [Formula], given as above, constructs a formula [Formula] such that [Formula] being valid in first-order logic with equality, if such a formula exists. For [Formula] of the form [Formula] with [Formula] quantifier-free, we prove that Boolean unification with predicates is already undecidable. The same holds for [Formula] of the form [Formula] for [Formula] quantifier-free. Instances of Boolean unification with predicates naturally occur in the context of automated theorem proving. Our results are relevant for cut-introduction and the automated search for induction invariants.
- 원문이 없습니다.
NDSL에서는 해당 원문을 복사서비스하고 있습니다. 위의 원문복사신청 또는 장바구니 담기를 통하여 원문복사서비스 이용이 가능합니다.
- 이 논문과 함께 출판된 논문 + 더보기