{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T16:01:11Z","timestamp":1765123271268},"reference-count":95,"publisher":"Elsevier","isbn-type":[{"type":"print","value":"9780444508133"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1016\/b978-044450813-3\/50022-9","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"1355-1402","source":"Crossref","is-referenced-by-count":30,"title":["Automated Deduction for Many-Valued Logics"],"prefix":"10.1016","author":[{"given":"Matthias","family":"Baaz","sequence":"first","affiliation":[]},{"given":"Christian G.","family":"Ferm\u00fcller","sequence":"additional","affiliation":[]},{"given":"Gernot","family":"Salzer","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/B978-044450813-3\/50022-9_bb0010","series-title":"Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems (CTRS 90)","first-page":"156","article-title":"An application of the theorem prover SBR3 to many-valued logic","author":"Anantharaman","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0015","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/S0004-3702(98)00032-0","article-title":"The value of four values","volume":"102","author":"Arieli","year":"1998","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0020","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/BF01531058","article-title":"Hypersequents, logical consequence and intermediate logics for concurrency","volume":"4","author":"Avron","year":"1991","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50022-9_bb0025","doi-asserted-by":"crossref","first-page":"276","DOI":"10.2307\/2274919","article-title":"Natural 3-valued logics\u2014characterization and proof theory","volume":"56","author":"Avron","year":"1991","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0030","series-title":"Proc. Logic Programming and Automated Reasoning LPAR'92","first-page":"107","article-title":"Resolution for many-valued logics","author":"Baaz","year":"1992"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50022-9_bb0035","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1006\/jsco.1995.1021","article-title":"Resolution-based theorem proving for many-valued logics","volume":"19","author":"Baaz","year":"1995","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0040","series-title":"Theorem Proving with Analytic Tableaux and Related Methods, 5th Int. Workshop, TABLEAUX'96","first-page":"65","article-title":"Combining many-valued and intuitionistic tableaux","author":"Baaz","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50022-9_rf0045","series-title":"Proc. 26th International Symposium on Multiple-valued Logic","first-page":"136","article-title":"Intuitionistic counterparts of finitely-valued logics","author":"Baaz","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0050","series-title":"Proc. Logic in Computer Science LICS","first-page":"213","article-title":"A non-elementary speed-up in proof length by structural clause form transformation","author":"Baaz","year":"1994"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50022-9_bb0055","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1005022012721","article-title":"Labeled calculi and finite-valued logics","volume":"61","author":"Baaz","year":"1998","journal-title":"Studia Logica"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0060","series-title":"Proc. 2nd Worshop on Theorem Proving with Tableaux and Related Methods","article-title":"Dual systems of sequents and tableaux for many-valued logics","author":"Baaz","year":"1992"},{"issue":"6","key":"10.1016\/B978-044450813-3\/50022-9_bb0065","first-page":"333","article-title":"Elimination of cuts in first-order finite-valued logics","volume":"29","author":"Baaz","year":"1994","journal-title":"J. Inform. Process. Cybernet. (EIK)"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0070","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1023\/A:1005026229560","article-title":"Embedding logics into product logic","volume":"61","author":"Baaz","year":"1998","journal-title":"Studia Logica"},{"issue":"6","key":"10.1016\/B978-044450813-3\/50022-9_bb0075","doi-asserted-by":"crossref","first-page":"1178","DOI":"10.1145\/195613.195637","article-title":"Mixed integer programming methods for computing nonmonotonic deductive databases","volume":"41","author":"Bell","year":"1994","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0080","series-title":"Modern uses of multiple-valued logic","first-page":"8","article-title":"A useful four-valued logic","author":"Belnap","year":"1977"},{"year":"1992","series-title":"Many-Valued Logics. 1: Theoretical Foundations","author":"Bolc","key":"10.1016\/B978-044450813-3\/50022-9_bb0085"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0090","series-title":"Newsletter of the Association for Automated Reasoning","article-title":"Problems in \u0141ukasiewicz logic","author":"Bonacina","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0095","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1016\/0747-7171(92)90009-S","article-title":"An optimality result for clause form translation","volume":"14","author":"Boy de la Tour","year":"1992","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0100","series-title":"Computer-Aided Verification: Proc. of the 2nd International Conference CAV'90","first-page":"33","article-title":"Formal verification of digital circuits using symbolic ternary system models","author":"Bryant","year":"1991"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50022-9_bb0105","doi-asserted-by":"crossref","first-page":"473","DOI":"10.2307\/2274395","article-title":"Systematization of finite many-valued logics through the method of tableaux","volume":"52","author":"Carnielli","year":"1987","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0110","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/S0747-7171(08)80043-0","article-title":"Multi-valued logic and Gr\u00f6bner bases with applications to modal logic","volume":"11\u201312","author":"Chazarain","year":"1991","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0115","series-title":"First World Conference on the Fundamentals of Artificial Intelligence WOCFAI-91","article-title":"A constraint-based approach to proof procedures for multi-valued logics","author":"Doherty","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0120","series-title":"Proc. 13th Conference on Automated Deduction","first-page":"568","article-title":"Semantic trees revisited: Some new completeness results","author":"Ferm\u00fcller","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0125","article-title":"Resolution Methods as Decision Procedures","volume":"Vol. 679","author":"Ferm\u00fcller","year":"1993"},{"year":"1983","series-title":"Proof Methods for Modal and Intuitionistic Logics","author":"Fitting","key":"10.1016\/B978-044450813-3\/50022-9_bb0130"},{"year":"1999","series-title":"Chaining techniques for automated theorem proving in many-valued logic","author":"Ganzinger","key":"10.1016\/B978-044450813-3\/50022-9_bb0135"},{"year":"1979","series-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"Garey","key":"10.1016\/B978-044450813-3\/50022-9_bb0140"},{"key":"10.1016\/B978-044450813-3\/50022-9_rf0145","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen I\u2013II","volume":"39","author":"Gentzen","year":"1934","journal-title":"Mathematische Zeitschrift"},{"key":"10.1016\/B978-044450813-3\/50022-9_rf0150","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/BF01201363","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen I\u2013II","volume":"39","author":"Gentzen","year":"1934","journal-title":"Mathematische Zeitschrift"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0150","first-page":"65","article-title":"Zum intuitionistischen Aussagenkalk\u00fcl","volume":"69","author":"G\u00f6del","year":"1932","journal-title":"Anzeiger der Akademie der Wissenschaften in Wien"},{"year":"1989","series-title":"Mehrwertige Logik. Eine Einf\u00fchrung in Theorie und Anwendungen","author":"Gottwald","key":"10.1016\/B978-044450813-3\/50022-9_rf0160"},{"year":"1993","series-title":"Fuzzy Sets and Fuzzy Logic","author":"Gottwald","key":"10.1016\/B978-044450813-3\/50022-9_bb0160"},{"year":"1996","series-title":"Logic Synthesis and Verification Algorithms","author":"Hachtel","key":"10.1016\/B978-044450813-3\/50022-9_bb0165"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0170","series-title":"Selected Papers from Computer Science Logic, CSL'90, Heidelberg, Germany","first-page":"248","article-title":"Towards an efficient tableau proof procedure for multiple-valued logics","author":"H\u00e4hnle","year":"1991"},{"year":"1994","series-title":"Automated Deduction in Multiple-Valued Logics, Vol. 10 of International Series of Monographs on Computer Science","author":"H\u00e4hnle","key":"10.1016\/B978-044450813-3\/50022-9_bb0175"},{"issue":"3,4","key":"10.1016\/B978-044450813-3\/50022-9_bb0180","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/BF01530787","article-title":"Many-valued logic and mixed integer programming","volume":"12","author":"H\u00e4hnle","year":"1994","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"6","key":"10.1016\/B978-044450813-3\/50022-9_bb0185","doi-asserted-by":"crossref","first-page":"905","DOI":"10.1093\/logcom\/4.6.905","article-title":"Short conjunctive normal forms in finitely-valued logics","volume":"4","author":"H\u00e4hnle","year":"1994","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50022-9_bb0190","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1023\/A:1005086415447","article-title":"Commodious axiomatization of quantifiers in multiple-valued logic","volume":"61","author":"H\u00e4hnle","year":"1998","journal-title":"Studia Logica"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50022-9_bb0195","first-page":"69","article-title":"Deduction in many-valued logics: a survey","volume":"IV","author":"H\u00e4hnle","year":"1997","journal-title":"Mathware & Soft Computing"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0200","series-title":"Proc. LPAR'93","first-page":"158","article-title":"Verification of switch level designs with many-valued logic","author":"H\u00e4hnle","year":"1993"},{"year":"1998","series-title":"Metamathematics of Fuzzy Logics","author":"Hajek","key":"10.1016\/B978-044450813-3\/50022-9_bb0205"},{"issue":"7","key":"10.1016\/B978-044450813-3\/50022-9_bb0210","doi-asserted-by":"crossref","first-page":"602","DOI":"10.1109\/TC.1986.1676801","article-title":"Pseudo-Boolean logic circuits","volume":"C-35","author":"Hayes","year":"1986","journal-title":"IEEE Transactions on Computers"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50022-9_bb0215","doi-asserted-by":"crossref","first-page":"395","DOI":"10.2307\/2270905","article-title":"Logic with truth values in a linearly ordered Heyting algebra","volume":"34","author":"Horn","year":"1969","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0220","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","article-title":"Constraint logic programming: A survey","volume":"19 & 20","author":"Jaffar","year":"1994","journal-title":"Journal of Logic Programming"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0225","doi-asserted-by":"crossref","first-page":"150","DOI":"10.2307\/2267778","article-title":"On a notation for ordinal numbers","volume":"3","author":"Kleene","year":"1938","journal-title":"Journal of Symbolic Logic"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50022-9_bb0230","doi-asserted-by":"crossref","first-page":"755","DOI":"10.1093\/jigpal\/6.5.755","article-title":"A relational formalization of arbitrary finite valued logics","volume":"6","author":"Konikowska","year":"1998","journal-title":"Logical Journal of the IGPL"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0235","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1016\/0743-1066(87)90007-0","article-title":"Negation in logic programming","volume":"4","author":"Kunen","year":"1987","journal-title":"Journal of Logic Programming"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0240","article-title":"A completeness theorem and a computer program for finding theorems derivable from given axioms","author":"Lee","year":"1967","journal-title":"Ph.D. Thesis, University of California, Berkely"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0245","series-title":"Texts in Theoretical Computer Science","article-title":"The Resolution Calculus","author":"Leitsch","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0250","series-title":"Automated Reasoning: Essays in Honor of Woody Bledsoe","first-page":"181","article-title":"Reasoning in paraconsistent logics","author":"Lu","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0255","series-title":"Proc. 23rd International Symposium on Multiple-Valued Logics","first-page":"48","article-title":"Signed formulas and annotated logics","author":"Lu","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0260","series-title":"The Computer Science And Engineering Handbook","first-page":"654","article-title":"Logic-based deductive reasoning in AI systems","author":"Lu","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0265","first-page":"169","article-title":"O logice tr\u00f2jwartosciowej","volume":"5","author":"\u0141ukasiewicz","year":"1920","journal-title":"Ruch Filozoficzny"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0270","first-page":"51","article-title":"Philosophische Bemerkungen zu mehrwertigen systemen des Aussagenkalk\u00fcls","volume":"23","author":"\u0141ukasiewicz","year":"1930","journal-title":"Comptes rendus des s\u00e9ances de la Soci\u00e9t\u00e9 des Sciences et des Lettres de Varsovie Cl. III"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0275","first-page":"30","article-title":"Untersuchungen \u00fcber den Aussagenkalk\u00fcl","volume":"23","author":"\u0141ukasiewicz","year":"1930","journal-title":"Comptes rendus des s\u00e9ances de la Soci\u00e9t\u00e9 des Sciences et des Lettres de Varsovie Cl. III"},{"key":"10.1016\/B978-044450813-3\/50022-9_rf0285","series-title":"Proceedings of the International Logic Programming Conference","first-page":"268","article-title":"Regular signed resolution applied to annotated logic programs","author":"Messing","year":"1995"},{"issue":"74-75-76","key":"10.1016\/B978-044450813-3\/50022-9_bb0285","first-page":"311","article-title":"A resolution principle for a class of many-valued logics","volume":"19","author":"Morgan","year":"1976","journal-title":"Logique et Analyse"},{"issue":"110\/111","key":"10.1016\/B978-044450813-3\/50022-9_bb0290","first-page":"257","article-title":"Autologic","volume":"28","author":"Morgan","year":"1985","journal-title":"Logique et Analyse"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0295","series-title":"Proceedings Workshop Computer Science Logic 90","first-page":"300","article-title":"The complexity of adaptive error-correcting codes","author":"Mundici","year":"1990"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50022-9_bb0300","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1109\/69.91059","article-title":"A Petri net model for reasoning in the presence of inconsistency","volume":"3","author":"Murata","year":"1991","journal-title":"IEEE Transactions on Knowledge and Data Engineering"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0305","series-title":"Proceedings International Symposium on Methodologies for Intelligent Systems","article-title":"Resolution and path-dissolution in multiple-valued logics","author":"Murray","year":"1991"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50022-9_bb0310","doi-asserted-by":"crossref","first-page":"237","DOI":"10.3233\/FI-1994-2135","article-title":"Adapting classical inference techniques to multiple-valued logics using signed formulas","volume":"21","author":"Murray","year":"1994","journal-title":"Fundamenta Informaticae"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50022-9_bb0315","first-page":"205","article-title":"Software agents: An overview","volume":"11","author":"Nowana","year":"1995","journal-title":"Knowledge Engineering Review"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0320","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/S0747-7171(10)80002-1","article-title":"A resolution framework for finitely-valued first-order logics","volume":"13","author":"O'Hearn","year":"1992","journal-title":"J. Symbolic Computation"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50022-9_bb0325","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1093\/jigpal\/1.1.69","article-title":"Translation methods for non-classical logics \u2014 an overview","volume":"1","author":"Ohlbach","year":"1993","journal-title":"Journal of the IGPL"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50022-9_bb0330","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/FI-1978-2102","article-title":"The resolution principle for ?+-valued logic","volume":"II","author":"Orlowska","year":"1978","journal-title":"Fundamenta Informaticae"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50022-9_bb0335","first-page":"445","article-title":"Towards a general approach for modeling actions and change in cooperating agents scenarios","volume":"4","author":"Pfalzgraf","year":"1996","journal-title":"Journal of the Interest Group in Pure and Applied Logics"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0340","series-title":"From Frege to G\u00f6del. A Source Book in Mathematical Logic, 1879\u20131931","first-page":"264","article-title":"Introduction to a general theory of elementary propositions","author":"Post","year":"1921"},{"year":"1969","series-title":"Many-Valued Logic","author":"Rescher","key":"10.1016\/B978-044450813-3\/50022-9_bb0345"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50022-9_bb0350","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"JACM"},{"year":"1952","series-title":"Many-Valued Logics","author":"Rosser","key":"10.1016\/B978-044450813-3\/50022-9_bb0355"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0360","doi-asserted-by":"crossref","first-page":"23","DOI":"10.4064\/fm-60-1-23-33","article-title":"Sequents in many valued logic I","volume":"LX","author":"Rousseau","year":"1967","journal-title":"Fundamenta Mathematic\u0153"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0365","series-title":"Proc. 13th Conference on Automated Deduction","first-page":"688","article-title":"Optimal axiomatizations for multiple-valued operators and quantifiers based on semilattices","author":"Salzer","year":"1996"},{"issue":"1\/2","key":"10.1016\/B978-044450813-3\/50022-9_bb0370","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1006\/inco.1999.2862","article-title":"Optimal axiomatizations of finitely-valued logics","volume":"162","author":"Salzer","year":"2000","journal-title":"Information and Computation"},{"year":"1993","series-title":"Logic Synthesis and Optimization","key":"10.1016\/B978-044450813-3\/50022-9_bb0375"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50022-9_bb0380","doi-asserted-by":"crossref","first-page":"159","DOI":"10.2307\/2964111","article-title":"Die Nichtaxiomatisierbarkeit des unendlichwertigen Pr\u00e4dikatenkalk\u00fcls von \u0141ukasiewicz","volume":"27","author":"Scarpellini","year":"1962","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0385","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0304-3975(88)90146-6","article-title":"Implication of clauses is undecidable","volume":"59","author":"Schmidt-Schauss","year":"1988","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0390","series-title":"Proc. 8th International Conference on Automated Deduction","first-page":"190","article-title":"Computational aspects of three-valued logic","author":"Schmitt","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0395","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1002\/malq.19550010402","article-title":"Methoden zur Axiomatisierung beliebiger Aussagen- und Pr\u00e4dikatenkalk\u00fcle","volume":"1","author":"Schr\u00f6ter","year":"1955","journal-title":"Zeitschrift f\u00fcr math. Logik und Grundlagen der Mathematik"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0400","article-title":"Fibered Structures and Applications to Automated Theorem Proving in Certain Classes of Finitely-Valued Logics and to Modeling Interacting Systems","author":"Sofronie-Stokkermans","year":"1997","journal-title":"PhD thesis, RISC-Linz, J. Kepler University Linz, Austria"},{"key":"10.1016\/B978-044450813-3\/50022-9_rf0410","series-title":"Proceedings of the 13th European Conference on Artificial Intelligence (ECAI 98)","first-page":"410","article-title":"On translation of finitely-valued logics to classical first-order logic","author":"Sofronie-Stokkermans","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0410","article-title":"Automated theorem proving by resolution for finitely-valued logics based on distributive lattices with operators","author":"Sofronie-Stokkermans","year":"1999","journal-title":"Multiple-Valued Logic \u2014 An International Journal"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0415","series-title":"Proceedings of the 29th IEEE International Symposium on Multiple-Valued Logic (ISMVL 99)","first-page":"242","article-title":"Representation theorems and automated theorem proving in non-classical logics","author":"Sofronie-Stokkermans","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0420","series-title":"Automated Deduction in Classical and Non-Classical Logics","first-page":"268","article-title":"Resolution-based theorem proving for SHn-logics","author":"Sofronie-Stokkermans","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0425","series-title":"Proc. of Algebraic Logic and Universal Algebra in Computer Science Conf.","first-page":"227","article-title":"The resolution rule: An algebraic perspective","author":"Stachniak","year":"1988"},{"year":"1996","series-title":"Resolution Proof Systems: an Algebraic Theory","author":"Stachniak","key":"10.1016\/B978-044450813-3\/50022-9_bb0430"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0435","doi-asserted-by":"crossref","first-page":"333","DOI":"10.3233\/FI-1990-13307","article-title":"Resolution in the domain of strongly finite logics","volume":"8","author":"Stachniak","year":"1990","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0440","article-title":"A Categorical Framework and Calculus for Critical-Pair Completion","author":"Stokkermans","year":"1995","journal-title":"PhD thesis, RISC-Linz, Johannes-Kepler-Universit\u00e4t, Linz"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50022-9_bb0445","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1006\/jsco.1999.0262","article-title":"A categorical critical-pair completion algorithm","volume":"27","author":"Stokkermans","year":"1999","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0450","first-page":"37","article-title":"La m\u00e9thode de Smullyan de construire le calcul n-valent de \u0141ukasiewicz avec implication et n\u00e9gation","volume":"2","author":"Such\u00f3n","year":"1974","journal-title":"Reports on Mathematical Logic, Universities of Cracow and Katowice"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0455","series-title":"Computer Science and Multiple-Valued Logics","first-page":"143","article-title":"An algorithm for axiomatizing every finite logic","author":"Surma","year":"1984"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50022-9_bb0460","doi-asserted-by":"crossref","first-page":"851","DOI":"10.2307\/2274139","article-title":"Intuitionistic fuzzy logic and intuitionistic fuzzy set theory","volume":"49","author":"Takeuti","year":"1984","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50022-9_bb0465","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1017\/S0269888900008122","article-title":"Intelligent agents: Theory and practice","volume":"10","author":"Wooldridge","year":"1995","journal-title":"Knowledge Engineering Review"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50022-9_bb0470","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1080\/11663081.1998.10510951","article-title":"An algebraic method to decide the deduction problem in many-valued logics","volume":"8","author":"Wu","year":"1998","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"10.1016\/B978-044450813-3\/50022-9_bb0475","article-title":"Proof theory of finite-valued logics","author":"Zach","year":"1993","journal-title":"Master's thesis, Institut f\u00fcr Algebra und Diskrete Mathematik, TU Wien"}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500229?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500229?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2021,8,14]],"date-time":"2021-08-14T23:35:36Z","timestamp":1628984136000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500229"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":95,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50022-9","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}