{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,24]],"date-time":"2025-02-24T05:11:33Z","timestamp":1740373893583,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540280057"},{"type":"electronic","value":"9783540318644"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11532231_17","type":"book-chapter","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T18:56:52Z","timestamp":1279738612000},"page":"235-249","source":"Crossref","is-referenced-by-count":2,"title":["Proof Planning for First-Order Temporal Logic"],"prefix":"10.1007","author":[{"given":"Claudio","family":"Castellini","sequence":"first","affiliation":[]},{"given":"Alan","family":"Smaill","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"17_CR1","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/77600.77617","volume":"37","author":"M. Abad\u00ed","year":"1990","unstructured":"Abad\u00ed, M., Manna, Z.: Nonclausal deduction in first-order temporal logic. Journal of the ACM\u00a037(2), 279\u2013317 (1990)","journal-title":"Journal of the ACM"},{"key":"17_CR2","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BFb0012826","volume-title":"9th International Conference on Automated Deduction","author":"A. Bundy","year":"1988","unstructured":"Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, R., Overbeek, R. (eds.) 9th International Conference on Automated Deduction, pp. 111\u2013120. Springer, Heidelberg (1988); Longer version available from Edinburgh as DAI Research Paper No. 349"},{"key":"17_CR3","unstructured":"Bundy, A.: Proof planning. In: Drabble, B. (ed.) Proceedings of the 3rd International Conference on AI Planning Systems (AIPS) 1996, pp. 261\u2013267 (1996); also available as DAI Research Report 886"},{"key":"17_CR4","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence\u00a062, 185\u2013253 (1993); Also available from Edinburgh as DAI Research Paper No. 567.","journal-title":"Artificial Intelligence"},{"key":"17_CR5","volume-title":"Feature Interactions in Telecommunications and Software Systems","author":"M. Calder","year":"2000","unstructured":"Calder, M., Magill, E.: Feature Interactions in Telecommunications and Software Systems, vol.\u00a0VI. IOS Press, Amsterdam (2000)"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Calder, M., Miller, A.: Automated verification of any number of concurrent, communicating processes. In: Proceedings of the 17th IEEE Automated Software Engineering (ASE 2002), pp. 227\u2013230 (2002)","DOI":"10.1109\/ASE.2002.1115017"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Calder, M., Kolberg, M., Magill, E.H., Reiff-Marganiec, S.: Feature interaction: A critical review and considered forecast. Computer Networks (2002)","DOI":"10.1016\/S1389-1286(02)00352-3"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-45139-0_9","volume-title":"Model Checking Software","author":"M. Calder","year":"2001","unstructured":"Calder, M., Miller, A.: Using SPIN for feature interaction analysis - A case study. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 143\u2013162. Springer, Heidelberg (2001)"},{"key":"17_CR9","unstructured":"Calder, M., Miller, A.: Feature interaction detection by pairwise analysis of LTL properties. Submitted to FMSD - Formal Methods in Software Development. Still under review at the time of writing (2005) (April 2002)"},{"key":"17_CR10","unstructured":"Castellini, C.: Automated reasoning in quantified modal and temporal logics. PhD thesis, School of Informatics, University of Edinburgh, UK (2005)"},{"key":"17_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/3-540-36078-6_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Castellini","year":"2002","unstructured":"Castellini, C., Smaill, A.: Proof planning for feature interactions: a preliminary report. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol.\u00a02514, pp. 102\u2013114. Springer, Heidelberg (2002)"},{"issue":"6","key":"17_CR12","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1093\/jigpal\/10.6.571","volume":"10","author":"C. Castellini","year":"2002","unstructured":"Castellini, C., Smaill, A.: A systematic presentation of quantified modal logics. Logic Journal of the IGPL\u00a010(6), 571\u2013599 (2002)","journal-title":"Logic Journal of the IGPL"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Fisher, M., Konev, B.: Monodic temporal resolution. In: Baader, F. (ed.) Proceedings of CADE-19, International Conference on Automated Deduction, Miami, FL, USA (2003)","DOI":"10.1007\/978-3-540-45085-6_35"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/BFb0031802","volume-title":"Formal Methods in Computer-Aided Design","author":"F.J. Cantu","year":"1996","unstructured":"Cantu, F.J., Bundy, A., Smaill, A., Basin, D.: Experiments in automating hardware verification using inductive proof planning. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 94\u2013108. Springer, Heidelberg (1996)"},{"issue":"1","key":"17_CR15","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/BF00881900","volume":"11","author":"A. Felty","year":"1993","unstructured":"Felty, A.: Implementing tactics and tacticals in a higher-order logic programming language. Journal of Automated Reasoning\u00a011(1), 43\u201381 (1993)","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR16","unstructured":"Felty, A.: Temporal logic theorem proving and its application to the feature interaction problem. In: E.\u00a0Giunchiglia and F.\u00a0Massacci, editors, Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, number D11 14\/01 in Technical Report, University of Siena (2001)"},{"key":"17_CR17","volume-title":"Feature Interactions Workshop","author":"A.P. Felty","year":"2000","unstructured":"Felty, A.P., Namjoshi, K.S.: Feature specification and automated conflict detection. In: Feature Interactions Workshop, IOS Press, Amsterdam (2000)"},{"issue":"4","key":"17_CR18","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1016\/S1389-1286(00)00007-4","volume":"32","author":"N. Griffeth","year":"2000","unstructured":"Griffeth, N., Blumenthal, R., Gregoire, J.-C., Ohta, T.: A feature interaction benchmark for the first feature interaction detection contest. Computer Networks 1999\u00a032(4), 389\u2013418 (2000)","journal-title":"Computer Networks 1999"},{"key":"17_CR19","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0168-0072(00)00018-X","volume":"106","author":"I. Hodkinson","year":"2000","unstructured":"Hodkinson, I., Wolter, F., Zakharyaschev, M.: Decidable fragments of first order temporal logics. Annals of Pure and Applied Logic\u00a0106, 85\u2013134 (2000)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"9","key":"17_CR20","doi-asserted-by":"publisher","first-page":"981","DOI":"10.1016\/0169-7552(93)90095-L","volume":"25","author":"G.J. Holzmann","year":"1993","unstructured":"Holzmann, G.J.: Design and validation of protocols: a tutorial. Computer Networks and ISDN Systems\u00a025(9), 981\u20131017 (1993); also in: Proc. 11th PSTV 1991, INWG\/IFIP, Stockholm, Sweden","journal-title":"Computer Networks and ISDN Systems"},{"issue":"5","key":"17_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker spin. IEEE Trans. on Software Engineering\u00a023(5), 279\u2013295 (1997); Special issue on Formal Methods in Software Practice.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"17_CR22","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/978-94-017-0437-3_4","volume-title":"Automated Deduction, a Basis for Application \u2013 Handbook of the German Focus Programme on Automated Deduction, ch. III.4","author":"M. Kerber","year":"1998","unstructured":"Kerber, M.: Proof planning: A practical approach to mechanized reasoning in mathematics. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction, a Basis for Application \u2013 Handbook of the German Focus Programme on Automated Deduction, ch. III.4, pp. 77\u201395. Kluwer Academic Publishers, Dordrecht (1998)"},{"key":"17_CR23","unstructured":"Maclean, E., Fleuriot, J., Smaill, A.: Proof-planning non-standard analysis. In: Proceedings of the Seventh International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida (2002)"},{"issue":"1","key":"17_CR24","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0004-3702(99)00076-4","volume":"115","author":"E. Melis","year":"1999","unstructured":"Melis, E., Siekmann, J.: Knowledge-based proof planning. Artificial Intelligence\u00a0115(1), 65\u2013105 (1999)","journal-title":"Artificial Intelligence"},{"key":"17_CR25","series-title":"Logic Programming","volume-title":"Handbook of Logic in AI and Logic Programming","author":"G. Nadathur","year":"1986","unstructured":"Nadathur, G., Miller, D.: Higher-order logic programming. In: Gabbay, D., Hogger, C., Robinson, A. (eds.) Handbook of Logic in AI and Logic Programming. Logic Programming, vol.\u00a05, Springer Verlag, Oxford (1986)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-20"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11532231_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T06:05:29Z","timestamp":1740290729000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11532231_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540280057","9783540318644"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/11532231_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}