{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:24:09Z","timestamp":1725470649027},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540379010"},{"type":"electronic","value":"9783540379027"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11829263_7","type":"book-chapter","created":{"date-parts":[[2006,9,19]],"date-time":"2006-09-19T03:32:51Z","timestamp":1158636771000},"page":"117-139","source":"Crossref","is-referenced-by-count":14,"title":["A Computerized Referee"],"prefix":"10.1007","author":[{"given":"Eugenio G.","family":"Omodeo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Domenico","family":"Cantone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Policriti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacob T.","family":"Schwartz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Aiello, L., Weyhrauch, R.W.: Using meta-theoretic reasoning to do algebra. In: [2] pp.\u00a01\u201313","DOI":"10.1007\/3-540-10009-1_1"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 5th conference on Automated Deduction","year":"1980","unstructured":"Bibel, W., Kowalski, R. (eds.): Proceedings of the 5th conference on Automated Deduction. LNCS, vol.\u00a087. Springer, Heidelberg (1980)"},{"key":"7_CR3","series-title":"Graduate Texts in Mathematics","volume-title":"Foundations of Real and Abstract Analysis","author":"D.S. Bridges","year":"1997","unstructured":"Bridges, D.S.: Foundations of Real and Abstract Analysis. Graduate Texts in Mathematics, vol.\u00a0174. Springer, Heidelberg (1997)"},{"key":"7_CR4","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/BFb0027409","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"D. Cantone","year":"1997","unstructured":"Cantone, D.: A fast saturation strategy for set-theoretic tableaux. In: Galmiche, D. (ed.) TABLEAUX 1997. LNCS (LNAI), vol.\u00a01227, pp. 122\u2013137. Springer, Heidelberg (1997)"},{"key":"7_CR5","series-title":"LNAI","first-page":"126","volume-title":"Proc. of the International Workshop on First-Order Theorem Proving (FTP 1998)","author":"D. Cantone","year":"2000","unstructured":"Cantone, D., Zarba, C.G.: A new fast tableau-based decision procedure for an unquantified fragment of set theory. In: Caferra, R., Salzer, G. (eds.) Proc. of the International Workshop on First-Order Theorem Proving (FTP 1998). LNCS (LNAI), vol.\u00a01761, pp. 126\u2013136. Springer, Heidelberg (2000)"},{"issue":"2","key":"7_CR6","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF00245817","volume":"6","author":"D. Cantone","year":"1990","unstructured":"Cantone, D., Omodeo, E.G., Policriti, A.: The automation of syllogistic II. Optimization and complexity issues. J. Automated Reasoning\u00a06(2), 173\u2013187 (1990)","journal-title":"J. Automated Reasoning"},{"key":"7_CR7","series-title":"Monographs in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3452-2","volume-title":"Set Theory for Computing. From Decision Procedures to Declarative Programming with Sets","author":"D. Cantone","year":"2001","unstructured":"Cantone, D., Omodeo, E.G., Policriti, A.: Set Theory for Computing. From Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science. Springer, New York (2001)"},{"key":"7_CR8","unstructured":"Cantone, D., Formisano, A., Omodeo, E.G., Schwartz, J.T.: Various commonly occurring decidable extensions of multi-level syllogistic. In: Ranise, S., Tinelli, C. (eds.) Pragmatics of Decision Procedures in Automated Reasoning 2003, PDPAR 2003 (CADE 19), Miami, USA (July 29, 2003)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-540-39910-0_8","volume-title":"Verification: Theory and Practice","author":"D. Cantone","year":"2004","unstructured":"Cantone, D., Omodeo, E.G., Schwartz, J.T., Ursino, P.: Notes from the logbook of a proof-checker\u2019s project. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 182\u2013207. Springer, Heidelberg (2004)"},{"issue":"1-3","key":"7_CR10","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/S0304-3975(03)00361-X","volume":"311","author":"A. Dovier","year":"2004","unstructured":"Dovier, A., Piazza, C., Policriti, A.: An Efficient Algorithm for Computing Bisimulation Equivalence. Theoretical Computer Science\u00a0311(1-3), 221\u2013256 (2004)","journal-title":"Theoretical Computer Science"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Ferro, A., Omodeo, E.G., Schwartz, J.T.: Decision procedures for some fragments of set theory. In: [2] pp.\u00a088\u201396","DOI":"10.1007\/3-540-10009-1_8"},{"issue":"5","key":"7_CR12","doi-asserted-by":"publisher","first-page":"599","DOI":"10.1002\/cpa.3160330503","volume":"33","author":"A. Ferro","year":"1980","unstructured":"Ferro, A., Omodeo, E.G., Schwartz, J.T.: Decision procedures for elementary sublanguages of set theory I. Multi-level syllogistic and some extensions. Comm. Pure Applied Math.\u00a033(5), 599\u2013608 (1980)","journal-title":"Comm. Pure Applied Math."},{"key":"7_CR13","volume-title":"Graduate Texts in Computer Science","author":"M.C. Fitting","year":"1996","unstructured":"Fitting, M.C.: First-Order Logic and Automated Theorem Proving. In: Graduate Texts in Computer Science, 2nd edn. Springer, Berlin (1996) (1st edn., 1990)","edition":"2"},{"issue":"1","key":"7_CR14","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1023\/A:1027328830731","volume":"31","author":"R. Gentilini","year":"2003","unstructured":"Gentilini, R., Piazza, C., Policriti, A.: From Bisimulation to Simulation. Coarsest Partition Problems. Journal of Automated Reasoning\u00a031(1), 73\u2013103 (2003)","journal-title":"Journal of Automated Reasoning"},{"issue":"9-10","key":"7_CR15","doi-asserted-by":"publisher","first-page":"1053","DOI":"10.1002\/cpa.3160480906","volume":"48","author":"J.-P. Keller","year":"1995","unstructured":"Keller, J.-P., Paige, R.: Program derivation with verified transformations - A case study. Comm. Pure Appl. Math.\u00a048(9-10), 1053\u20131113 (1995); Special issue in honor of Schwartz, J.T.","journal-title":"Comm. Pure Appl. Math."},{"key":"7_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-83189-8","volume-title":"Foundation of Logic Programming","author":"J.W. Lloyd","year":"1987","unstructured":"Lloyd, J.W.: Foundation of Logic Programming, 2nd edn. Springer, Heidelberg (1987)","edition":"2"},{"key":"7_CR17","unstructured":"McCune, W.W.: Otter 2.0 User Guide. Technical Report ANL-90\/9, Argonne National Laboratory, Argonne, Illinois (1990)"},{"key":"7_CR18","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/3-540-45632-5_9","volume-title":"Computational Logic: Logic Programming and Beyond","author":"E.G. Omodeo","year":"2002","unstructured":"Omodeo, E.G., Schwartz, J.T.: A \u2018Theory\u2019 mechanism for a proof-verifier based on first-order set theory. In: Kakas, A.C., Sadri, F. (eds.) Computational Logic: Logic Programming and Beyond. LNCS (LNAI), vol.\u00a02408, pp. 214\u2013230. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Reasoning, Action and Interaction in AI Theories and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11829263_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T03:13:26Z","timestamp":1619493206000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11829263_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540379010","9783540379027"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/11829263_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}