{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:21:16Z","timestamp":1758979276720,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540577850"},{"type":"electronic","value":"9783540483328"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57785-8_131","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:21:08Z","timestamp":1330262468000},"page":"59-70","source":"Crossref","is-referenced-by-count":5,"title":["The complexity of resource-bounded first-order classical logic"],"prefix":"10.1007","author":[{"given":"Jean","family":"Goubault","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P. B. Andrews","year":"1981","unstructured":"P. B. Andrews. Theorem proving via general matings. J. ACM, 28(2):193\u2013214, 1981.","journal-title":"J. ACM"},{"key":"5_CR2","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/S0747-7171(87)80027-5","volume":"3","author":"D. Benanav","year":"1987","unstructured":"D. Benanav, D. Kapur, and P. Narendran. Complexity of matching problems. J. Symb. Computation, 3:203\u2013216, 1987.","journal-title":"J. Symb. Computation"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg, second, revised edition, 1987.","DOI":"10.1007\/978-3-322-90102-6"},{"key":"5_CR4","volume-title":"Technical Report 494","author":"A. Boudet","year":"1989","unstructured":"A. Boudet. A new combination technique for AC-unification. Technical Report 494, LRI, Orsay, France, Juin 1989."},{"key":"5_CR5","unstructured":"C.-L. Chang and R. C.-T. Lee. Symbolic Logic and Mechanical Theorem Proving. Computer Science Classics. Academic Press, 1973."},{"key":"5_CR6","doi-asserted-by":"crossref","first-page":"40","DOI":"10.2307\/2269326","volume":"1","author":"A. Church","year":"1936","unstructured":"A. Church. A note on the Entscheidungsproblem. J. Symb. Logic, 1:40\u201341, 1936.","journal-title":"J. Symb. Logic"},{"key":"5_CR7","doi-asserted-by":"crossref","first-page":"101","DOI":"10.2307\/2269030","volume":"1","author":"A. Church","year":"1936","unstructured":"A. Church. A note on the Entscheidungsproblem (correction). J. Symb. Logic, 1:101\u2013102, 1936.","journal-title":"J. Symb. Logic"},{"key":"5_CR8","first-page":"151","volume-title":"3rd STOC","author":"S. A. Cook","year":"1971","unstructured":"S. A. Cook. The complexity of theorem-proving procedures. In 3rd STOC, pages 151\u2013158, New York, 1971. ACM."},{"key":"5_CR9","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"3","author":"W. F. Dowling","year":"1984","unstructured":"W. F. Dowling and J. H. Gallier. Linear time algorithms for testing the satisfiability of propositional Horn formulae. J. Logic Programming, 3:267\u2013284, 1984.","journal-title":"J. Logic Programming"},{"key":"5_CR10","volume-title":"The Decision Problem \u2014 Solvable Classes of Quantificational Formulas","author":"B. Dreben","year":"1979","unstructured":"B. Dreben and W. D. Goldfarb. The Decision Problem \u2014 Solvable Classes of Quantificational Formulas. Addison-Wesley, Reading, Massachussetts, 1979."},{"key":"5_CR11","volume-title":"Artificial Intelligence","author":"E. Eder","year":"1992","unstructured":"E. Eder. Relative Complexities of First-Order Calculi. Artificial Intelligence. Vieweg Verlag, Wiesbaden, Germany, 1992."},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"M. C. Fitting. First-Order Logic and Automated Theorem Proving. Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"5_CR13","volume-title":"Computers and Intractability \u2014 A Guide to the Theory of NP-Completeness","author":"M. R. Garey","year":"1979","unstructured":"M. R. Garey and D. S. Johnson. Computers and Intractability \u2014 A Guide to the Theory of NP-Completeness. W.H. Freeman and Co., San Francisco, 1979."},{"key":"5_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"J.-Y. Girard. Linear logic. TCS, 50:1\u2013102, 1987.","journal-title":"TCS"},{"key":"5_CR15","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W. D. Goldfarb","year":"1981","unstructured":"W. D. Goldfarb. The undecidability of the second-order unification problem. TCS, 13:225\u2013230, 1981.","journal-title":"TCS"},{"key":"5_CR16","volume-title":"PhD thesis","author":"J. Goubault","year":"1993","unstructured":"J. Goubault. D\u00e9monstration automatique en logique classique: complexit\u00e9 et m\u00e9thodes. PhD thesis, \u00e9cole Polytechnique, Palaiseau, France, September 1993."},{"key":"5_CR17","unstructured":"J. Goubault. Syntax independent connections. In Workshop on Theorem Proving with Analytic Tableaux and Related Methods, number MPI-I-93-213 in Max-Planck-Iinstitut f\u00fcr Informatik, pages 101-111, Marseille, France, avril 1993."},{"key":"5_CR18","first-page":"140","volume":"42","author":"Y. Gurevich","year":"1990","unstructured":"Y. Gurevich. On the classical decision problem. Bulletin of the EATCS, 42:140\u2013150, October 1990.","journal-title":"Bulletin of the EATCS"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"D. Kapur and P. Narendran. Matching, unification and complexity. SIGSAM Bulletin, October 1987.","DOI":"10.1145\/36330.36332"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"D. Kapur and P. Narendran. Double-exponential complexity of computing a complete set of AC-unifiers. In 7th LICS, pages 11\u201321, 1992.","DOI":"10.1109\/LICS.1992.185515"},{"issue":"4","key":"5_CR21","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1147\/rd.254.0327","volume":"25","author":"D. Kozen","year":"1981","unstructured":"D. Kozen. Positive first-order logic is NP-complete. IBM J. Res. and Development, 25(4):327\u2013332, 1981.","journal-title":"IBM J. Res. and Development"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"H. R. Lewis. Complexity of solvable cases of the decision problem for the predicate calculus. In 19th FOCS, pages 35\u201347, 1978.","DOI":"10.1109\/SFCS.1978.9"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar. Decision problems for propositional linear logic. In 32nd FOCS, pages 662\u2013671, 1990.","DOI":"10.1109\/FSCS.1990.89588"},{"key":"5_CR24","unstructured":"P. Lincoln and A. Scedrov. First order linear logic without modalities is nexptimehard. Available through anonymous ftp from ftp.csl.sri.com, 1992."},{"key":"5_CR25","unstructured":"P. Lincoln and T. Winkler. Constant-only multiplicative linear logic is NP-complete. Available through anonymous ftp from ftp.csl.sri.com, file\/pub\/lincoln\/comultnpc.dvi, 1992."},{"key":"5_CR26","unstructured":"M. Minoux. LTUR: A simplified linear-time unit resolution algorithm for Horn formul\u00c6 and computer implementation. Technical Report 206, Laboratoire MASI, CNRS UA 818, Universit\u00e9 Pierre et Marie Curie, janvier 1988."},{"key":"5_CR27","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1090\/S0002-9947-1973-0432416-X","volume":"177","author":"R. Parikh","year":"1973","unstructured":"R. Parikh. Some results on the lengths of proofs. Trans. AMS, 177:29\u201336, 1973.","journal-title":"Trans. AMS"},{"key":"5_CR28","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M. Paterson","year":"1978","unstructured":"M. Paterson and M. Wegman. Linear unification. J. Comp. Sys. Sciences, 16:158\u2013167, 1978.","journal-title":"J. Comp. Sys. Sciences"},{"key":"5_CR29","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"G. Plotkin. Building in equational theories. Machine Intelligence, 7:73\u201390, 1972.","journal-title":"Machine Intelligence"},{"key":"5_CR30","volume-title":"PhD thesis","author":"J. Posegga","year":"1993","unstructured":"J. Posegga. Deduction with Shannon Graphs or: How to Lift BDDs to First-order Logic. PhD thesis, Institut f\u00fcr Logik, Komplexit\u00e4t und Deduktionssysteme, Uni. Karlsruhe, FRG, 1993."},{"key":"5_CR31","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","volume":"26","author":"D. Prawitz","year":"1960","unstructured":"D. Prawitz. An improved proof procedure. Theoria, 26:102\u2013139, 1960.","journal-title":"Theoria"},{"key":"5_CR32","first-page":"59","volume":"4","author":"D. Prawitz","year":"1969","unstructured":"D. Prawitz. Advances and problems in mechanical proof procedures. Machine Intelligence, 4:59\u201371, 1969.","journal-title":"Machine Intelligence"},{"key":"5_CR33","first-page":"1","volume-title":"5th STOC","author":"L. J. Stockmeyer","year":"1973","unstructured":"L. J. Stockmeyer and A. R. Meyer. Word problems requiring exponential time. In 5th STOC, pages 1\u20139, New York, NY, USA, 1973. ACM."},{"key":"5_CR34","first-page":"466","volume":"8","author":"G. Tseitin","year":"1970","unstructured":"G. Tseitin. On the complexity of proofs in propositional logics. Seminars in Mathematics, 8:466\u2013483, 1970.","journal-title":"Seminars in Mathematics"},{"key":"5_CR35","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/0304-3975(76)90062-1","volume":"3","author":"C. Wrathall","year":"1976","unstructured":"C. Wrathall. Complete sets and the polynomial-time hierarchy. TCS, 3:23\u201333, 1976.","journal-title":"TCS"}],"container-title":["Lecture Notes in Computer Science","STACS 94"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57785-8_131.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:14:02Z","timestamp":1742595242000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57785-8_131"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540577850","9783540483328"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-57785-8_131","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}