{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:27:01Z","timestamp":1725470821740},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540356332"},{"type":"electronic","value":"9783540356363"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11784180_25","type":"book-chapter","created":{"date-parts":[[2006,9,26]],"date-time":"2006-09-26T14:12:21Z","timestamp":1159279941000},"page":"323-337","source":"Crossref","is-referenced-by-count":0,"title":["Tableaux for Lattices"],"prefix":"10.1007","author":[{"given":"Georg","family":"Struth","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","unstructured":"Birkhoff, G.: Lattice Theory. Colloquium Publications, vol.\u00a025. American Mathematical Society (reprint, 1984)"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/3-540-56868-9_29","volume-title":"Rewriting Techniques and Applications","author":"C. Delor","year":"1993","unstructured":"Delor, C., Puel, L.: Extension of the associative path ordering to a chain of associative-commutative symbols. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol.\u00a0690, pp. 389\u2013404. Springer, Heidelberg (1993)"},{"key":"25_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M. Fitting","year":"1996","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, Heidelberg (1996)","edition":"2"},{"key":"25_CR4","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/BF00370680","volume":"50","author":"J.M. Font","year":"1991","unstructured":"Font, J.M., Verd\u00fa, V.: Algebraic logic for classical conjunction and disjunction. Studia Logica\u00a050, 391\u2013419 (1991)","journal-title":"Studia Logica"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Freese, R., Je\u017eek, J., Nation, J.B.: Free Lattices. Surveys and Monographs, vol.\u00a042. American Mathematical Society (1995)","DOI":"10.1090\/surv\/042"},{"key":"25_CR6","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift\u00a039, 176\u2013210, 405\u2013431 (1935)","journal-title":"Mathematische Zeitschrift"},{"issue":"2","key":"25_CR7","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266681","volume":"16","author":"P. Lorenzen","year":"1951","unstructured":"Lorenzen, P.: Algebraische und logistische Untersuchungen \u00fcber freie Verb\u00e4nde. The Journal of Symbolic Logic\u00a016(2), 81\u2013106 (1951)","journal-title":"The Journal of Symbolic Logic"},{"issue":"4","key":"25_CR8","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1017\/S0960129504004244","volume":"14","author":"S. Negri","year":"2004","unstructured":"Negri, S., von Plato, J.: Proof systems for lattice theory. Mathematical Structures in Computer Science\u00a014(4), 507\u2013526 (2004)","journal-title":"Mathematical Structures in Computer Science"},{"key":"25_CR9","unstructured":"Rusinowitch, M.: D\u00e9monstration Automatique: Techniques de R\u00e9ecriture. Science Informatique. InterEditions, Paris (1989)"},{"key":"25_CR10","doi-asserted-by":"publisher","first-page":"867","DOI":"10.1016\/S0049-237X(08)71124-8","volume-title":"Handbook of Mathematical Logic","author":"H. Schwichtenberg","year":"1977","unstructured":"Schwichtenberg, H.: Proof theory: Some applications of cut-elimination. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 867\u2013895. North-Holland, Amsterdam (1977)"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/10721975_15","volume-title":"Rewriting Techniques and Applications","author":"G. Struth","year":"2000","unstructured":"Struth, G.: An algebra of resolution. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 214\u2013228. Springer, Heidelberg (2000)"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/3-540-45127-7_22","volume-title":"Rewriting Techniques and Applications","author":"G. Struth","year":"2001","unstructured":"Struth, G.: Deriving focused calculi for transitive relations. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, pp. 291\u2013305. Springer, Heidelberg (2001)"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/3-540-45610-4_7","volume-title":"Rewriting Techniques and Applications","author":"G. Struth","year":"2002","unstructured":"Struth, G.: Deriving focused lattice calculi. In: Tison, S. (ed.) RTA 2002. LNCS, vol.\u00a02378, pp. 83\u201397. Springer, Heidelberg (2002)"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/978-3-540-39893-6_31","volume-title":"Formal Methods and Software Engineering","author":"G. Struth","year":"2003","unstructured":"Struth, G.: A calculus for set-based program development. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol.\u00a02885, pp. 541\u2013559. Springer, Heidelberg (2003)"},{"key":"25_CR15","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1109\/SEFM.2004.1347536","volume-title":"2nd International Conference on Software Engineering and Formal Methods","author":"G. Struth","year":"2004","unstructured":"Struth, G.: Automated element-wise reasoning with sets. In: Cuellar, J.R., Liu, Z. (eds.) 2nd International Conference on Software Engineering and Formal Methods, pp. 320\u2013329. IEEE Computer Society Press, Los Alamitos (2004)"},{"issue":"2","key":"25_CR16","doi-asserted-by":"publisher","first-page":"325","DOI":"10.2307\/1969001","volume":"42","author":"P..M. Whitman","year":"1941","unstructured":"Whitman, Ph.M.: Free lattices. Ann. of Math.\u00a042(2), 325\u2013330 (1941)","journal-title":"Ann. of Math."}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11784180_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:18:48Z","timestamp":1619507928000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11784180_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540356332","9783540356363"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/11784180_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}