{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T16:50:33Z","timestamp":1776271833575,"version":"3.50.1"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2018,12,4]],"date-time":"2018-12-04T00:00:00Z","timestamp":1543881600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2019,8]]},"DOI":"10.1007\/s00153-018-0653-0","type":"journal-article","created":{"date-parts":[[2018,12,4]],"date-time":"2018-12-04T16:20:31Z","timestamp":1543940431000},"page":"605-625","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Cut elimination for entailment relations"],"prefix":"10.1007","volume":"58","author":[{"given":"Davide","family":"Rinaldi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6768-4457","authenticated-orcid":false,"given":"Daniel","family":"Wessel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,12,4]]},"reference":[{"key":"653_CR1","unstructured":"Aczel, P., Rathjen, M.: Notes on constructive set theory. Technical report, Institut Mittag\u2013Leffler, 2000\u20132001. Report No. 40"},{"issue":"1","key":"653_CR2","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/BF02952513","volume":"5","author":"E Artin","year":"1927","unstructured":"Artin, E.: \u00dcber die Zerlegung definiter Funktionen in Quadrate. Abh. Math. Sem. Univ. Hambg. 5(1), 100\u2013115 (1927)","journal-title":"Abh. Math. Sem. Univ. Hambg."},{"issue":"1","key":"653_CR3","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/BF02952512","volume":"5","author":"E Artin","year":"1927","unstructured":"Artin, E., Schreier, O.: Algebraische Konstruktion reeller K\u00f6rper. Abh. Math. Sem. Univ. Hambg. 5(1), 85\u201399 (1927)","journal-title":"Abh. Math. Sem. Univ. Hambg."},{"key":"653_CR4","doi-asserted-by":"crossref","unstructured":"Cederquist, J., Coquand, T.: Entailment relations and distributive lattices. In: Buss, S.R., H\u00e1jek,P., Pudl\u00e1k, P. (eds.) Logic colloquium \u201998. Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Prague, Czech Republic, August 9\u201315, 1998, vol.\u00a013 of Lecture\u00a0Notes Logic, pp. 127\u2013139. A.\u00a0K.\u00a0Peters, Natick, MA (2000)","DOI":"10.1017\/9781316756140.011"},{"key":"653_CR5","unstructured":"Coquand, T.: Topology and sequent calculus. In: Conference Presentation: Topology in Computer Science: Constructivity. Asymmetry and Partiality; Digitization, Dagstuhl (2000)"},{"key":"653_CR6","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1017\/S0305004105008935","volume":"140","author":"T Coquand","year":"2006","unstructured":"Coquand, T.: Geometric Hahn\u2013Banach theorem. Math. Proc. Camb. Philos. Soc. 140, 313\u2013315 (2006)","journal-title":"Math. Proc. Camb. Philos. Soc."},{"key":"653_CR7","unstructured":"Coquand, T., Lombardi, H.: Hidden constructions in abstract algebra. In: Krull Dimension, Going Up, Going Down. Technical report. G\u00f6teborg University (2001)"},{"key":"653_CR8","unstructured":"Coquand , T., Lombardi, H.: Hidden constructions in abstract algebra (3): Krull dimension of distributive lattices and commutative rings. In: Fontana, M., Kabbaj, S.-E., Wiegand, S., (eds.) Commutative Ring Theory and Applications, volume 231 of Lecture Notes in Pure and Applied Mathematics, pp. 477\u2013499. Addison-Wesley, Reading, MA (2002)"},{"key":"653_CR9","doi-asserted-by":"publisher","first-page":"885","DOI":"10.1017\/S0960129506005627","volume":"16","author":"T Coquand","year":"2006","unstructured":"Coquand, T., Lombardi, H.: A logical approach to abstract algebra. Math. Struct. Comput. Sci. 16, 885\u2013900 (2006)","journal-title":"Math. Struct. Comput. Sci."},{"key":"653_CR10","unstructured":"Coquand, T., Lombardi, H., Neuwirth, S.: Lattice-ordered groups generated by ordered groups and regular systems of ideals (2017). arXiv:1701.05115 (preprint)"},{"key":"653_CR11","first-page":"239","volume-title":"From Sets and Types to Topology and Analysis, volume 48 of Oxford Logic Guides","author":"T Coquand","year":"2005","unstructured":"Coquand, T., Lombardi, H., Roy, M.-F.: An elementary characterisation of Krull dimension. In: Crosilla, L., Schuster, P. (eds.) From Sets and Types to Topology and Analysis, volume 48 of Oxford Logic Guides, pp. 239\u2013244. Oxford University Press, Oxford (2005)"},{"key":"653_CR12","first-page":"220","volume":"48","author":"T Coquand","year":"2007","unstructured":"Coquand, T., Lombardi, H., Schuster, P.: The projective spectrum as a distributive lattice. Cah. Topol. G\u00e9om. Diff\u00e9r. Cat\u00e9g. 48, 220\u2013228 (2007)","journal-title":"Cah. Topol. G\u00e9om. Diff\u00e9r. Cat\u00e9g."},{"issue":"3","key":"653_CR13","doi-asserted-by":"publisher","first-page":"1183","DOI":"10.2307\/2586694","volume":"65","author":"T Coquand","year":"2000","unstructured":"Coquand, T., Sadocco, S., Sambin, G., Smith, J.M.: Formal topologies on the set of first-order formulae. J. Symb. Log. 65(3), 1183\u20131192 (2000)","journal-title":"J. Symb. Log."},{"key":"653_CR14","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0168-0072(03)00052-6","volume":"124","author":"T Coquand","year":"2003","unstructured":"Coquand, T., Sambin, G., Smith, J., Valentini, S.: Inductively generated formal topologies. Ann. Pure Appl. Logic 124, 71\u2013106 (2003)","journal-title":"Ann. Pure Appl. Logic"},{"key":"653_CR15","first-page":"277","volume-title":"Computer Science Logic (Fischbachau, 2000), Volume 1862 of Lecture Notes in Computer\u00a0Science","author":"T Coquand","year":"2000","unstructured":"Coquand, T., Zhang, G.: Sequents, frames, and completeness. In: Clote, P.G., Schwichtenberg, H. (eds.) Computer Science Logic (Fischbachau, 2000), Volume 1862 of Lecture Notes in Computer\u00a0Science, pp. 277\u2013291. Springer, Berlin (2000)"},{"issue":"3","key":"653_CR16","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/S0168-0072(01)00026-4","volume":"111","author":"M Coste","year":"2001","unstructured":"Coste, M., Lombardi, H., Roy, M.-F.: Dynamical method in algebra: effective Nullstellens\u00e4tze. Ann. Pure Appl. Logic 111(3), 203\u2013256 (2001)","journal-title":"Ann. Pure Appl. Logic"},{"key":"653_CR17","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1515\/9781614518471.351","volume-title":"Formalism and Beyond. On the Nature of Mathematical Discourse, Volume 23 of Logos","author":"L Crosilla","year":"2014","unstructured":"Crosilla, L., Schuster, P.: Finite methods in mathematical practice. In: Link, G. (ed.) Formalism and Beyond. On the Nature of Mathematical Discourse, Volume 23 of Logos, pp. 351\u2013410. Walter de Gruyter, Boston (2014)"},{"key":"653_CR18","first-page":"113","volume-title":"Kreiseliana. About and Around Georg Kreisel","author":"CN Delzell","year":"1996","unstructured":"Delzell, C.N.: Kreisel\u2019s unwinding of Artin\u2019s proof. In: Odifreddi, P. (ed.) Kreiseliana. About and Around Georg Kreisel, pp. 113\u2013246. A K Peters, Wellesley (1996)"},{"key":"653_CR19","volume-title":"Partially Ordered Algebraic Systems","author":"L Fuchs","year":"2011","unstructured":"Fuchs, L.: Partially Ordered Algebraic Systems. Dover Publications, Mineola (2011)"},{"key":"653_CR20","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/BF01201363","volume":"39","author":"G Gentzen","year":"1934","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen II. Math. Z. 39, 405\u2013431 (1934)","journal-title":"Math. Z."},{"key":"653_CR21","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/BF02015371","volume":"16","author":"G Gentzen","year":"1974","unstructured":"Gentzen, G.: \u00dcber das Verh\u00e4ltnis zwischen intuitionistischer und klassischer Arithmetik. Arch. Math. Logik Grundlagenforsch. 16, 119\u2013132 (1974)","journal-title":"Arch. Math. Logik Grundlagenforsch."},{"issue":"1","key":"653_CR22","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/BF01454856","volume":"101","author":"P Hertz","year":"1929","unstructured":"Hertz, P.: \u00dcber Axiomensysteme f\u00fcr beliebige Satzsysteme. Math. Ann. 101(1), 457\u2013514 (1929)","journal-title":"Math. Ann."},{"key":"653_CR23","volume-title":"Stone Spaces","author":"P Johnstone","year":"1982","unstructured":"Johnstone, P.: Stone Spaces. Cambridge University Press, Cambridge (1982)"},{"key":"653_CR24","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/S0168-0072(97)80700-2","volume":"91","author":"H Lombardi","year":"1998","unstructured":"Lombardi, H.: Relecture constructive de la th\u00e9orie d\u2019Artin\u2013Schreier. Ann. Pure Appl. Logic 91, 59\u201392 (1998)","journal-title":"Ann. Pure Appl. Logic"},{"key":"653_CR25","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1016\/j.apal.2005.05.023","volume":"137","author":"H Lombardi","year":"2006","unstructured":"Lombardi, H.: Alg\u00e8bre dynamique, espaces topologiques sans points et programme de Hilbert. Ann. Pure Appl. Logic 137, 256\u2013290 (2006)","journal-title":"Ann. Pure Appl. Logic"},{"key":"653_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-9944-7","volume-title":"Commutative Algebra: Constructive Methods: Finite Projective Modules","author":"H Lombardi","year":"2015","unstructured":"Lombardi, H., Quitt\u00e9, C.: Commutative Algebra: Constructive Methods: Finite Projective Modules. Springer, Dordrecht (2015)"},{"issue":"2","key":"653_CR27","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266681","volume":"16","author":"P Lorenzen","year":"1951","unstructured":"Lorenzen, P.: Algebraische und logistische Untersuchungen \u00fcber freie Verb\u00e4nde. J. Symb. Logic 16(2), 81\u2013106 (1951)","journal-title":"J. Symb. Logic"},{"issue":"1","key":"653_CR28","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/BF01174126","volume":"58","author":"P Lorenzen","year":"1953","unstructured":"Lorenzen, P.: Die Erweiterung halbgeordneter Gruppen zu Verbandsgruppen. Math. Z. 58(1), 15\u201324 (1953)","journal-title":"Math. Z."},{"key":"653_CR29","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-94-015-9757-9_13","volume-title":"Reuniting the Antipodes\u2014Constructive and Nonstandard Views of the Continuum (Venice. 1999), Volume 306 of Synthese Library","author":"S Negri","year":"2001","unstructured":"Negri, S.: A sequent calculus for constructive ordered field. In: Schuster, P., Berger, U., Osswald, H. (eds.) Reuniting the Antipodes\u2014Constructive and Nonstandard Views of the Continuum (Venice. 1999), Volume 306 of Synthese Library, pp. 143\u2013155. Kluwer, Dordrecht (2001)"},{"issue":"4","key":"653_CR30","doi-asserted-by":"publisher","first-page":"418","DOI":"10.2307\/420956","volume":"4","author":"S Negri","year":"1998","unstructured":"Negri, S., von Plato, J.: Cut elimination in the presence of axioms. Bull. Symb. Log. 4(4), 418\u2013435 (1998)","journal-title":"Bull. Symb. Log."},{"key":"653_CR31","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural Proof Theory","author":"S Negri","year":"2001","unstructured":"Negri, S., von Plato, J.: Structural Proof Theory. Cambridge University Press, Cambridge (2001)"},{"key":"653_CR32","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139003513","volume-title":"Proof Analysis. A Contribution to Hilbert\u2019s Last Problem","author":"S Negri","year":"2011","unstructured":"Negri, S., von Plato, J.: Proof Analysis. A Contribution to Hilbert\u2019s Last Problem. Cambridge University Press, Cambridge (2011)"},{"key":"653_CR33","first-page":"269","volume-title":"Cut Elimination in Sequent Calculi with Implicit Contraction, with a Conjecture on the Origin of Gentzen\u2019s Altitude Line Construction, Ontos Mathematical Logic","author":"S Negri","year":"2016","unstructured":"Negri, S., von Plato, J.: Concepts of Proof in Mathematics, Philosophy, and Computer Science. In: Probst, D., Schuster, P. (eds.) Cut Elimination in Sequent Calculi with Implicit Contraction, with a Conjecture on the Origin of Gentzen\u2019s Altitude Line Construction, Ontos Mathematical Logic, vol. 6, pp. 269\u2013290. Walter de Gruyter, Berlin (2016)"},{"key":"653_CR34","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s11787-007-0015-x","volume":"2","author":"G Payette","year":"2007","unstructured":"Payette, G., Schotch, P.K.: On preserving. Log. Univers. 2, 295\u2013310 (2007)","journal-title":"Log. Univers."},{"issue":"5","key":"653_CR35","doi-asserted-by":"publisher","first-page":"1003","DOI":"10.1007\/s11225-013-9519-y","volume":"102","author":"G Payette","year":"2014","unstructured":"Payette, G., Schotch, P.K.: Remarks on the Scott\u2013Lindenbaum theorem. Stud-Logica 102(5), 1003\u20131020 (2014)","journal-title":"Stud-Logica"},{"key":"653_CR36","unstructured":"Persson, H.: An application of the constructive spectrum of a ring. In: Type Theory and the Integrated Logic of Programs. Chalmers University and University of G\u00f6teborg, Ph.D. thesis (1999)"},{"key":"653_CR37","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1016\/j.jalgebra.2013.02.034","volume":"383","author":"D Rinaldi","year":"2013","unstructured":"Rinaldi, D.: A constructive notion of codimension. J. Algebra 383, 178\u2013196 (2013)","journal-title":"J. Algebra"},{"key":"653_CR38","doi-asserted-by":"publisher","first-page":"55","DOI":"10.5802\/cml.18","volume":"7","author":"D Rinaldi","year":"2015","unstructured":"Rinaldi, D., Sambin, G., Schuster, P.: The basic Zariski topology. Conflu. Math. 7, 55\u201381 (2015)","journal-title":"Conflu. Math."},{"key":"653_CR39","doi-asserted-by":"publisher","first-page":"3207","DOI":"10.1016\/j.jpaa.2016.02.011","volume":"220","author":"D Rinaldi","year":"2016","unstructured":"Rinaldi, D., Schuster, P.: A universal Krull\u2013Lindenbaum theorem. J. Pure Appl. Algebra 220, 3207\u20133232 (2016)","journal-title":"J. Pure Appl. Algebra"},{"issue":"2","key":"653_CR40","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1017\/bsl.2017.13","volume":"23","author":"D Rinaldi","year":"2017","unstructured":"Rinaldi, D., Schuster, P., Wessel, D.: Eliminating disjunctions by disjunction elimination. Bull. Symb. Logic 23(2), 181\u2013200 (2017)","journal-title":"Bull. Symb. Logic"},{"issue":"1","key":"653_CR41","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1016\/j.indag.2017.09.011","volume":"29","author":"D Rinaldi","year":"2018","unstructured":"Rinaldi, D., Schuster, P., Wessel, D.: Eliminating disjunctions by disjunction elimination. Indag. Math. (N.S.) 29(1), 226\u2013259 (2018)","journal-title":". Indag. Math. (N.S.)"},{"key":"653_CR42","unstructured":"Rinaldi, D., Wessel, D.: Extension by conservation: Sikorski\u2019s theorem. Technical report, University of Verona and University of Trento (2016) (submitted)"},{"issue":"2","key":"653_CR43","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1006\/inco.2001.3073","volume":"171","author":"WC Rounds","year":"2001","unstructured":"Rounds, W.C., Zhang, G.-Q.: Clausal logic and logic programming in algebraic domains. Inf. Comput. 171(2), 183\u2013200 (2001)","journal-title":"Inf. Comput."},{"key":"653_CR44","doi-asserted-by":"crossref","unstructured":"Sambin, G.: Intuitionistic formal spaces\u2014a first communication. In: Skordev, D., (ed.) Mathematical Logic and Its Applications, Proceedings of Advanced International Summer School-Conference, Druzhba, Bulgaria, 1986, pp. 187\u2013204. Plenum, New York (1987)","DOI":"10.1007\/978-1-4613-0897-3_12"},{"issue":"1\u20133","key":"653_CR45","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1016\/S0304-3975(02)00704-1","volume":"305","author":"G Sambin","year":"2003","unstructured":"Sambin, G.: Some points in formal topology. Theor. Comput. Sci. 305(1\u20133), 347\u2013408 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"653_CR46","unstructured":"Sambin, G.: The Basic Picture. Structures for Constructive Topology. Oxford Logic Guides. Clarendon Press, Oxford (forthcoming)"},{"key":"653_CR47","doi-asserted-by":"publisher","first-page":"787","DOI":"10.2307\/2024952","volume":"68","author":"D Scott","year":"1971","unstructured":"Scott, D.: On engendering an illusion of understanding. J. Philos. 68, 787\u2013807 (1971)","journal-title":"J. Philos."},{"key":"653_CR48","doi-asserted-by":"crossref","unstructured":"Scott, D.: Completeness and axiomatizability in many-valued logic. In: Henkin, L., Addison, J., Chang, C.C., Craig, W., Scott, D., Vaught, R. (eds.) Proceedings of the Tarski Symposium (Proc. Sympos. Pure Math., Vol. XXV, Univ. California, Berkeley, Calif., 1971), pp. 411\u2013435. Amer. Math. Soc., Providence, RI (1974)","DOI":"10.1090\/pspum\/025\/0363802"},{"key":"653_CR49","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511565687","volume-title":"Multiple-Conclusion Logic","author":"DJ Shoesmith","year":"1978","unstructured":"Shoesmith, D.J., Smiley, T.J.: Multiple-Conclusion Logic. Cambridge University Press, Cambridge (1978)"},{"key":"653_CR50","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BF01696782","volume":"37","author":"A Tarski","year":"1930","unstructured":"Tarski, A.: Fundamentale Begriffe der Methodologie der deduktiven Wissenschaften. I. Monatsh. Math. Phys. 37, 361\u2013404 (1930)","journal-title":"I. Monatsh. Math. Phys."},{"key":"653_CR51","unstructured":"Wessel, D.: Ordering groups constructively. Commun.\u00a0Algebra (forthcoming)"},{"key":"653_CR52","unstructured":"Zhang, G.-Q., Rounds, W.C.: An information-system representation of the Smyth powerdomain. In: International Symposium on Domain Theory, Shanghai (1999)"}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-018-0653-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00153-018-0653-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-018-0653-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,7]],"date-time":"2022-09-07T15:23:22Z","timestamp":1662564202000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00153-018-0653-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,4]]},"references-count":52,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2019,8]]}},"alternative-id":["653"],"URL":"https:\/\/doi.org\/10.1007\/s00153-018-0653-0","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"value":"0933-5846","type":"print"},{"value":"1432-0665","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,12,4]]},"assertion":[{"value":"19 December 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 November 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 December 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}