{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,17]],"date-time":"2025-04-17T15:48:35Z","timestamp":1744904915703},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2006,9,22]],"date-time":"2006-09-22T00:00:00Z","timestamp":1158883200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2007,1,17]]},"DOI":"10.1007\/s10817-006-9029-y","type":"journal-article","created":{"date-parts":[[2006,10,7]],"date-time":"2006-10-07T23:21:04Z","timestamp":1160263264000},"page":"3-20","source":"Crossref","is-referenced-by-count":4,"title":["Axiomatizing the Skew Boolean Propositional Calculus"],"prefix":"10.1007","volume":"37","author":[{"given":"R.","family":"Veroff","sequence":"first","affiliation":[]},{"given":"M.","family":"Spinks","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,9,22]]},"reference":[{"key":"9029_CR1","first-page":"23","volume-title":"G\u00f6del\u201996: Logical Foundations of Mathematics, Computer Science, and Physics, vol. 6 of Lecture Notes in Logic","author":"M. Baaz","year":"1996","unstructured":"Baaz, M.: Infinite-valued G\u00f6del logic with 0-1-projections and relativisations. In: H\u00e1jek, Petr (ed.) G\u00f6del\u201996: Logical Foundations of Mathematics, Computer Science, and Physics, vol. 6 of Lecture Notes in Logic, pp. 23\u201333. Springer, Heidelberg New York (1996)"},{"key":"9029_CR2","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1109\/ISMVL.1991.130704","volume-title":"Proceedings of the Twenty-first International Symposium on Multiple-Valued Logic","author":"R.J. Bignall","year":"1991","unstructured":"Bignall, R.J.: A non-commutative multiple-valued logic. In: Miller, D.M. (ed.) Proceedings of the Twenty-first International Symposium on Multiple-Valued Logic, pp. 49\u201354. IEEE Computer Society, Los Alamitos, CA (1991)"},{"key":"9029_CR3","unstructured":"Bignall, R.J., Spinks, M., Veroff, R.: On the assertional logics of the generic pointed discriminator and generic pointed fixedpoint discriminator varieties. Manuscript (2004)"},{"key":"9029_CR4","doi-asserted-by":"crossref","unstructured":"Blok, W.J., Pigozzi, D.: Algebraisable logics. Mem. Am. Math. Soc. 77(396) (1989)","DOI":"10.1090\/memo\/0396"},{"key":"9029_CR5","unstructured":"Blok, W.J., Pigozzi, D.: Abstract algebraic logic and the deduction theorem. Bull. Symb. Log., to appear"},{"key":"9029_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-8130-3","volume-title":"A Course in Universal Algebra. Number 78 in Graduate Texts in Mathematics","author":"S. Burris","year":"1981","unstructured":"Burris, S., Sankappanavar, H.P.: A Course in Universal Algebra. Number 78 in Graduate Texts in Mathematics. Springer, Berlin Heidelberg New York (1981)"},{"key":"9029_CR7","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/j.apal.2003.11.008","volume":"127","author":"J. Czelakowski","year":"2004","unstructured":"Czelakowski, J., Pigozzi, D.: Fregean logics. Ann. Pure Appl. Logic 127, 17\u201376 (2004)","journal-title":"Ann. Pure Appl. Logic"},{"key":"9029_CR8","doi-asserted-by":"crossref","first-page":"481","DOI":"10.2307\/2586552","volume":"65","author":"J.M. Font","year":"2000","unstructured":"Font, J.M., Rius, M.: An abstract algebraic logic approach to tetravalent modal logics. J. Symb. Log. 65, 481\u2013518 (2000)","journal-title":"J. Symb. Log."},{"key":"9029_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-011-5300-3","volume-title":"Metamathematics of Fuzzy Logic, vol. 4 of Trends in Logic","author":"P. H\u00e1jek","year":"1998","unstructured":"H\u00e1jek, P.: Metamathematics of Fuzzy Logic, vol. 4 of Trends in Logic. Kluwer, Dordercht (1998)"},{"key":"9029_CR10","unstructured":"Hillenbrand, T., et al.: Waldmeister. http:\/\/www.waldmeister.org"},{"key":"9029_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1305\/ndjfl\/1027953481","volume":"41","author":"L. Humberstone","year":"2000","unstructured":"Humberstone, L.: An intriguing logic with two implicational connectives. Notre Dame J. Form. Log. 41, 1\u201341 (2000)","journal-title":"Notre Dame J. Form. Log."},{"key":"9029_CR12","unstructured":"Humberstone, L.: Identical twins, deduction theorems and pattern functions: Exploring the implicative ${BCSK}$ fragment of $\\mathbf{S5}$ . J. Philos. Logic, to appear"},{"key":"9029_CR13","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1305\/ndjfl\/1093870762","volume":"26","author":"I. Loureiro","year":"1985","unstructured":"Loureiro, I.: Principal congruences of tetravalent modal algebras. Notre Dame J. Form. Log. 26, 76\u201380 (1985)","journal-title":"Notre Dame J. Form. Log."},{"key":"9029_CR14","first-page":"1","volume":"2","author":"J. McCharen","year":"1976","unstructured":"McCharen, J., Overbeek, R., Wos, L.: Complexity and related enhancements for automated theorem-proving programs. Comput. Math. Appl. 2, 1\u201316 (1976)","journal-title":"Comput. Math. Appl."},{"key":"9029_CR15","doi-asserted-by":"crossref","unstructured":"McCune, W.: OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94\/6, Argonne National Laboratory, Argonne, Illinois (1994)","DOI":"10.2172\/10129052"},{"issue":"4","key":"9029_CR16","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1007\/s00012-004-1902-0","volume":"52","author":"W. McCune","year":"2005","unstructured":"McCune, W., Padmanabhan, R., Rose, M., Veroff, R.: Automated discovery of single axioms for ortholattices. Algebra Univers. 52(4), 541\u2013549 (2005)","journal-title":"Algebra Univers."},{"key":"9029_CR17","unstructured":"McCune, W.: Prover9. http:\/\/www.mcs.anl.gov\/~mccune\/prover9\/"},{"key":"9029_CR18","volume-title":"An Algebraic Approach to Non-Classical Logics. Number 78 in Studies in Logic and the Foundations of Mathematics","author":"H. Rasiowa","year":"1974","unstructured":"Rasiowa, H.: An Algebraic Approach to Non-Classical Logics. Number 78 in Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1974)"},{"key":"9029_CR19","first-page":"255","volume":"6","author":"M. Spinks","year":"2000","unstructured":"Spinks, M.: A non-classical extension of classical implicative propositional logic. Bull. Symb. Log. 6, 255 (2000). (Presented at the Austral. Assoc. Logic Annual Conference, Melbourne, July 1999.)","journal-title":"Bull. Symb. Log."},{"key":"9029_CR20","first-page":"264","volume":"9","author":"M. Spinks","year":"2003","unstructured":"Spinks, M.: On BCSK logic. Bull. Symb. Log. 9, 264 (2003). (Presented at the Austral. Assoc. Logic Annual Conference, Canberra, Dec. 2002.)","journal-title":"Bull. Symb. Log."},{"issue":"3","key":"9029_CR21","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/BF00252178","volume":"16","author":"R. Veroff","year":"1996","unstructured":"Veroff, R.: Using hints to increase the effectiveness of an automated reasoning program: Case studies. J. Autom. Reason. 16(3), 223\u2013239 (1996)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9029_CR22","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1023\/A:1010639725972","volume":"27","author":"R. Veroff","year":"2001","unstructured":"Veroff, R.: Solving open questions and other challenge problems using proof sketches. J. Autom. Reason. 27(2), 157\u2013174 (2001)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9029_CR23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1027322305654","volume":"31","author":"R. Veroff","year":"2003","unstructured":"Veroff, R.: A shortest 2-basis for Boolean algebra in terms of the Sheffer stroke. J. Autom. Reason. 31(1), 1\u20139 (2003)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9029_CR24","first-page":"299","volume":"27","author":"V. Vychodil","year":"2006","unstructured":"Vychodil, V., Chajda, I.: A note on residuated lattices with globalization. Int. J. Pure Appl. Math., 27(3), 299\u2013303 (2006)","journal-title":"Int. J. Pure Appl. Math."},{"issue":"1","key":"9029_CR25","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1142\/S0218213006002540","volume":"15","author":"L. Wos","year":"2006","unstructured":"Wos, L.: Milestones for automated reasoning. Int. J. Artif. Intell. 15(1), 3\u201319 (2006)","journal-title":"Int. J. Artif. Intell."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9029-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-006-9029-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9029-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:46Z","timestamp":1559265706000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-006-9029-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,9,22]]},"references-count":25,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2007,1,17]]}},"alternative-id":["9029"],"URL":"https:\/\/doi.org\/10.1007\/s10817-006-9029-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,9,22]]}}}