{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:19Z","timestamp":1749125179625},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540612087"},{"type":"electronic","value":"9783540683681"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61208-4_20","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:19:12Z","timestamp":1330273152000},"page":"312-329","source":"Crossref","is-referenced-by-count":17,"title":["Proof-search in intuitionistic logic based on constraint satisfaction"],"prefix":"10.1007","author":[{"given":"Andrei","family":"Voronkov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"20_CR1","first-page":"29","volume":"5","author":"F.V. Anufriev","year":"1972","unstructured":"F.V. Anufriev and Z.M. Aselderov. The algorithm of evidence (in Russian). Kibernetika, (5):29\u201360, 1972.","journal-title":"Kibernetika"},{"issue":"3","key":"20_CR2","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/BF01069968","volume":"22","author":"A. Degtyarev","year":"1986","unstructured":"A. Degtyarev and A. Voronkov. Equality control methods in machine theorem proving. Cybernetics, 22(3):298\u2013307, 1986.","journal-title":"Cybernetics"},{"key":"20_CR3","first-page":"105","volume":"5","author":"A.I. Degtyarev","year":"1978","unstructured":"A.I. Degtyarev, A.P. Zhezherun, and A.V. Lyaletski. Deductive tools of a mathematical text processing system (in Russian). Kibernetika, (5):105\u2013108, 1978.","journal-title":"Kibernetika"},{"key":"20_CR4","unstructured":"A. Degtyarev and A. Voronkov. Skolemization and decidability problems for fragments of intuitionistic logic. To appear in LICS'96, 10 pages, 1996."},{"key":"20_CR5","doi-asserted-by":"crossref","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R. Dyckhoff","year":"1992","unstructured":"R. Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 57:795\u2013807, 1992.","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"20_CR6","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1093\/logcom\/5.2.133","volume":"5","author":"M. Gabbrielli","year":"1995","unstructured":"M. Gabbrielli, G.M. Dore, and G. Levi. Observable semantics for constraint logic programs. Journal of Logic and Computation, 5(2):133\u2013171, 1995.","journal-title":"Journal of Logic and Computation"},{"key":"20_CR7","volume-title":"Computers and Intractability","author":"M.R. Garey","year":"1979","unstructured":"M.R. Garey and D.S. Johnson. Computers and Intractability. Freeman, San Francisco, 1979."},{"issue":"1","key":"20_CR8","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1093\/logcom\/3.1.63","volume":"3","author":"J. Hudelmaier","year":"1993","unstructured":"J. Hudelmaier. An O(n log n)-space decision procedure for intuitionistic propositional logic. Journal of Logic and Computation, 3(1):63\u201375, 1993.","journal-title":"Journal of Logic and Computation"},{"key":"20_CR9","volume-title":"volume 1 of Studies in Philosophy","author":"S. Kanger","year":"1957","unstructured":"S. Kanger. Provability in Logic, volume 1 of Studies in Philosophy. Almqvist and Wicksell, Stockholm, 1957."},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"S. Kanger. A simplified proof method for elementary logic. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning. Classical Papers on Computational Logic, volume 1, pages 364\u2013371. Springer Verlag, 1983. Originally appeared in 1963.","DOI":"10.1007\/978-3-642-81952-0_23"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"H. Kirchner. On the use of constraints in automated deduction. In A. Podelski, editor, Constraint Programming: Basics and Tools, volume 910 of Lecture Notes in Computer Science, pages 128\u2013146. Springer Verlag, 1995.","DOI":"10.1007\/3-540-59155-9_8"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"P. Lincoln, A. Scedrov, and N. Shankar. Linearizing intuitionistic implication. In Proc. IEEE Conference on Logic in Computer Science (LICS), pages 51\u201362, 1991.","DOI":"10.1109\/LICS.1991.151630"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"M.J. Maher. A CLP view of logic programming. In Proc. Conf. on Algebraic and Logic Programming, volume 632 of Lecture Notes in Computer Science, pages 364\u2013383, October 1992.","DOI":"10.1007\/BFb0013838"},{"issue":"2","key":"20_CR14","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"A. Martelli and U. Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258\u2013282, 1982.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"20_CR15","first-page":"36","volume-title":"Zapiski Nauchnyh Seminarov LOMI, 4, 1967","author":"S. Maslov","year":"1969","unstructured":"S.Yu. Maslov. An invertible sequential variant of constructive predicate calculus (in Russian). Zapiski Nauchnyh Seminarov LOMI, 4, 1967. English Translation in: Seminars in Mathematics: Steklov Math. Inst. 4, Consultants Bureau, NY-London, 1969, p.36\u201342."},{"key":"20_CR16","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/BF00881949","volume":"13","author":"P. Miglioli","year":"1994","unstructured":"P. Miglioli, U. Moscato, and M. Ornaghi. An improved refutation system for intuitionistic predicate logic. Journal of Automated Reasoning, 13:361\u2013373, 1994.","journal-title":"Journal of Automated Reasoning"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis and A. Rubio. AC-superposition with constraints: no AC-unifiers needed. In A. Bundy, editor, Automated Deduction \u2014 CADE-12. 12th International Conference on Automated Deduction., volume 814 of Lecture Notes in Artificial Intelligence, pages 545\u2013559, Nancy, France, June\/July 1994.","DOI":"10.1007\/3-540-58156-1_40"},{"key":"20_CR18","series-title":"number 918 in Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/3-540-59338-1_32","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"J. Otten","year":"1995","unstructured":"J. Otten and C. Kreitz. A connection based proof method for intuitionistic logic. In P. Baumgartner, R. H\u00e4hnle, and J. Posegga, editors, Theorem Proving with Analytic Tableaux and Related Methods, number 918 in Lecture Notes in Computer Science, pages 122\u2013137, Schlo\u00df Rheinfels, St. Goar, Germany, May 1995."},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"D. Prawitz. An improved proof procedure. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning. Classical Papers on Computational Logic, volume 1, pages 162\u2013201. Springer Verlag, 1983. Originally appeared in 1960.","DOI":"10.1007\/978-3-642-81952-0_12"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"D. Prawitz. A proof procedure with matrix reduction. In M. Laudet, L. Lacombe, L. Nolin, and M Schutzenberger, editors, Symp. on Automatic Demonstration, volume 125 of Lecture Notes in Mathematics, pages 207\u2013213. Springer Verlag, 1970.","DOI":"10.1007\/BFb0060634"},{"key":"20_CR21","first-page":"522","volume-title":"volume 607 of Lecture Notes in Artificial Intelligence","author":"N. Shankar","year":"1992","unstructured":"N. Shankar. Proof search in the intuitionistic sequent calculus. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 522\u2013536, Saratoga Springs, NY, USA, June 1992. Springer Verlag."},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"R. Statman. Intuitionistic logic is polynomial-space complete. Theoretical Computer Science, 9, 1979.","DOI":"10.1016\/0304-3975(79)90006-9"},{"key":"20_CR23","unstructured":"T. Tammet. A resolution theorem prover for intuitionistic logic. Submitted."},{"key":"20_CR24","first-page":"689","volume":"58","author":"N.N. Vorob'ev","year":"1952","unstructured":"N.N. Vorob'ev. The derivability problem in the constructive propositional calculus with strong negation. Dokl. Akad. Nauk SSSR (in Russian), 58:689\u2013692, 1952.","journal-title":"Dokl. Akad. Nauk SSSR (in Russian)"},{"key":"20_CR25","unstructured":"N.N. Vorob'ev. A new derivability algorithm in the constructive propositional calculus. In Trudy Math. Inst. Steklov, volume 52. Moscow, 1958."},{"key":"20_CR26","first-page":"648","volume-title":"volume 607 of Lecture Notes in Artificial Intelligence","author":"A. Voronkov","year":"1992","unstructured":"A. Voronkov. Theorem proving in non-standard logics based on the inverse method. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 648\u2013662, Saratoga Springs, NY, USA, June 1992. Springer Verlag."},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"A. Voronkov. On proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-Unification. UPMAIL Technical Report 121, Uppsala University, Computing Science Department, January 1996.","DOI":"10.1007\/3-540-61511-3_67"},{"key":"20_CR28","doi-asserted-by":"crossref","unstructured":"A. Voronkov. Proof-search in intuitionistic logic based on the constraint satisfaction. UPMAIL Technical Report 120, Uppsala University, Computing Science Department, January 1996.","DOI":"10.1007\/3-540-61208-4_20"},{"key":"20_CR29","unstructured":"L.A. Wallen. Automated Deduction in Nonclassical Logics. MIT Press, 1990."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61208-4_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T15:08:20Z","timestamp":1687273700000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61208-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540612087","9783540683681"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-61208-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}