{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T01:21:56Z","timestamp":1755220916192,"version":"3.43.0"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2003,2,1]],"date-time":"2003-02-01T00:00:00Z","timestamp":1044057600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,2,1]],"date-time":"2003-02-01T00:00:00Z","timestamp":1044057600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Studia Logica"],"published-print":{"date-parts":[[2003,2]]},"DOI":"10.1023\/a:1022993408070","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T18:16:51Z","timestamp":1049739411000},"page":"131-152","source":"Crossref","is-referenced-by-count":4,"title":["On Different Proof-Search Strategies for Orthologic"],"prefix":"10.1007","volume":"73","author":[{"given":"Uwe","family":"Egly","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans","family":"Tompits","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5117575_CR1","doi-asserted-by":"crossref","first-page":"823","DOI":"10.2307\/1968621","volume":"37","author":"G. Birkhoff","year":"1936","unstructured":"Birkhoff, G., and J. V. Neumann, \u2018The Logic of Quantum Mechanics\u2019, Ann. Math., 37:823\u2013843, 1936.","journal-title":"Ann. Math."},{"key":"5117575_CR2","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/FI-1999-391204","volume":"39","author":"U. Egly","year":"1999","unstructured":"Egly, U., and S. Schmitt, \u2018On Intuitionistic Proof Transformations, Their Complexity and Application to Constructive Program Synthesis\u2019, Fundamenta Informaticae, 39:59\u201383, 1999.","journal-title":"Fundamenta Informaticae"},{"key":"5117575_CR3","unstructured":"Faggian, C., and G. Sambin, \u2018From Basic Logic to Quantum Logics with Cut-Elimination\u2019, International Journal of Theoretical Physics, 12, 1997."},{"key":"5117575_CR4","doi-asserted-by":"crossref","unstructured":"Freese, R., J. Je\u017dek, and J. B. Nation, Free Lattices, vol. 42 of Mathematical Surveys and Monographs. Amer. Math. Soc., 1995.","DOI":"10.1090\/surv\/042"},{"key":"5117575_CR5","unstructured":"Kalmbach, G., Orthomodular Lattices, Academic Press, 1983."},{"key":"5117575_CR6","first-page":"1","volume":"10","author":"S. C. Kleene","year":"1952","unstructured":"Kleene, S. C., \u2018Permutability of Inferences in Gentzen's Calculi LK and LJ\u2019, Memoirs of the AMS, 10:1\u201326, 1952.","journal-title":"Memoirs of the AMS"},{"key":"5117575_CR7","first-page":"17","volume":"159","author":"S. Y. Maslov","year":"1964","unstructured":"Maslov, S. Yu., \u2018An Inverse Method for Establishing Deducibility in the Classical Predicate Calculus\u2019, Doklady Akademii Nauk SSSR, 159:17\u201320, 1964.","journal-title":"Doklady Akademii Nauk SSSR"},{"key":"5117575_CR8","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1016\/S0020-0190(98)00015-5","volume":"65","author":"W. McCune","year":"1998","unstructured":"McCune, W., \u2018Automatic Proofs and Counterexamples for some Ortholattice Examples\u2019, Information Processing Letters, 65:285\u2013291, 1998.","journal-title":"Information Processing Letters"},{"key":"5117575_CR9","unstructured":"Pavi\u010ci\u0106, M., and N. Megill, \u2018Binary Orthologic with Modus Ponens is Either Orthomodular or Distributive\u2019, Helv. Phys. Acta, 71, 1998."},{"key":"5117575_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-93862-6","volume-title":"The Efficiency of Theorem Proving Strategies","author":"D. A. Plaisted","year":"1997","unstructured":"Plaisted, D. A., and Y. Zhu, The Efficiency of Theorem Proving Strategies. Computational Intelligence, Vieweg, Braunschweig, 1997."},{"issue":"3","key":"5117575_CR11","doi-asserted-by":"crossref","first-page":"979","DOI":"10.2307\/2586685","volume":"65","author":"G. Sambin","year":"2000","unstructured":"Sambin, G., G. Battilotti, and C. Faggian, \u2018Basic Logic: Reflection, Symmetry, Visibility\u2019, Journal of Symbolic Logic, 65(3):979\u20131013, 2000.","journal-title":"Journal of Symbolic Logic"},{"key":"5117575_CR12","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1007\/BF02483891","volume":"12","author":"J. Schulte M\u00d6nting","year":"1981","unstructured":"Schulte M\u00d6nting, J., \u2018Cut Elimination and Word Problems for Varieties of Lattices\u2019, Algebra Universalis, 12:290\u2013321, 1981.","journal-title":"Algebra Universalis"},{"key":"5117575_CR13","first-page":"1","volume":"4","author":"T. Skolem","year":"1920","unstructured":"Skolem, T., \u2018Logisch-kombinatorische Untersuchungen \u00fcber die Erf\u00fcllbarkeit oder Beweisbarkeit mathematischer S\u00e4tze nebst einem Theoreme \u00fcber dichte Mengen\u2019, Skrifter utgit av Videnskapsselskapet i Kristiania I, Matematisk-naturvidenskabelig klasse, 4:1\u201336, 1920.","journal-title":"Skrifter utgit av Videnskapsselskapet i Kristiania I, Matematisk-naturvidenskabelig klasse"},{"key":"5117575_CR14","doi-asserted-by":"crossref","unstructured":"Smullyan, R., First-Order Logic. Springer Verlag, 1968. Second Printing 1971.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"5117575_CR15","unstructured":"Troelstra, A. S., and H. Schwichtenberg, Basic Proof Theory, vol. 43 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1996."},{"key":"5117575_CR16","doi-asserted-by":"crossref","unstructured":"Voronkov, A., \u2018Theorem Proving in Non-Standard Logics Based on the Inverse Method\u2019, in D. Kapur, editor, Proc. of the 11th International Conference on Automated Deduction (CADE-11), pp. 648\u2013662, Springer Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_198"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022993408070.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1022993408070\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022993408070.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:14:00Z","timestamp":1754630040000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1022993408070"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,2]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,2]]}},"alternative-id":["5117575"],"URL":"https:\/\/doi.org\/10.1023\/a:1022993408070","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2003,2]]}}}