{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:19:01Z","timestamp":1750306741699,"version":"3.41.0"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,12,12]],"date-time":"2014-12-12T00:00:00Z","timestamp":1418342400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["280-10"],"award-info":[{"award-number":["280-10"]}],"id":[{"id":"10.13039\/501100003977","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2015,3]]},"abstract":"<jats:p>We develop a fully algorithmic approach to \u201ctaming\u201d logics expressed Hilbert style, that is, reformulating them in terms of analytic sequent calculi and useful semantics. Our approach applies to Hilbert calculi extending the positive fragment of propositional classical logic with axioms of a certain general form that contain new unary connectives. Our work encompasses various results already obtained for specific logics. It can be applied to new logics, as well as to known logics for which an analytic calculus or a useful semantics has so far not been available. A Prolog implementation of the method is described.<\/jats:p>","DOI":"10.1145\/2661636","type":"journal-article","created":{"date-parts":[[2014,12,16]],"date-time":"2014-12-16T13:39:54Z","timestamp":1418737194000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Taming Paraconsistent (and Other) Logics"],"prefix":"10.1145","volume":"16","author":[{"given":"Agata","family":"Ciabattoni","sequence":"first","affiliation":[{"name":"Vienna University of Technology, Wien, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ori","family":"Lahav","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lara","family":"Spendier","sequence":"additional","affiliation":[{"name":"Vienna University of Technology, Wien, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anna","family":"Zamansky","sequence":"additional","affiliation":[{"name":"University of Haifa, Haifa, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,12,12]]},"reference":[{"volume-title":"We Will Show Them: Essays in Honor of Dov Gabbay","author":"Avron Arnon","key":"e_1_2_1_1_1","unstructured":"Arnon Avron . 2005. Logical non-determinism as a tool for logical modularity: An introduction . In We Will Show Them: Essays in Honor of Dov Gabbay . College Publications , 105--124. Arnon Avron. 2005. Logical non-determinism as a tool for logical modularity: An introduction. In We Will Show Them: Essays in Honor of Dov Gabbay. College Publications, 105--124."},{"volume-title":"Handbook of Paraconsistency, Jean-Yves Beziau, Walter A","author":"Avron Arnon","key":"e_1_2_1_2_1","unstructured":"Arnon Avron . 2007. Non-deterministic semantics for families of paraconsistent logics . In Handbook of Paraconsistency, Jean-Yves Beziau, Walter A . Carnielli, and Dov Gabbay (Eds.). Studies in Logic, Vol. 9 . College Publications , 285--320. Arnon Avron. 2007. Non-deterministic semantics for families of paraconsistent logics. In Handbook of Paraconsistency, Jean-Yves Beziau, Walter A. Carnielli, and Dov Gabbay (Eds.). Studies in Logic, Vol. 9. College Publications, 285--320."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11787-006-0003-6"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.20"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exs039"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exi001"},{"volume-title":"Handbook of Philosophical Logic, Dov Gabbay and Franz Guenthner (Eds.).","author":"Avron Arnon","key":"e_1_2_1_7_1","unstructured":"Arnon Avron and Anna Zamansky . 2011. Non-deterministic semantics for logical systems: A survey . In Handbook of Philosophical Logic, Dov Gabbay and Franz Guenthner (Eds.). Vol. 16 . Springer , 227--304. Arnon Avron and Anna Zamansky. 2011. Non-deterministic semantics for logical systems: A survey. In Handbook of Philosophical Logic, Dov Gabbay and Franz Guenthner (Eds.). Vol. 16. Springer, 227--304."},{"volume-title":"Towards an expert system for many-valued logics","author":"Baaz Matthias","key":"e_1_2_1_8_1","unstructured":"Matthias Baaz , Christian G. Ferm\u00fcller , Gernot Salzer , and Richard Zach . 1996. M Ultlog 1.0 : Towards an expert system for many-valued logics . In Proceedings of CADE. Springer , 226--230. Matthias Baaz, Christian G. Ferm\u00fcller, Gernot Salzer, and Richard Zach. 1996. MUltlog 1.0: Towards an expert system for many-valued logics. In Proceedings of CADE. Springer, 226--230."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9273-x"},{"volume-title":"Bounded proofs and step frames","author":"Bezhanishvili Nick","key":"e_1_2_1_10_1","unstructured":"Nick Bezhanishvili and Silvio Ghilardi . 2013. Bounded proofs and step frames . In Proceedings of TABLEAUX. Springer , 44--58. Nick Bezhanishvili and Silvio Ghilardi. 2013. Bounded proofs and step frames. In Proceedings of TABLEAUX. Springer, 44--58."},{"volume-title":"Handbook of Proof Theory, Samuel R","author":"Buss Samuel R.","key":"e_1_2_1_11_1","unstructured":"Samuel R. Buss . 1998. An introduction to proof theory . In Handbook of Proof Theory, Samuel R . Buss (Ed.). Vol. 137 . Elsevier , 1--78. Samuel R. Buss. 1998. An introduction to proof theory. In Handbook of Proof Theory, Samuel R. Buss (Ed.). Vol. 137. Elsevier, 1--78."},{"volume-title":"Handbook of Philosophical Logic, Dov Gabbay and Franz Guenthner (Eds.).","author":"Carnielli Walter A.","key":"e_1_2_1_12_1","unstructured":"Walter A. Carnielli , Marcelo E. Coniglio , and Jo\u00e3o Marcos . 2007. Logics of formal inconsistency . In Handbook of Philosophical Logic, Dov Gabbay and Franz Guenthner (Eds.). Vol. 14 . Springer , 15--107. Walter A. Carnielli, Marcelo E. Coniglio, and Jo\u00e3o Marcos. 2007. Logics of formal inconsistency. In Handbook of Philosophical Logic, Dov Gabbay and Franz Guenthner (Eds.). Vol. 14. Springer, 15--107."},{"key":"e_1_2_1_13_1","series-title":"Lecture Notes in Pure and Applied Mathematics","volume-title":"Carnielli and Jo\u00e3o Marcos","author":"Walter","year":"2002","unstructured":"Walter A. Carnielli and Jo\u00e3o Marcos . 2002 . A taxonomy of C-systems. In Paraconsistency : The Logical Way to the Inconsistent, Walter A. Carnielli, Marcelo E. Coniglio, and Itala D\u2019Ottaviano (Eds.). Number 228 in Lecture Notes in Pure and Applied Mathematics . Marcel Dekker , 1--94. Walter A. Carnielli and Jo\u00e3o Marcos. 2002. A taxonomy of C-systems. In Paraconsistency: The Logical Way to the Inconsistent, Walter A. Carnielli, Marcelo E. Coniglio, and Itala D\u2019Ottaviano (Eds.). Number 228 in Lecture Notes in Pure and Applied Mathematics. Marcel Dekker, 1--94."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.39"},{"volume-title":"Logical Foundations of Computer Science","author":"Ciabattoni Agata","key":"e_1_2_1_15_1","unstructured":"Agata Ciabattoni , Ori Lahav , Lara Spendier , and Anna Zamansky . 2013. Automated support for the investigation of paraconsistent and other logics . In Logical Foundations of Computer Science . Springer , 119--133. Agata Ciabattoni, Ori Lahav, Lara Spendier, and Anna Zamansky. 2013. Automated support for the investigation of paraconsistent and other logics. In Logical Foundations of Computer Science. Springer, 119--133."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.10.004"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093891487"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-009-9173-6"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-013-9533-0"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_6"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/2029664.2029681"},{"volume-title":"A Proof Assistant for Higher-order Logic","author":"Nipkow Topias","key":"e_1_2_1_22_1","unstructured":"Topias Nipkow , Lawrence C. Paulson , and Markus Wenzel . 2002. Isabelle\/HOL : A Proof Assistant for Higher-order Logic . Springer . Topias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle\/HOL: A Proof Assistant for Higher-order Logic. Springer."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/4.1.109"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_7"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2661636","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2661636","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:15Z","timestamp":1750231695000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2661636"}},"subtitle":["An Algorithmic Approach"],"short-title":[],"issued":{"date-parts":[[2014,12,12]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,3]]}},"alternative-id":["10.1145\/2661636"],"URL":"https:\/\/doi.org\/10.1145\/2661636","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2014,12,12]]},"assertion":[{"value":"2014-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-12-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}