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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Birkhoff, G., and J. V. Neumann, ‘The Logic of Quantum Mechanics’, Ann. Math., 37:823–843, 1936.
Egly, U., and S. Schmitt, ‘On Intuitionistic Proof Transformations, Their Complexity and Application to Constructive Program Synthesis’, Fundamenta Informaticae, 39:59–83, 1999.
Faggian, C., and G. Sambin, ‘From Basic Logic to Quantum Logics with Cut-Elimination’, International Journal of Theoretical Physics, 12, 1997.
Freese, R., J. JeŽek, and J. B. Nation, Free Lattices, vol. 42 of Mathematical Surveys and Monographs. Amer. Math. Soc., 1995.
Kalmbach, G., Orthomodular Lattices, Academic Press, 1983.
Kleene, S. C., ‘Permutability of Inferences in Gentzen's Calculi LK and LJ’, Memoirs of the AMS, 10:1–26, 1952.
Maslov, S. Yu., ‘An Inverse Method for Establishing Deducibility in the Classical Predicate Calculus’, Doklady Akademii Nauk SSSR, 159:17–20, 1964.
McCune, W., ‘Automatic Proofs and Counterexamples for some Ortholattice Examples’, Information Processing Letters, 65:285–291, 1998.
PaviČiĆ, M., and N. Megill, ‘Binary Orthologic with Modus Ponens is Either Orthomodular or Distributive’, Helv. Phys. Acta, 71, 1998.
Plaisted, D. A., and Y. Zhu, The Efficiency of Theorem Proving Strategies. Computational Intelligence, Vieweg, Braunschweig, 1997.
Sambin, G., G. Battilotti, and C. Faggian, ‘Basic Logic: Reflection, Symmetry, Visibility’, Journal of Symbolic Logic, 65(3):979–1013, 2000.
Schulte MÖnting, J., ‘Cut Elimination and Word Problems for Varieties of Lattices’, Algebra Universalis, 12:290–321, 1981.
Skolem, T., ‘Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem Theoreme über dichte Mengen’, Skrifter utgit av Videnskapsselskapet i Kristiania I, Matematisk-naturvidenskabelig klasse, 4:1–36, 1920.
Smullyan, R., First-Order Logic. Springer Verlag, 1968. Second Printing 1971.
Troelstra, A. S., and H. Schwichtenberg, Basic Proof Theory, vol. 43 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1996.
Voronkov, A., ‘Theorem Proving in Non-Standard Logics Based on the Inverse Method’, in D. Kapur, editor, Proc. of the 11th International Conference on Automated Deduction (CADE-11), pp. 648–662, Springer Verlag, 1992.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Egly, U., Tompits, H. On Different Proof-Search Strategies for Orthologic. Studia Logica 73, 131–152 (2003). https://doi.org/10.1023/A:1022993408070
Issue Date:
DOI: https://doi.org/10.1023/A:1022993408070