{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:35Z","timestamp":1749124055518},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1995,3,1]],"date-time":"1995-03-01T00:00:00Z","timestamp":794016000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[1995,3]]},"DOI":"10.1007\/bf01535839","type":"journal-article","created":{"date-parts":[[2005,4,19]],"date-time":"2005-04-19T06:36:20Z","timestamp":1113892580000},"page":"1-18","source":"Crossref","is-referenced-by-count":1,"title":["Structured proof procedures"],"prefix":"10.1007","volume":"15","author":[{"given":"Enrico","family":"Giunchiglia","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Armando","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paolo","family":"Pecchiari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","first-page":"475","volume":"8","author":"A. Armando","year":"1993","unstructured":"A. Armando and E. Giunchiglia, Embedding complex decision procedures inside an interactive theorem prover, Ann. Math. and AI 8(1993)475?502.","journal-title":"Ann. Math. and AI"},{"key":"CR2","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1145\/77600.77617","volume":"37","author":"M. Abadi","year":"1990","unstructured":"M. Abadi and Z. Manna, Nonclausal deduction in first-order temporal logic, J. ACM 37(1990)279?317.","journal-title":"J. ACM"},{"key":"CR3","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(1981)193?214.","journal-title":"J. ACM"},{"key":"CR4","unstructured":"M. Buro and H.K. B\u00fcning, Report on a SAT competition, Technical Report No. 110, FB-17, Mathematik\/Informatik Universit\u00e4t Paderborn (1992)."},{"key":"CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-90100-2","volume-title":"Automated Theorem Proving","author":"W. Bibel","year":"1982","unstructured":"W. Bibel,Automated Theorem Proving (Vieweg, Braunschweig, 1982)."},{"key":"CR6","first-page":"83","volume":"11","author":"R.S. Boyer","year":"1988","unstructured":"R.S. Boyer and J.S. More, Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic, Machine Intelligence 11(1988)83?124.","journal-title":"Machine Intelligence"},{"key":"CR7","unstructured":"B. Dreben and W.D. Goldfarb,The Decision Problem ? Solvable Classes of Quantificational Formulas (Addison-Wesley, 1979)."},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"M. Davis, G. Longemann and D. Loveland, A machine program for theorem proving, J. ACM 5(7) (1962).","DOI":"10.1145\/368273.368557"},{"key":"CR9","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam, A computing procedure for quantification theory, J. ACM 7(1960)201?215.","journal-title":"J. ACM"},{"key":"CR10","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1147\/rd.41.0028","volume":"4","author":"P.C. Gilmore","year":"1960","unstructured":"P.C. Gilmore, A proof method for quantification theory: Its justification and realization, IBM J. Res. Develop. 4(1960)28?35.","journal-title":"IBM J. Res. Develop."},{"key":"CR11","volume-title":"The GETFOL Manual ? GETFOL Version 1, Technical Report 9204-01","author":"F. Giunchiglia","year":"1992","unstructured":"F. Giunchiglia, The GETFOL Manual ? GETFOL Version 1, Technical Report 9204-01, DIST, University of Genova, Genoa, Italy (1992). Forthcoming IRST Technical Report."},{"key":"CR12","unstructured":"F. Harche, J.N. Hooker and G.L. Thompson, A computational study of satisfiability algorithms for propositional logic, Working Paper 1991-27 (1991)."},{"key":"CR13","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0167-9236(88)90128-5","volume":"4","author":"R.G. Jeroslow","year":"1988","unstructured":"R.G. Jeroslow, Computation-oriented reduction of predicate to propositional logic, Decision Support Syst. 4(1988)183?197.","journal-title":"Decision Support Syst."},{"key":"CR14","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"W.H. Joyner","year":"1976","unstructured":"W.H. Joyner, Resolution strategies as decision procedures, J. ACM 23(1976)398?417.","journal-title":"J. ACM"},{"key":"CR15","unstructured":"S.J. Lee and D.A. Plaisted, Eliminating duplication with the hyper-linking strategy, Technical Report TR90-032, Department of Computer Science, University of North Carolina (1990)."},{"key":"CR16","doi-asserted-by":"crossref","unstructured":"N.V. Murray and E. Rosenthal, Dissolution: Making paths vanish, J. ACM, to appear.","DOI":"10.1145\/174130.174135"},{"key":"CR17","unstructured":"G. Nelson and D.C. Oppen, Simplification by cooperating decision procedures, Technical Report STAN-CS-78-652, Stanford Computer Science Department (1978)."},{"key":"CR18","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F.J. Pelletier","year":"1986","unstructured":"F.J. Pelletier, Seventy-five problems for testing automatic theorem provers, J. Autom. Reasoning 2(1986)191?216. See also Errata Corrige in J. Autom. Reasoning 4(1988)235?236.","journal-title":"J. Autom. Reasoning"},{"key":"CR19","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(1960)102?139.","journal-title":"Theoria"},{"key":"CR20","volume-title":"Natural Deduction ? A Proof Theoretical Study","author":"D. Prawitz","year":"1965","unstructured":"D. Prawitz,Natural Deduction ? A Proof Theoretical Study (Almquist-Wiksell, Stockholm, 1965)."},{"key":"CR21","volume-title":"Logic and Data Bases","author":"R. Reiter","year":"1978","unstructured":"R. Reiter, Deductive questions-answering on relational databases, in:Logic and Data Bases, eds. H. Gallaire and J. Minker (Plenum Press, New York, 1978)."},{"key":"CR22","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"A. Robinson","year":"1965","unstructured":"A. Robinson, A machine oriented logic based on the resolution principle, J. ACM 12(1965)23?41.","journal-title":"J. ACM"},{"key":"CR23","first-page":"333","volume":"4","author":"M. Stickel","year":"1985","unstructured":"M. Stickel, Automated deduction by theory resolution, J. Autom. Reasoning 4(1985)333?356.","journal-title":"J. Autom. Reasoning"},{"key":"CR24","doi-asserted-by":"crossref","unstructured":"G. Winskel,The Formal Semantics of Programming Languages (MIT Press, 1993).","DOI":"10.7551\/mitpress\/3054.001.0001"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01535839\/fulltext.html","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01535839.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01535839\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01535839","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,7]],"date-time":"2020-04-07T00:08:19Z","timestamp":1586218099000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01535839"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,3]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1995,3]]}},"alternative-id":["BF01535839"],"URL":"https:\/\/doi.org\/10.1007\/bf01535839","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,3]]}}}