{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:15:43Z","timestamp":1759032943566},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544876"},{"type":"electronic","value":"9783540384014"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54487-9_62","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T17:53:45Z","timestamp":1330192425000},"page":"248-260","source":"Crossref","is-referenced-by-count":25,"title":["Towards an efficient tableau proof procedure for multiple-valued logics"],"prefix":"10.1007","author":[{"given":"Reiner","family":"H\u00e4hnle","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"14_CR1","first-page":"262","volume-title":"Logik-Texte. Kommentierte Auswahl zur Geschichte der modernen Logik","author":"E. W. Beth","year":"1986","unstructured":"E. W. Beth. Semantic entailment and formal derivability. In Karel Berka and Lothar Kreiser, editors, Logik-Texte. Kommentierte Auswahl zur Geschichte der modernen Logik, pages 262\u2013266. Akademie-Verlag, Berlin, 1986."},{"key":"14_CR2","volume-title":"A Course in Universal Algebra, volume 78 of Graduate Texts in Mathematics","author":"S. Burris","year":"1981","unstructured":"Stanley Burris and H.P. Sankappanavar. A Course in Universal Algebra, volume 78 of Graduate Texts in Mathematics. Springer, New York, 1981."},{"issue":"2","key":"14_CR3","doi-asserted-by":"crossref","first-page":"473","DOI":"10.2307\/2274395","volume":"52","author":"W. A. Carnielli","year":"1987","unstructured":"Walter A. Carnielli. Systematization of finite many-valued logics through the method of tableaux. Journal of Symbolic Logic, 52(2):473\u2013493, June 1987.","journal-title":"Journal of Symbolic Logic"},{"key":"14_CR4","volume-title":"Algorithms for the Minimization of Binary and Multiple-Valued Logic Functions","author":"G. W. Dueck","year":"1988","unstructured":"Gerhard W. Dueck. Algorithms for the Minimization of Binary and Multiple-Valued Logic Functions. PhD thesis, University of Manitoba, Winnipeg, 1988."},{"key":"14_CR5","unstructured":"Jens Erik Fenstad, Per-Kristian Halvorsen, Tore Langholm, and Johan von Benthem. Equations, schemata and situations: A framework for linguistic semantics. Technical Report CSLI-85-29, Center for the Studies of Language and Information Stanford, 1985."},{"key":"14_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intutionistic Logics","author":"M. C. Fitting","year":"1983","unstructured":"Melvin C. Fitting. Proof Methods for Modal and Intutionistic Logics. Reidel, Dordrecht, 1983."},{"key":"14_CR7","unstructured":"Melvin C. Fitting. Negation as refutation. In LICS 1989 Proceedings, 1989."},{"key":"14_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-0357-2","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M. C. Fitting","year":"1990","unstructured":"Melvin C. Fitting. First-Order Logic and Automated Theorem Proving. Springer, New York, 1990."},{"key":"14_CR9","unstructured":"Reiner H\u00e4hnle. Spezifikation eines Theorembeweisers f\u00fcr dreiwertige First-Order Logik. IWBS Report 136, Wissenschaftliches Zentrum, IWBS, IBM Deutschland, September 1990."},{"key":"14_CR10","unstructured":"Reiner H\u00e4hnle. Uniform notation of tableaux rules for multiple-valued logics. In To appear in Proceedings International Symposium on Multiple-Valued Logic, Victoria, 1991."},{"key":"14_CR11","unstructured":"T. Kropf and H.-J. Wunderlich. Hierarchische Testmustergenerierung f\u00fcr sequentielle Schaltungen mit Hilfe von Temporaler Logik. II. ITG\/GI Workshop Testmethoden und Zuverl\u00e4ssigkeit von Schaltungen und Systemen, 1990."},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"F. Oppacher and E. Suen. Controlling deduction with proof condensation and heuristics. In J\u00f6rg H. Siekmann, editor, Proc. 8th International Conference on Automated Deduction, pages 384\u2013393, 1986.","DOI":"10.1007\/3-540-16780-3_105"},{"key":"14_CR13","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/BF00244513","volume":"4","author":"F. Oppacher","year":"1988","unstructured":"F. Oppacher and E. Suen. HARP: A tableau-based theorem prover. Journal of Automated Reasoning, 4:69\u2013100, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Peter H. Schmitt. Perspectives in multi-valued logic. Proceedings International Scientific Symposium on Natural Language and Logic, Hamburg, 1989.","DOI":"10.1007\/3-540-53082-7_24"},{"key":"14_CR15","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/0304-3975(89)90106-0","volume":"65","author":"J. C. Sheperdson","year":"1989","unstructured":"John C. Sheperdson. A sound and complete semantics for a version of negation as failure. Theoretical Computer Science, 65:343\u2013371, 1989.","journal-title":"Theoretical Computer Science"},{"key":"14_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"R. Smullyan","year":"1968","unstructured":"Raymond Smullyan. First-Order Logic. Springer, New York, second edition, 1968.","edition":"second edition"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Z. Stachniak. Note on resolution approximation of many-valued logics. In 20th International Symposium on Multiple-Valued Logic, Charlotte, pages 204\u2013209, May 1990.","DOI":"10.1109\/ISMVL.1990.122622"},{"key":"14_CR18","first-page":"143","volume-title":"Computer Science and Multiple-Valued Logics","author":"S. J. Surma","year":"1984","unstructured":"Stanis\u0142aw J. Surma. An algorithm for axiomatizing every finite logic. In David C. Rine, editor, Computer Science and Multiple-Valued Logics, pages 143\u2013149. North-Holland, Amsterdam, 1984."},{"key":"14_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-6942-2","volume-title":"Theory of Logical Calculi","author":"R. W\u00f3jcicki","year":"1988","unstructured":"Ryszard W\u00f3jcicki. Theory of Logical Calculi. Reidel, Dordrecht, 1988."},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Pierre Wolper. Temporal logic can be more expressive. In Proceedings 22nd Annual Symposium on Foundations of Computer Science, pages 340\u2013348, 1981.","DOI":"10.1109\/SFCS.1981.44"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54487-9_62.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:55:06Z","timestamp":1605628506000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54487-9_62"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544876","9783540384014"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-54487-9_62","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}