On different proof-search strategies for orthologic

Studia Logica 73 (1):131 - 152 (2003)
  Copy   BIBTEX


In this paper, we consider three different search strategies for a cut-free sequent system formalizing orthologic, and estimate the respective search spaces. Applying backward search, there are classes of formulae for which both the minimal proof length and the search space are exponential. In a combined forward and backward approach, all proofs are polynomial, but the potential search space remains exponential. Using a forward strategy, the potential search space becomes polynomial yielding a polynomial decision procedure for orthologic and the word problem for free ortholattices.



    Upload a copy of this work     Papers currently archived: 93,127

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles


Added to PP

6 (#1,485,580)

6 months
53 (#90,063)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references