{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T11:50:45Z","timestamp":1649159445568},"reference-count":81,"publisher":"Informa UK Limited","issue":"3-4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Non-Classical Logics"],"published-print":{"date-parts":[[2006,1]]},"DOI":"10.3166\/jancl.16.367-408","type":"journal-article","created":{"date-parts":[[2007,4,11]],"date-time":"2007-04-11T13:06:10Z","timestamp":1176296770000},"page":"367-408","source":"Crossref","is-referenced-by-count":10,"title":["An efficient relational deductive system for propositional non-classical logics"],"prefix":"10.1080","volume":"16","author":[{"given":"Andrea","family":"Formisano","sequence":"first","affiliation":[{"name":"a Dipartimento di Informatica , Universit\u00e0 di L'Aquila , via Vetoio, loc. Coppito, I-67010 , L'Aquila , Italy"}]},{"given":"Marianna","family":"Nicolosi-Asmundo","sequence":"additional","affiliation":[{"name":"b Dipartimento di Matematica e Informatica , Universit\u00e0 di Catania , viale A. Doria 6, I-95125 , Catania , Italy"}]}],"member":"301","published-online":{"date-parts":[[2012,4,13]]},"reference":[{"key":"CIT0001","volume-title":"Two Solutions to Incorporate Zero, Successor and Equality in Binary Decision Diagrams","author":"BADBAN B.","year":"2002"},{"key":"CIT0002","volume-title":"Proceedings of CSICC04","author":"BADBAN B."},{"issue":"1","key":"CIT0003","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.apal.2004.10.005","volume":"133","author":"BADBAN B.","year":"2005","journal-title":"Annals of Pure and Applied Logic"},{"key":"CIT0004","first-page":"91","volume-title":"Proceedings, International Conference on Theorem Proving with Analytic Tableaux and Related Methods, vol. 1227 ofLNCS","author":"BECKERT B."},{"key":"CIT0005","volume-title":"Machine Support of Relational Computations: The Kiel RELVIEW System","author":"BEHNKE R.","year":"1997"},{"key":"CIT0006","first-page":"241","volume-title":"6th International Conference on Relational Methods in Computer Science, RelMiCS 2001, vol. 2561 of LNCS","author":"BERGHAMMER R."},{"issue":"9","key":"CIT0007","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1109\/12.537122","volume":"45","author":"BOLLIG B.","year":"1996","journal-title":"IEEE Transactions on Computers"},{"key":"CIT0008","volume-title":"Advances in Computing Science","author":"BRINK C.","year":"1997"},{"key":"CIT0009","first-page":"372","volume-title":"Proceedings, 9th Annual IEEE Symposium on Logic in Computer Science","author":"BROWN C."},{"key":"CIT0010","first-page":"56","volume-title":"The 3rd International Symposium on Logical Foundations of Computer Science","author":"BROWN C."},{"key":"CIT0011","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"CIT0012","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"issue":"2","key":"CIT0013","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1016\/S0304-3975(01)00355-3","volume":"293","author":"CANTONE D.","year":"2003","journal-title":"Theoretical Computer Science"},{"key":"CIT0014","doi-asserted-by":"crossref","unstructured":"DEL CERRO , L. F. FAUTHOUX , D. GASQUET , O. HERZIG , A. LONGIN , D. and MASSACCI , F.Lotrec: the Generic Tableau Prover for Modal and Description Logics453\u2013458. Gor\u00e9 et al. [GOR 01]","DOI":"10.1007\/3-540-45744-5_38"},{"issue":"1","key":"CIT0015","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1016\/0167-6423(95)00025-9","volume":"26","author":"CURTIS S.","year":"1996","journal-title":"Science of Computer Programming"},{"key":"CIT0016","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/BF00156916","volume":"1","author":"D'AGOSTINO M.","year":"1992","journal-title":"Journal of Logic, Language and Information"},{"key":"CIT0017","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/4.3.285"},{"key":"CIT0018","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-1754-0_2","volume-title":"Tableau Methods for Classical Propositional Logic","author":"D'AGOSTINO M.","year":"1999"},{"key":"CIT0019","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-1754-0"},{"key":"CIT0020","first-page":"264","volume-title":"Proceedings of the European Workshop on Logics in Artificial Intelligence (JELIA-98), vol. 1489 of LNCS","author":"DAWSON J. E."},{"key":"CIT0021","series-title":"An EATCS Series","volume-title":"Monographs in Theoretical Computer Science","author":"DEMRI S.","year":"2002"},{"issue":"3","key":"CIT0022","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1023\/A:1004764610651","volume":"29","author":"D\u00dcNTSCH I.","year":"2000","journal-title":"Journal of Philosophical Logic"},{"key":"CIT0023","first-page":"277","volume-title":"Relational Methods for Computer Science Applications","author":"D\u00dcNTSCH I.","year":"2001"},{"key":"CIT0024","first-page":"132","volume":"1","author":"D\u00dcNTSCH I.","year":"2004","journal-title":"Journal on Relational Methods in Computer Science"},{"key":"CIT0025","volume-title":"LIBRA: a Lazy Interpreter of Binary Relational Algebra","author":"DWYER B.","year":"1995"},{"issue":"3","key":"CIT0026","volume":"44","author":"FORMISANO A.","year":"2001","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"CIT0027","doi-asserted-by":"crossref","unstructured":"FORMISANO , A. OMODEO , E. G. and TEMPERINI , M.Instructing Equational Set- Reasoning with Otter152\u2013167. Gor\u00e9 et al. [GOR 01]","DOI":"10.1007\/3-540-45744-5_12"},{"key":"CIT0028","volume-title":"Declarative Programming","volume":"48","author":"FORMISANO A.","year":"2001"},{"key":"CIT0029","first-page":"1","volume-title":"TABLEAUX 2005 Position Papers and Tutorial Descriptions","author":"FORMISANO A.","year":"2005"},{"key":"CIT0030","volume-title":"Theory and Applications of Relational Structures as Knowledge Instruments II","author":"FORMISANO A.","year":"2006"},{"key":"CIT0031","volume-title":"Proof Search without Backtracking for Free Variable Tableaux","author":"GIESE M.","year":"2002"},{"key":"CIT0032","author":"GOLI\u0143SKA-PILAREK J.","year":"2006","journal-title":"Studia Logica"},{"key":"CIT0033","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093635335"},{"key":"CIT0034","first-page":"198","volume-title":"CSL, vol. 1258 of LNCS","author":"GOR\u00c9 R.","year":"1996"},{"key":"CIT0035","first-page":"239","volume-title":"Proceedings of the 15th International Conference on Automated Deduction, vol. 1502 of LNCS","author":"GOR\u00c9 R."},{"key":"CIT0036","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-1754-0_6","volume-title":"Tableau Methods for Modal and Temporal Logics","author":"GOR\u00c9 R.","year":"1999"},{"key":"CIT0037","doi-asserted-by":"crossref","volume-title":"Automated Reasoning: First International Joint Conference, IJCAR 2001. Proceedings, vol. 2083 of LNCS","author":"GOR\u00c9 R.","DOI":"10.1007\/3-540-45744-5"},{"key":"CIT0038","first-page":"499","volume-title":"Proceedings of the 12th International Conference on Automated Deduction, vol. 814 of LNCS","author":"GOUBAULT J.","year":"1994"},{"key":"CIT0039","first-page":"541","volume-title":"Proceedings 8th International Symposium on Methodologies for Intelligent Systems ISMIS, vol. 869 of LNCS","author":"GOUBAULT J."},{"issue":"6","key":"CIT0040","doi-asserted-by":"crossref","first-page":"827","DOI":"10.1093\/jigpal\/3.6.827","volume":"3","author":"GOUBAULT J.","year":"1995","journal-title":"Journal of the IGPL"},{"key":"CIT0041","volume-title":"Implementing Tableaux by Decision Diagrams","author":"GOUBAULT-LARRECQ J.","year":"1996"},{"key":"CIT0042","first-page":"161","volume-title":"Logic for Programming and Automated Reasoning: 7th International Conference, LPAR 2000, vol. 1955 of LNCS","author":"GROOTE J. F."},{"issue":"1","key":"CIT0043","first-page":"1","volume":"57","author":"GROOTE J. F.","year":"2003","journal-title":"Journal of Logic and Algebraic Programing"},{"key":"CIT0044","volume-title":"Proc. of AMAST93","author":"HATTENSPERGER C."},{"issue":"1","key":"CIT0045","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1016\/0022-0000(80)90007-0","volume":"20","author":"HENNESSY M. C. B.","year":"1980","journal-title":"Journal of Computer and System Sciences"},{"key":"CIT0046","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093870378"},{"key":"CIT0047","volume-title":"Proceedings of the 8th International Conference on Relational Methods in Computer Science (RelMiCS 8)","author":"J\u00c4RVINEN J."},{"key":"CIT0048","first-page":"51","author":"JIFENG H.","year":"1986","journal-title":"Fundamenta Informaticae"},{"issue":"1","key":"CIT0049","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","volume":"27","author":"KORF R. E.","year":"1985","journal-title":"Artificial Intelligence"},{"key":"CIT0050","volume-title":"Problems of Expressibility in Finite Languages","author":"KWATINETZ M.","year":"1981"},{"key":"CIT0051","volume-title":"ReVAT - Relational Validator by Analytic Tableaux","author":"LEE G.","year":"2002"},{"key":"CIT0052","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-1754-0_3","volume-title":"First-Order Tableau Methods","author":"LETZ R.","year":"1999"},{"key":"CIT0053","volume-title":"A Logic of Typed Relations and its Applications to Relational Databases","author":"MACCAULL W.","year":"2003"},{"key":"CIT0054","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0168-0072(83)90055-6","volume":"25","author":"MADDUX R. D.","year":"1983","journal-title":"Annals of Pure and Applied Logic"},{"issue":"3","key":"CIT0055","doi-asserted-by":"crossref","first-page":"421","DOI":"10.1007\/BF00370681","volume":"50","author":"MADDUX R. D.","year":"1991","journal-title":"Studia Logica"},{"key":"CIT0056","first-page":"380","volume-title":"Proceedings of the 14th International Conference on Automated Deduction, vol. 1249 of LNCS","author":"VON OHEIMB D."},{"key":"CIT0057","doi-asserted-by":"crossref","first-page":"1403","DOI":"10.1016\/B978-044450813-3\/50023-0","volume-title":"Handbook of Automated Reasoning","author":"OHLBACH H. J.","year":"2001"},{"issue":"6","key":"CIT0058","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1016\/0020-0190(88)90218-9","volume":"27","author":"OR\u0141OWSKA E.","year":"1988","journal-title":"Information Processing Letters"},{"key":"CIT0059","first-page":"443","volume-title":"Algebraic Logic, vol. 54 of Colloquia mathematica Societatis Janos Bolyai","author":"OR\u0141OWSKA E.","year":"1991"},{"issue":"4","key":"CIT0060","doi-asserted-by":"crossref","first-page":"1425","DOI":"10.2307\/2275375","volume":"57","author":"OR\u0141OWSKA E.","year":"1992","journal-title":"Journal of Symbolic Logic"},{"key":"CIT0061","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-94-015-8273-5_11","volume-title":"Philosophical Logic in Poland","author":"OR\u0141OWSKA E.","year":"1994"},{"key":"CIT0062","first-page":"249","volume-title":"Time and Logic \u2014 A Computational Approach","author":"OR\u0141OWSKA E.","year":"1995"},{"key":"CIT0063","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/978-94-017-2798-3_5","volume-title":"Proof Theory of Modal Logic","volume":"2","author":"OR\u0141OWSKA E.","year":"1996"},{"key":"CIT0064","series-title":"Advances in Computing Science, chapter 6","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1007\/978-3-7091-6510-2_6","volume-title":"Relational Methods in Computer Science","author":"OR\u0141OWSKA E.","year":"1997"},{"key":"CIT0065","first-page":"147","volume-title":"Logic, Methodology and Philosophy of Science. Proceedings of the 12th International Congress","author":"OR\u0141OWSKA E."},{"key":"CIT0066","first-page":"769","volume-title":"Proceedings of MFCS, vol. 3618 of LNCS","author":"VAN DE POL J."},{"key":"CIT0067","first-page":"67","volume-title":"GWAI, vol. 671 of LNCS","author":"POSEGGA J.","year":"1992"},{"issue":"6","key":"CIT0068","doi-asserted-by":"crossref","first-page":"697","DOI":"10.1093\/logcom\/5.6.697","volume":"5","author":"POSEGGA J.","year":"1995","journal-title":"Journal of Logic and Computation"},{"key":"CIT0069","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-1754-0_10","volume-title":"Implementing Semantic Tableaux","author":"POSEGGA J.","year":"1999"},{"key":"CIT0070","volume-title":"The Mathematics of Metamathematics","author":"RASIOWA H.","year":"1963"},{"key":"CIT0071","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1002\/malq.19820281408","volume":"28","author":"SCH\u00d6NFELD W.","year":"1982","journal-title":"Zeitschrift fuer Mathematische Logic und Grundlagen der Mathematik"},{"issue":"1","key":"CIT0072","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/BF01384237","volume":"5","author":"SCHNEIDER K.","year":"1994","journal-title":"Formal Methods in System Design"},{"issue":"1","key":"CIT0073","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1006\/inco.1999.2863","volume":"162","author":"SCH\u00dcTZ H.","year":"2000","journal-title":"Information and Computation"},{"key":"CIT0074","first-page":"177","volume-title":"Proceedings of the 17th International Conference on Automated Deduction, vol. 1831 of LNCS","author":"SINZ C."},{"key":"CIT0075","volume-title":"First-Order Logic","author":"SMULLYAN R. M.","year":"1995"},{"key":"CIT0076","volume-title":"A Formalization of Set Theory without Variables, vol. 41 of Colloquium Publications","author":"TARSKI A."},{"issue":"1","key":"CIT0077","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/S0166-218X(03)00297-X","volume":"138","author":"WEGENER I.","year":"2004","journal-title":"Discrete Applied Mathematics"},{"key":"CIT0078","first-page":"17","volume-title":"Proceedings of 5th LOPSTR, vol. 1048 of LNCS","author":"WUNDERWALD J. E."},{"key":"CIT0079","volume-title":"Web repository of computational tools for non-Classical logics, AiML"},{"key":"CIT0080","volume-title":"Web reference for SICStus Prolog"},{"issue":"1","key":"CIT0081","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/S1567-8326(01)00013-3","volume":"49","author":"ZANTEMA H.","year":"2001","journal-title":"Journal of Logic and Algebraic Programing"}],"container-title":["Journal of Applied Non-Classical Logics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.tandfonline.com\/doi\/pdf\/10.3166\/jancl.16.367-408","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T07:28:33Z","timestamp":1556350113000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.tandfonline.com\/doi\/full\/10.3166\/jancl.16.367-408"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,1]]},"references-count":81,"journal-issue":{"issue":"3-4","published-online":{"date-parts":[[2012,4,13]]},"published-print":{"date-parts":[[2006,1]]}},"alternative-id":["10.3166\/jancl.16.367-408"],"URL":"https:\/\/doi.org\/10.3166\/jancl.16.367-408","relation":{},"ISSN":["1166-3081","1958-5780"],"issn-type":[{"value":"1166-3081","type":"print"},{"value":"1958-5780","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,1]]}}}