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

논문 상세정보

Journal of logic and computation v.27 no.1, 2017년, pp.81 - 107  

Completeness and termination for a Seligman-style tableau system

Blackburn, Patrick ; Bolander, Thomas ; Brauner, Torben ; Jørgensen, Klaus Frovin ;
  • 초록  

    Proof systems for hybrid logic typically use [Formula]-operators to access information hidden behind modalities; this labelling approach lies at the heart of the best known hybrid resolution, natural deduction and tableau systems. But there is another approach, which we have come to believe is conceptually clearer. We call this Seligman-style inference, as it was first introduced and explored by Jerry Seligman in natural deduction and sequent calculus in the 1990s. The purpose of this article is to introduce a Seligman-style tableau system, to prove its completeness, and to show how it can be made to terminate. The most obvious feature of Seligman-style systems is that they work with arbitrary formulas, not just statements prefixed by [Formula]-operators. They do so by introducing machinery for switching to other proof contexts. We capture this idea in the setting of tableaus by introducing a rule called GoTo, which allows us to ‘jump to a named world’ on a tableau branch. We first develop a Seligman-style tableau system for basic hybrid logic and prove its completeness. We then prove termination of a restricted version of the system without resorting to loop checking, and show that the restrictions do not effect completeness. Both completeness and termination results are proved by explicit translations that transform tableaus in a standard labelled system into Seligman-style tableaus and vice-versa.


  • 주제어

    Tableau systems .   hybrid logic .   Seligman-style systems .   labelled deduction .   completeness .   termination.  

 활용도 분석

  • 상세보기

    amChart 영역
  • 원문보기

    amChart 영역

원문보기

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

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

원문복사신청을 하시면, 일부 해외 인쇄학술지의 경우 외국학술지지원센터(FRIC)에서
무료 원문복사 서비스를 제공합니다.

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

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