{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:32:51Z","timestamp":1725485571810},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540000105"},{"type":"electronic","value":"9783540360780"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36078-6_7","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T02:48:36Z","timestamp":1180666116000},"page":"102-114","source":"Crossref","is-referenced-by-count":1,"title":["Proof Planning for Feature Interactions: A Preliminary Report"],"prefix":"10.1007","author":[{"given":"Claudio","family":"Castellini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Smaill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,10,24]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Martin Abad\u00ed and Zohar Manna. Nonclausal deduction in first-order temporal logic. Journal of the ACM, 37(2):279\u2013317, April 1990.","DOI":"10.1145\/77600.77617"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"A. Bundy. The use of explicit plans to guide inductive proofs. In R. Lusk and R. Overbeek, editors, 9th International Conference on Automated Deduction, pages 111\u2013120. Springer-Verlag, 1988. Longer version available from Edinburgh as DAI Research Paper No. 349.","DOI":"10.1007\/BFb0012826"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Muffy Calder, Mario Kolberg, Evan H. Magill, and Stephan Reiff-Marganiec. Feature interaction: A critical review and considered forecast. Computer Networks, 2002.","DOI":"10.1016\/S1389-1286(02)00352-3"},{"key":"7_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/3-540-45139-0_9","volume-title":"Model checking software: 8th International SPIN Workshop, Toronto, Canada, May 19\u201320, 2001: proceedings","author":"M. Calder","year":"2001","unstructured":"Muffy Calder and Alice Miller. Using SPIN for feature interaction analysis \u2014A case study. In M.B. Dwyer, editor, Model checking software: 8th International SPIN Workshop, Toronto, Canada, May 19\u201320, 2001: proceedings, pages 143\u2013162. Springer, 2001. Lecture Notes in Computer Science No. 2057."},{"key":"7_CR5","unstructured":"C. Castellini and A. Smaill. Tactic-based theorem proving in first-order modal and temporal logics. In E. Giunchiglia and F. Massacci, editors, Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, TR DII 14\/01. University of Siena, June 2001."},{"key":"7_CR6","unstructured":"C. Castellini and A. Smaill. Modular, uniform and normalising sequent calculi for quantified modal logics. Technical report, Division of Informatics, 2002."},{"issue":"1","key":"7_CR7","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/BF00881900","volume":"11","author":"A. Felty","year":"1993","unstructured":"A. Felty. Implementing tactics and tacticals in a higher-order logic programming language. Journal of Automated Reasoning, 11(1):43\u201381, 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"7_CR8","unstructured":"Amy Felty. Temporal logic theorem proving and its application to the feature interaction problem. In E. Giunchiglia and F. Massacci, editors, Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, TR DII 14\/01. University of Siena, June 2001."},{"issue":"4","key":"7_CR9","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1006\/jsco.1996.0094","volume":"23","author":"A. Felty","year":"1997","unstructured":"Amy Felty and Laurent Thery. Interactive theorem proving with temporal logic. Journal of Symbolic Computation, 23(4):367\u2013397, 1997.","journal-title":"Journal of Symbolic Computation"},{"key":"7_CR10","unstructured":"Amy P. Felty and Kedar S. Namjoshi. Feature specification and automated conflict detection. In Feature Interactions Workshop. IOS Press, 2000."},{"key":"7_CR11","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538332.001.0001","volume-title":"Labelled Deductive Systems, Volume 1","author":"D. M. Gabbay","year":"1996","unstructured":"Dov M. Gabbay. Labelled Deductive Systems, Volume 1. Oxford University Press, Oxford, 1996."},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Nancy Griffeth, Ralph Blumenthal, Jean-Charles Gregoire, and Tadashi Ohta. A feature interaction benchmark for the first feature interaction detection contest. Computer Networks (Amsterdam, Netherlands: 1999), 32(4):389\u2013418, April 2000.","DOI":"10.1016\/S1389-1286(00)00007-4"},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0168-0072(00)00018-X","volume":"106","author":"I. Hodkinson","year":"2000","unstructured":"I. Hodkinson, F. Wolter, and M. Zakharyaschev. Decidable fragments of first order temporal logics. Annals of Pure and Applied Logic, 106:85\u2013134, 2000.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1","key":"7_CR14","first-page":"65","volume":"8","author":"B. Jonsson","year":"2001","unstructured":"Bengt Jonsson, Tiziana Margaria, Gustaf Naeser, Jan Nystr\u00f6m, and Bernhard Steffen. Incremental requirement specification for evolving systems. Nordic Journal of Computing, 8(1):65\u201387, Spring 2001.","journal-title":"Nordic Journal of Computing"},{"key":"7_CR15","volume-title":"Handbook of Logic in AI and Logic Programming, Volume 5: Logic Programming","author":"G. Nadathur","year":"1986","unstructured":"Gopalan Nadathur and Dale Miller. Higher-order logic programming. In D. Gabbay, C. Hogger, and A. Robinson, editors, Handbook of Logic in AI and Logic Programming, Volume 5: Logic Programming. Springer Verlag, Oxford, 1986."},{"key":"7_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1007\/3-540-44957-4_35","volume-title":"On an \u03c9-decidable deductive procedure for non-Horn sequents of a restricted FTL","author":"R. Pliuskevi\u010dius","year":"2000","unstructured":"Regimantas Pliuskevi\u010dius. On an \u03c9-decidable deductive procedure for non-Horn sequents of a restricted FTL. Lecture Notes in Computer Science, 1861:523\u2013537, 2000."},{"key":"7_CR17","first-page":"522","volume-title":"Proceedings 11th Intl. Conf. on Automated Deduction, CADE\u201992, Saratoga Springs, CA, USA, 15\u201318 June 1992","author":"N. Shankar","year":"1992","unstructured":"Natarajan Shankar. Proof search in the intuitionistic sequent calculus. In D. Kapur, editor, Proceedings 11th Intl. Conf. on Automated Deduction, CADE\u201992, Saratoga Springs, CA, USA, 15\u201318 June 1992, volume 607, pages 522\u2013536. Springer-Verlag, Berlin, 1992."},{"key":"7_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/BFb0105418","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996","author":"A. Smaill","year":"1996","unstructured":"Alan Smaill and Ian Green. Higher-order annotated terms for proof search. In Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996, volume 1275 of Lecture Notes in Computer Science, pages 399\u2013414, Turku, Finland, 1996. Springer-Verlag. Also available as DAI Research Paper 799."},{"key":"7_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3208-5","volume-title":"Labelled Non-Classical Logics","author":"L. Vigan\u00f3","year":"2000","unstructured":"Luca Vigan\u00f3. Labelled Non-Classical Logics. Kluwer Academic Publishers, Dordrecht, 2000."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36078-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,14]],"date-time":"2024-02-14T18:15:32Z","timestamp":1707934532000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36078-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540000105","9783540360780"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-36078-6_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}