{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T12:45:00Z","timestamp":1760013900873},"reference-count":16,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2010,5,27]],"date-time":"2010-05-27T00:00:00Z","timestamp":1274918400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2010,8]]},"abstract":"<jats:p>The uniform word problem for finitely presented ortholattices is shown to be solvable through a method of terminating proof search. The axioms of ortholattices are all Harrop formulas, and thus can be expressed in natural deduction style as single succedent rules. A system of natural deduction style rules for orthologic is given as an extension of the system for lattices presented by Negri and von Plato. By considering formal derivations of atomic formulas from a finite number of given atomic formulas, it is shown that proof search is bounded, and thus that the question of derivability of any atomic formula from any finite set of given atomic formulas is decidable.<\/jats:p>","DOI":"10.1017\/s0960129510000125","type":"journal-article","created":{"date-parts":[[2010,5,27]],"date-time":"2010-05-27T12:47:23Z","timestamp":1274964443000},"page":"625-638","source":"Crossref","is-referenced-by-count":6,"title":["A solution of the uniform word problem for ortholattices"],"prefix":"10.1017","volume":"20","author":[{"given":"ANDREA","family":"MEINANDER","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2010,5,27]]},"reference":[{"key":"S0960129510000125_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004244"},{"key":"S0960129510000125_ref14","first-page":"1","article-title":"Logisch-kombinatorische Untersuchungen \u00fcber die Erf\u00fcllbarkeit oder Beweisbarkeit mathematischer S\u00e4tze nebst einem Theoreme \u00fcber dichte Mengen","volume":"I","author":"Skolem","year":"1920","journal-title":"Skrifter utgitt av Videnskapsselskapet i Kristiania"},{"key":"S0960129510000125_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s000120200012"},{"key":"S0960129510000125_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/BF02483891"},{"key":"S0960129510000125_ref15","volume-title":"Selected works in logic","author":"Skolem","year":"1970"},{"key":"S0960129510000125_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/BF00671616"},{"key":"S0960129510000125_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/BF00652069"},{"key":"S0960129510000125_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-8130-3"},{"key":"S0960129510000125_ref16","first-page":"133","article-title":"A Gentzen formulation without the cut rule for ortholattices","volume":"5","author":"Tamura","year":"1988","journal-title":"Kobe J. Math."},{"key":"S0960129510000125_ref2","doi-asserted-by":"publisher","DOI":"10.2307\/1968621"},{"key":"S0960129510000125_ref1","volume-title":"The logic of quantum mechanics, Encyclopedia of Mathematics and its Applications","author":"Beltrametti","year":"1981"},{"key":"S0960129510000125_ref3","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19950410204"},{"key":"S0960129510000125_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90048-X"},{"key":"S0960129510000125_ref6","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026652903971"},{"key":"S0960129510000125_ref8","volume-title":"Orthomodular lattices","author":"Kalmbach","year":"1983"},{"key":"S0960129510000125_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/BF00670687"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129510000125","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T19:01:32Z","timestamp":1556478092000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129510000125\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,5,27]]},"references-count":16,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2010,8]]}},"alternative-id":["S0960129510000125"],"URL":"https:\/\/doi.org\/10.1017\/s0960129510000125","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,5,27]]}}}