{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:34Z","timestamp":1725488614196},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540671909"},{"type":"electronic","value":"9783540465089"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46508-1_18","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:02:03Z","timestamp":1186171323000},"page":"267-281","source":"Crossref","is-referenced-by-count":0,"title":["Resolution-Based Theorem Proving for SH n-Logics"],"prefix":"10.1007","author":[{"given":"Viorica","family":"Sofronie-Stokkermans","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1145\/321592.321603","volume":"17","author":"R. Anderson","year":"1970","unstructured":"R. Anderson and W. Bledsoe. A linear format for resolution with merging and a new technique for establishing completeness. Journal of the ACM, 17:525\u2013534, 1970.","journal-title":"Journal of the ACM"},{"key":"18_CR2","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1006\/jsco.1995.1021","volume":"19","author":"M. Baaz","year":"1995","unstructured":"M. Baaz and C.G. Ferm\u00fcller. Resolution-based theorem proving for manyvalued logics. Journal of Symbolic Computation, 19:353\u2013391, 1995.","journal-title":"Journal of Symbolic Computation"},{"key":"18_CR3","unstructured":"B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990."},{"key":"18_CR4","unstructured":"H. Ganzinger and V. Sofronie-Stokkermans. Chaining calculi and resolutionbased theorem proving in many-valued logic. In preparation, 1999."},{"issue":"6","key":"18_CR5","doi-asserted-by":"publisher","first-page":"905","DOI":"10.1093\/logcom\/4.6.905","volume":"4","author":"R. H\u00e4hnle","year":"1994","unstructured":"R. H\u00e4hnle. Short conjunctive normal forms in finitely valued logics. Journal of Logic and Computation, 4(6):905\u2013927, 1994.","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"18_CR6","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1080\/11663081.1996.10510866","volume":"6","author":"R. H\u00e4hnle","year":"1996","unstructured":"R. H\u00e4hnle. Exploiting data dependencies in many-valued logics. Journal of Applied Non-Classical Logics, 6(1):49\u201369, 1996.","journal-title":"Journal of Applied Non-Classical Logics"},{"issue":"1","key":"18_CR7","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/A:1005086415447","volume":"61","author":"R. H\u00e4hnle","year":"1998","unstructured":"R. H\u00e4hnle. Commodious axiomatization of quantifiers in multiple-valued logic. Studia Logica, 61(1):101\u2013121, 1998.","journal-title":"Studia Logica"},{"key":"18_CR8","unstructured":"L. Iturrioz and E. Or\u0142owska. A Kripke-style and relational semantics for logics based on Lukasiewicz algebras. Conference in honour of J. Lukasiewicz, Dublin, 1996."},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"L. Iturrioz. Modal operators on symmetrical Heyting algebras. In T. Traczyk, editor, Universal Algebra and Applications, Banach Center Publications, Vol. 9, pages 289\u2013303. PWN-Polish Scientific Publishers, 1982.","DOI":"10.4064\/-9-1-289-303"},{"key":"18_CR10","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1002\/malq.19830290202","volume":"29","author":"L. Iturrioz","year":"1983","unstructured":"L. Iturrioz. Symmetrical Heyting algebras with operators. Zeitschrift f. math. Logik und Grundlagen d. Mathematik, 29:33\u201370, 1983.","journal-title":"Zeitschrift f. math. Logik und Grundlagen d. Mathematik"},{"key":"18_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"688","DOI":"10.1007\/3-540-61511-3_122","volume-title":"Proc. 13th Conference on Automated Deduction, New Brunswick\/NJ, USA","author":"G. Salzer","year":"1996","unstructured":"G. Salzer. Optimal axiomatizations for multiple-valued operators and quantifiers based on semilattices. In M. McRobbie and J. Slaney, editors, Proc. 13th Conference on Automated Deduction, New Brunswick\/NJ, USA, LNCS 1104, pages 688\u2013702. Springer Verlag, 1996."},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"D.S. Scott. Background to formalization. In H. Leblanc, editor, Truth, Syntax and Modality. Proceedings of the Temple University Conference on Alternative Semantics, Studies in Logic and the Foundations of Mathematics, Vol. 68, pages 244\u2013273, 1973.","DOI":"10.1016\/S0049-237X(08)71542-8"},{"key":"18_CR13","volume-title":"Fibered Structures and Applications to Automated Theorem Proving in Certain Classes of Finitely-Valued Logics and to Modeling Interacting Systems","author":"V. Sofronie-Stokkermans","year":"1997","unstructured":"V. Sofronie-Stokkermans. Fibered Structures and Applications to Automated Theorem Proving in Certain Classes of Finitely-Valued Logics and to Modeling Interacting Systems. PhD thesis, RISC-Linz, J.Kepler University Linz, Austria, 1997."},{"key":"18_CR14","unstructured":"V. Sofronie-Stokkermans. On translation of finitely-valued logics to classical first-order logic. In H. Prade, editor, Proceedings of ECAI 98, pages 410\u2013411. John Wiley & Sons, 1998."},{"key":"18_CR15","unstructured":"V. Sofronie-Stokkermans. Automated theorem proving by resolution for finitely-valued logics based on distributive lattices with operators. Submitted, 1999."},{"key":"18_CR16","unstructured":"V. Sofronie-Stokkermans. Priestley duality for SHn-algebras and applications to the study of Kripke-style models for SHn-logics. Multiple-Valued Logic \u2014 An International Journal, To appear, 1999."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Classical and Non-Classical Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46508-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T22:50:43Z","timestamp":1550443843000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46508-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540671909","9783540465089"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-46508-1_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}