On Different Proof-Search Strategies for Orthologic |
| |
Authors: | Uwe Egly Hans Tompits |
| |
Affiliation: | (1) Institut für Informationssysteme 184/3, Technische Universität Wien, Favoritenstraße 9-11, A-1040 Vienna, Austria |
| |
Abstract: | 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. |
| |
Keywords: | orthologic minimal quantum logic proof theory Gentzen system proof complexity polynomial decision procedure |
本文献已被 SpringerLink 等数据库收录! |
|