{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:26:37Z","timestamp":1725549997529},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540289319"},{"type":"electronic","value":"9783540318224"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11554554_9","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T14:02:57Z","timestamp":1127829777000},"page":"93-107","source":"Crossref","is-referenced-by-count":4,"title":["A Tableau-Based Decision Procedure for a Fragment of Graph Theory Involving Reachability and Acyclicity"],"prefix":"10.1007","author":[{"given":"Domenico","family":"Cantone","sequence":"first","affiliation":[]},{"given":"Calogero G.","family":"Zarba","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Baader, F.: Augmenting concept languages by transitive closure of roles: An alternative to terminological cycles. In: Mylopoulos, J., Reiter, R. (eds.) International Joint Conference on Artificial Intelligence, pp. 446\u2013451 (1991)"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-49099-X_2","volume-title":"European Symposium on Programming","author":"M. Benedikt","year":"1999","unstructured":"Benedikt, M., Reps, T.W., Sagiv, S.: A decidable logic for describing linked data structures. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol.\u00a01576, pp. 2\u201319. Springer, Heidelberg (1999)"},{"key":"9_CR3","first-page":"23","volume":"7","author":"R.M. Burstall","year":"1972","unstructured":"Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. Machine Intelligence\u00a07, 23\u201350 (1972)","journal-title":"Machine Intelligence"},{"key":"9_CR4","unstructured":"Cantone, D., Cincotti, G.: The decision problem in graph theory with reachability related constructs. In: Baumgartner, P., Zhang, H., (eds.), First-Order Theorem Proving, Technical Report 5\/2000, pp. 68\u201390. Universit\u00e4t Koblenz-Landau (2000)"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Cantone, D., Cutello, V.: A decidable fragment of the elementary theory of relations and some applications. In: International Symposium on Symbolic and Algebraic Computation, pp. 24\u201329 (1990)","DOI":"10.1145\/96877.96887"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Cantone, D., Zarba, C.G.: A tableau-based decision procedure for a fragment of graph theory involving reachability and acyclicity. Technical report, Department of Computer Science, University of New Mexico (2005)","DOI":"10.1007\/11554554_9"},{"key":"9_CR7","volume-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving","author":"J.H. Gallier","year":"1986","unstructured":"Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row, New York (1986)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-540-27864-1_26","volume-title":"Static Analysis","author":"V. Kuncak","year":"2004","unstructured":"Kuncak, V., Rinard, M.: Generalized records and spatial conjunction in role logic. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 361\u2013376. Springer, Heidelberg (2004)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/BFb0012842","volume-title":"9th International Conference on Automated Deduction","author":"L.E. Moser","year":"1988","unstructured":"Moser, L.E.: A decision procedure for unquantified formulas of graph theory. In: Lusk, E.R., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 344\u2013357. Springer, Heidelberg (1988)"},{"key":"9_CR10","unstructured":"Ranise, S., Zarba, C.G.: A decidable logic for pointer programs manipulating linked lists. Unpublished (2005)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-540-24725-8_28","volume-title":"Programming Languages and Systems","author":"A. Rensink","year":"2004","unstructured":"Rensink, A.: Canonical graph shapes. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 401\u2013415. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11554554_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:46:47Z","timestamp":1605642407000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11554554_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540289319","9783540318224"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/11554554_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}