{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:24Z","timestamp":1749125184123},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540593386"},{"type":"electronic","value":"9783540492351"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59338-1_44","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:14:13Z","timestamp":1330276453000},"page":"310-323","source":"Crossref","is-referenced-by-count":10,"title":["Propositional logics on the computer"],"prefix":"10.1007","author":[{"given":"Alain","family":"Heuerding","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerhard","family":"J\u00e4ger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Schwendimann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Seyfried","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"issue":"3","key":"21_CR1","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J. Andreoli","year":"1992","unstructured":"Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297\u2013347, 1992.","journal-title":"Journal of Logic and Computation"},{"key":"21_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00258073","volume":"9","author":"G. Boolos","year":"1980","unstructured":"George Boolos. Provability, truth, and modal logic. Journal of Philosophical Logic, 9:1\u20137, 1980.","journal-title":"Journal of Philosophical Logic"},{"issue":"3","key":"21_CR3","doi-asserted-by":"crossref","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R. Dyckhoff","year":"1992","unstructured":"Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. The Journal of Symbolic Logic, 57(3):795\u2013807, 1992.","journal-title":"The Journal of Symbolic Logic"},{"key":"21_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intuitionistic Logics","author":"M. Fitting","year":"1983","unstructured":"Melvin Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, Dordrecht, 1983."},{"key":"21_CR5","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BF00244394","volume":"4","author":"M. Fitting","year":"1988","unstructured":"Melvin Fitting. First-order modal tableaux. Journal of Automated Reasoning, 4:191\u2013213, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"21_CR6","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","volume":"54","author":"J. Y. Halpern","year":"1992","unstructured":"Joseph Y. Halpern and Yoram Moses. A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence, 54:319\u2013379, 1992.","journal-title":"Artificial Intelligence"},{"key":"21_CR7","unstructured":"Roger J. Hindley and Jonathan R. Seldin. Introduction to Combinators and Lambda Calculus. Cambridge University Press, 1986."},{"issue":"1","key":"21_CR8","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1093\/logcom\/3.1.63","volume":"3","author":"J. Hudelmaier","year":"1993","unstructured":"J\u00f6rg Hudelmaier. An O(nlog 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"},{"issue":"3","key":"21_CR9","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R. E. Ladner","year":"1977","unstructured":"Richard E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM journal on computing, 6(3):467\u2013480, 1977.","journal-title":"SIAM journal on computing"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Nicholas Rescher and Alasdair Urquhart. Temporal Logic. Springer, 1971.","DOI":"10.1007\/978-3-7091-7664-1"},{"issue":"5","key":"21_CR11","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1093\/logcom\/2.5.619","volume":"2","author":"D. Sahlin","year":"1992","unstructured":"Dan Sahlin, Torkel Franz\u00e9n, and Seif Haridi. An intuitionistic predicate logic theorem prover. Journal of Logic and Computation, 2(5):619\u2013656, 1992.","journal-title":"Journal of Logic and Computation"},{"key":"21_CR12","unstructured":"Michael Seyfried. A sequent calculus for proof search in the (\u2192, \u2227)-fragment of intuitionistic logic. Technical notes, 1994."},{"key":"21_CR13","volume-title":"Programming Methodology Group report 70","author":"T. Tammet","year":"1993","unstructured":"Tanel Tammet. Proof search strategies in linear logic. Programming Methodology Group report 70, Department of Computer Sciences, Chalmers University of Technology, G\u00f6teborg, Sweden, 1993."},{"key":"21_CR14","volume-title":"Diploma thesis","author":"H. Zimmermann","year":"1994","unstructured":"Heinrich Zimmermann. A directed tree calculus for minimal tense logic. Diploma thesis, IAM, University of Bern, Switzerland, 1994."}],"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-59338-1_44.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:27:11Z","timestamp":1619573231000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59338-1_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540593386","9783540492351"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-59338-1_44","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}