본문 바로가기
HOME> 논문 > 논문 검색상세

논문 상세정보

Journal of logic and computation v.27 no.1, 2017년, pp.109 - 128  

Boolean unification with predicates

Eberhard, Sebastian ; Hetzl, Stefan ; Weller, Daniel ;
  • 초록  

    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.


  • 주제어

    Boolean unification .   second-order unification .   quantifier elimination .   decidability .   complexity.  

 활용도 분석

  • 상세보기

    amChart 영역
  • 원문보기

    amChart 영역

원문보기

무료다운로드
  • 원문이 없습니다.
유료다운로드

유료 다운로드의 경우 해당 사이트의 정책에 따라 신규 회원가입, 로그인, 유료 구매 등이 필요할 수 있습니다. 해당 사이트에서 발생하는 귀하의 모든 정보활동은 NDSL의 서비스 정책과 무관합니다.

NDSL에서는 해당 원문을 복사서비스하고 있습니다. 위의 원문복사신청 또는 장바구니 담기를 통하여 원문복사서비스 이용이 가능합니다.

이 논문과 함께 출판된 논문 + 더보기