{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T02:08:36Z","timestamp":1649124516494},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2006,10,6]],"date-time":"2006-10-06T00:00:00Z","timestamp":1160092800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2007,1,17]]},"DOI":"10.1007\/s10817-006-9037-y","type":"journal-article","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T07:01:46Z","timestamp":1160031706000},"page":"45-66","source":"Crossref","is-referenced-by-count":0,"title":["Checking Consistency and Completeness of On-Line Product Manuals"],"prefix":"10.1007","volume":"37","author":[{"given":"Carsten","family":"Sinz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"K\u00fcchlin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dieter","family":"Feichtinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georg","family":"G\u00f6rtler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,10,6]]},"reference":[{"key":"9037_CR1","volume-title":"The Description Logic Handbook","year":"2000","unstructured":"Baader, F., McGuinness, D., Nardi, P., Patel-Schneider, P. (eds.) The Description Logic Handbook. Cambridge University Press, Cambridge, UK (2003)"},{"issue":"3","key":"9037_CR2","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1145\/62065.62067","volume":"32","author":"V.E. Barker","year":"1989","unstructured":"Barker, V.E., O\u2019Connor, D.E.: Expert systems for configuration at Digital: XCON and beyond. Commun. ACM 32(3), 298\u2013318 (1989)","journal-title":"Commun. ACM"},{"issue":"8","key":"9037_CR3","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"9037_CR4","doi-asserted-by":"crossref","unstructured":"B\u00fchler, D., K\u00fcchlin, W.: A flexible similarity assessment framework for XML documents based on XQL and Java Reflection. In: Proc. 14th Intl. Conf. on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (IEA\/AIE 2001), LNAI 2070, Budapest, Hungary. Springer, Berlin Heidelberg New York (2001)","DOI":"10.1007\/3-540-45517-5_21"},{"issue":"7","key":"9037_CR5","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"3","key":"9037_CR6","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"9037_CR7","unstructured":"Davis, S.M.: Future Perfect. Addison-Wesley, New York (1987)"},{"key":"9037_CR8","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Proc. 6th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2003), pp. 502\u2013518. Springer, Berlin Heidelberg New York (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"issue":"4","key":"9037_CR9","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1142\/S0218194000000249","volume":"10","author":"A. Felfernig","year":"2000","unstructured":"Felfernig, A., Friedrich, G.E., Jannach, D.: UML as domain specific language for the construction of knowledge-based configuration systems. Int. J. Softw. Eng. Knowl. Eng. 10(4), 449\u2013469 (2000)","journal-title":"Int. J. Softw. Eng. Knowl. Eng."},{"key":"9037_CR10","unstructured":"Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Proc. 5th Intl. Conf. on Logic Programming, pp. 1070\u20131080. The MIT Press, Cambridge, MA (1988)"},{"key":"9037_CR11","unstructured":"Haarslev, V., M\u00f6ller, R.: Description of the RACER system and its applications. In: Working Notes of the 2001 International Description Logics Workshop (DL-2001), Stanford, CA (2001)"},{"key":"9037_CR12","unstructured":"Horrocks, I.: FaCT. In: Proceedings of the 1998 International Workshop on Description Logics (DL\u201998), IRST, Povo-Trento, Italy (1998)"},{"key":"9037_CR13","unstructured":"Kaiser, A.: A SAT-based propositional prover for consistency checking of automotive product data. Technical report, WSI-2001-16, University of T\u00fcbingen (2001)"},{"issue":"1\u20132","key":"9037_CR14","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1023\/A:1006370506164","volume":"24","author":"W. K\u00fcchlin","year":"2000","unstructured":"K\u00fcchlin, W., Sinz, C.: Proving consistency assertions for automotive product data management. J. Autom. Reason. 24(1\u20132), 145\u2013163 (2000)","journal-title":"J. Autom. Reasoning"},{"issue":"3","key":"9037_CR15","first-page":"76","volume":"29","author":"D. Lee","year":"2000","unstructured":"Lee, D., Chu, W.W.: Comparative analysis of six XML schema languages. SIGMOD Record (ACM Special Interest Group on Management of Data) 29(3), 76\u201387 (2000)","journal-title":"SIGMOD Record (ACM Special Interest Group on Management of Data)"},{"issue":"4","key":"9037_CR16","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1017\/S0890060498124101","volume":"12","author":"D. Mailharro","year":"1998","unstructured":"Mailharro, D.: A classification and constraint-based framework for configuration. Artif. Intell. Eng. Des. Anal. Manuf. (AI EDAM) 12(4), 383\u2013397 (1998)","journal-title":"Artif. Intell. Eng. Des. Anal. Manuf. (AI EDAM)"},{"key":"9037_CR17","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: Conflict analysis in search algorithms for propositional satisfiability. In: Proc. IEEE International Conference on Tools with Artificial Intelligence (1996)"},{"issue":"1","key":"9037_CR18","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/0004-3702(82)90021-2","volume":"19","author":"J. McDermott","year":"1982","unstructured":"McDermott, J.: R1: A rule-based configurer of computer systems. Artif. Intell. 19(1), 39\u201388 (1982)","journal-title":"Artif. Intell."},{"issue":"4","key":"9037_CR19","first-page":"333","volume":"12","author":"D.L. McGuiness","year":"1998","unstructured":"McGuiness, D.L., Wright, J.R.: Conceptual modelling for configuration: a description logic-based approach. AI EDAM 12(4), 333\u2013344 (1998)","journal-title":"AI EDAM"},{"key":"9037_CR20","unstructured":"McGuinness, D.L.: Configuration. In Baader et al. [1], pp. 397\u2013414"},{"key":"9037_CR21","unstructured":"Mittal, S., Frayman, F.: Towards a generic model of configuration tasks. In: Proc. 11th Intl. Joint Conf. on Artificial Intelligence, pp. 1395\u20131401, Detroit, MI (1989)"},{"key":"9037_CR22","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. 38th Design Automation Conference (DAC\u201901) (2001)","DOI":"10.1145\/378239.379017"},{"issue":"2","key":"9037_CR23","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/514183.514186","volume":"2","author":"C. Nentwich","year":"2002","unstructured":"Nentwich, C., Capra, L., Emmerich, W., Finkelstein, A.: XLinkIt: A consistency checking and smart link generation service. ACM Transactions on Internet Technology 2(2), 151\u2013185 (2002)","journal-title":"ACM Transactions on Internet Technology"},{"key":"9037_CR24","first-page":"153","volume-title":"Proc. Artificial Intelligence and Manufacturing Research Planning Workshop","author":"D. Sabin","year":"1996","unstructured":"Sabin, D., Freuder, E.C.: Configuration as composite constraint satisfaction. In: Luger, G.F. (ed.) Proc. Artificial Intelligence and Manufacturing Research Planning Workshop, pp. 153\u2013161. AAAI, Albuquerque, NM (1996)"},{"issue":"4","key":"9037_CR25","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1109\/5254.708432","volume":"13","author":"D. Sabin","year":"1998","unstructured":"Sabin, D., Weigel, R.: Product configuration frameworks \u2013 a survey. IEEE Intell. Syst. 13(4), 42\u201349 (1998)","journal-title":"IEEE Intell. Syst."},{"key":"9037_CR26","doi-asserted-by":"crossref","unstructured":"Sinz, C.: Towards an optimal CNF encoding of Boolean cardinality constraints. In: Proc. 11th Intl. Conf. on Principles and Practice of Constraint Programming (CP 2005), pp. 827\u2013831 (2005)","DOI":"10.1007\/11564751_73"},{"key":"9037_CR27","volume-title":"LICS\u20192001 Workshop on Theory and Applications of Satisfiability Testing (SAT\u20192001), vol. 9 of Electronic Notes in Discrete Mathematics","author":"C. Sinz","year":"2001","unstructured":"Sinz, C., Blochinger, W., K\u00fcchlin, W.: PaSAT - parallel SAT-checking with lemma exchange: Implementation and applications. In: Kautz, H., Selman, B. (eds.) LICS\u20192001 Workshop on Theory and Applications of Satisfiability Testing (SAT\u20192001), vol. 9 of Electronic Notes in Discrete Mathematics. Elsevier Science, Boston, MA (2001)"},{"issue":"1","key":"9037_CR28","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1017\/S0890060403171065","volume":"17","author":"C. Sinz","year":"2003","unstructured":"Sinz, C., Kaiser, A., K\u00fcchlin, W.: Formal methods for the validation of automotive product configuration data. Artif. Intell. Eng. Des. Anal. Manuf. 17(1), 75\u201397 (2003). Special issue on configuration","journal-title":"Artif. Intell. Eng. Des. Anal. Manuf."},{"key":"9037_CR29","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1109\/QSIC.2003.1319113","volume-title":"Proc. 3rd International Conference on Quality Software (QSIC 2003)","author":"C. Sinz","year":"2003","unstructured":"Sinz, C., Khosravizadeh, A., K\u00fcchlin, W., Mihajlovski, V.: Verifying CIM models of Apache web server configurations. In: Proc. 3rd International Conference on Quality Software (QSIC 2003), pp. 290\u2013297. IEEE Computer Society, Dallas, TX (2003)"},{"key":"9037_CR30","first-page":"391","volume-title":"Proc. 6th Intl. Conf. on Formal Engineering Methods (ICFEM\u20192004)","author":"C. Sinz","year":"2004","unstructured":"Sinz, C., K\u00fcchlin, W.: Verifying the on-line help system of SIEMENS magnetic resonance tomographs. In: Proc. 6th Intl. Conf. on Formal Engineering Methods (ICFEM\u20192004), pp. 391\u2013402. Springer, Seattle, WA (2004)"},{"issue":"14","key":"9037_CR31","doi-asserted-by":"crossref","first-page":"857","DOI":"10.1016\/S0950-5849(02)00120-9","volume":"44","author":"C. Sinz","year":"2002","unstructured":"Sinz, C., Lumpp, T., Schneider, J., K\u00fcchlin, W.: Detection of dynamic execution errors in IBM System Automation\u2019s rule-based expert system. Inf. Softw. Technol. 44(14), 857\u2013873 (2002)","journal-title":"Inf. Softw. Technol."},{"key":"9037_CR32","unstructured":"Smolka, G.: A feature logic with subsorts. LILOG Report 33, IWBS, IBM Deutschland, Stuttgart, Germany (1988)"},{"key":"9037_CR33","doi-asserted-by":"crossref","unstructured":"Soininen, T., Niemel\u00e4, I.: Developing a declarative rule language for applications in product configuration. In: Proc. 1st Intl. Workshop on Practical Aspects of Declarative Languages (PADL\u201999), pp. 305\u2013319, San Antonio, TX (1999)","DOI":"10.1007\/3-540-49201-1_21"},{"issue":"4","key":"9037_CR34","first-page":"357","volume":"12","author":"T. Soininen","year":"1998","unstructured":"Soininen, T., Tiihonen, J., M\u00e4nnist\u00f6, T., Sulonen, R.: Towards a general ontology of configuration. AI EDAM 12(4), 357\u2013372 (1998)","journal-title":"AI EDAM"},{"key":"9037_CR35","unstructured":"Somenzi, F.: Cudd: Cu decision diagram package release (1998)"},{"key":"9037_CR36","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed) Studies in Constructive Mathematics and Mathematical Logic, pp. 115\u2013125 (1970)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"9037_CR37","unstructured":"XML Schema Parts 0\u20132: Primer, Structures, Datatypes. W3C Recommendation (2001)"},{"key":"9037_CR38","unstructured":"XML Path Language 2.0. W3C Working Draft, April 2002"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9037-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-006-9037-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9037-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:21:46Z","timestamp":1559251306000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-006-9037-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10,6]]},"references-count":38,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2007,1,17]]}},"alternative-id":["9037"],"URL":"https:\/\/doi.org\/10.1007\/s10817-006-9037-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,10,6]]}}}