{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,22]],"date-time":"2026-02-22T00:05:09Z","timestamp":1771718709688,"version":"3.50.1"},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"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":[[1993]]},"DOI":"10.1007\/bf00881838","type":"journal-article","created":{"date-parts":[[2004,12,25]],"date-time":"2004-12-25T19:07:06Z","timestamp":1104001626000},"page":"265-281","source":"Crossref","is-referenced-by-count":70,"title":["Gentzen-type systems, resolution and tableaux"],"prefix":"10.1007","volume":"10","author":[{"given":"Arnon","family":"Avron","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/0890-5401(91)90023-U","volume":"92","author":"A. Avron","year":"1991","unstructured":"Avron, A., ?Simple consequence relations?,Information and Computation 92, 105?139 (1991).","journal-title":"Information and Computation"},{"key":"CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-90100-2","volume-title":"Automated Theorem Proving","author":"W. Bibel","year":"1982","unstructured":"Bibel, W.,Automated Theorem Proving, Vieweg Verlag, Braunschweig (1982)."},{"key":"CR3","volume-title":"A Course in Mathematical Logic","author":"J. L. Bell","year":"1977","unstructured":"Bell, J. L. and Machover, M.,A Course in Mathematical Logic, North-Holland, Amsterdam (1977)."},{"key":"CR4","volume-title":"The Computer Modelling of Mathematical Reasoning","author":"A. Bundy","year":"1983","unstructured":"Bundy, A.,The Computer Modelling of Mathematical Reasoning, Academic Press, New York (1983)."},{"key":"CR5","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. Chang","year":"1973","unstructured":"Chang, C. and Lee, R. C.,Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York (1973)."},{"key":"CR6","volume-title":"First Order Logic and Automated Theorem Proving","author":"M. C. Fitting","year":"1989","unstructured":"Fitting, M. C.,First Order Logic and Automated Theorem Proving, Springer-Verlag, New York (1989)."},{"key":"CR7","volume-title":"Logic and Computer Science ? Foundations of Automatic Theorem Proving","author":"J. H. Gallier","year":"1986","unstructured":"Gallier, J. H.,Logic and Computer Science ? Foundations of Automatic Theorem Proving, Harper & Row, New York (1986)."},{"key":"CR8","volume-title":"The Collected Work of Gerhard Gentzen","author":"G. Gentzen","year":"1969","unstructured":"Gentzen, G., ?Investigations into logical deduction?, inThe Collected Work of Gerhard Gentzen, M.E. Szabo (Ed.), North Holland, Amsterdam (1969)."},{"key":"CR9","volume-title":"Proofs and Types","author":"J. Y. Girard","year":"1989","unstructured":"Girard, J. Y., Lafont, Y. and Taylor, P.,Proofs and Types, Cambridge University Press, Cambridge (1989)."},{"key":"CR10","unstructured":"Girard, J. Y.,Proof Theory and Logical Complexity, Bibliopolis (1987)."},{"key":"CR11","volume-title":"Logic for Problem Solving","author":"R. Kowalski","year":"1979","unstructured":"Kowalski, R.,Logic for Problem Solving, Elsevier\/North-Holland, New York (1979)."},{"key":"CR12","volume-title":"Automated Theorem Proving: A Logical Basis","author":"D. W. Loveland","year":"1978","unstructured":"Loveland, D. W.,Automated Theorem Proving: A Logical Basis, Elsevier\/North-Holland, New York (1978)."},{"key":"CR13","first-page":"364","volume-title":"Proceedings of CADE 8","author":"F. Oppacher","year":"1986","unstructured":"Oppacher, F. and Suen, E., ?Controlling deduction with proof condensation and heuristics?, inProceedings of CADE 8, pp. 364?393, Springer-Verlag, Berlin (1986)."},{"key":"CR14","volume-title":"Logic: Form and Function","author":"J. A. Robinson","year":"1979","unstructured":"Robinson, J. A.,Logic: Form and Function, Elsevier\/North-Holland, New York (1979)."},{"key":"CR15","volume-title":"First-Order Logic","author":"R. M. Smullyan","year":"1986","unstructured":"Smullyan, R. M.,First-Order Logic, Springer-Verlag, Berlin (1986)."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881838.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881838\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881838","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T12:58:10Z","timestamp":1556542690000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881838"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"references-count":15,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1993]]}},"alternative-id":["BF00881838"],"URL":"https:\/\/doi.org\/10.1007\/bf00881838","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}