{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:02:04Z","timestamp":1725663724062},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540577850"},{"type":"electronic","value":"9783540483328"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57785-8_132","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:21:21Z","timestamp":1330262481000},"page":"71-82","source":"Crossref","is-referenced-by-count":8,"title":["Two proof procedures for a cardinality based language in propositional calculus"],"prefix":"10.1007","author":[{"given":"Belaid","family":"Benhamou","sequence":"first","affiliation":[]},{"given":"Lakhdar","family":"Sais","sequence":"additional","affiliation":[]},{"given":"Pierre","family":"Siegel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"6_CR1","volume-title":"PhD thesis","author":"A. S. M. Aguirre","year":"1992","unstructured":"A. S. M. Aguirre. How to use symmetries in boolean constraints solving. PhD thesis, GIA-Luminy (Marseille), 1992."},{"key":"6_CR2","unstructured":"B. Benhamou and L. Sais. Cardinality formulas in propositional calculus. Technical Report 1, Universit\u00e9 de provence, 1992."},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"B. Benhamou and L. Sais. Theoretical study of symmetries in propositional calculus and application. Eleventh International Conference on Automated Deduction, Saratoga Springs,NY, USA, 1992.","DOI":"10.1007\/3-540-55602-8_172"},{"issue":"28","key":"6_CR4","first-page":"412","volume":"4","author":"A. Colmerauer","year":"1990","unstructured":"A. Colmerauer. An introduction to prolog III. CACM, 4(28):412\u2013418, 1990.","journal-title":"CACM"},{"key":"6_CR5","volume-title":"working paper","author":"C. C. Cook","year":"1985","unstructured":"C. C. Cook, W. Cook and Gy. Cook, on the complexity of cutting-planes proofs, working paper, Cornell university, ithaca, ny. 1985."},{"key":"6_CR6","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. A computing procedure for quatification theory. JACM, (7):201\u2013215, 1960.","journal-title":"JACM"},{"key":"6_CR7","unstructured":"M. Dincbas, P. V. Hentenryck, H. Simonis, A. Aggoun, T. Grof, and F.Berthier. The constraint logic programing language CHIP. In the International Conference on Fifth Generation Computer Systems, Tokyo, Japon, December 1988."},{"key":"6_CR8","unstructured":"P. V. Hentenryck and Y. Deville. The cardinality operator: A new logical connective for constraint logic programming. Technical report, CS Departement, Brown University, Technical Report, October, 1990."},{"key":"6_CR9","unstructured":"J. N. Hooker. Generalized resolution and cutting planes. Approches to Intelligent Decision Suport, a volume in Annals of Operations Researchs series."},{"key":"6_CR10","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0167-9236(88)90097-8","volume":"4","author":"J. N. Hooker","year":"1988","unstructured":"J. N. Hooker. A quantitive approach to logical inference. Decision Suport Systems, (4):45\u201369, 1988.","journal-title":"Decision Suport Systems"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"J. Jaffar and J. L. Lassez. Constraint logic programing. POPL-87,Munich, FRG, January 1988.","DOI":"10.1145\/41625.41635"},{"key":"6_CR12","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","volume":"2","author":"R. Kowalski","year":"1971","unstructured":"R. Kowalski and D. Kuehner. Linear resolution with selection function. Artificial Intelligence, (2):227\u2013260, 1971.","journal-title":"Artificial Intelligence"},{"key":"6_CR13","first-page":"253","volume":"22","author":"B. Krishnamurty","year":"1985","unstructured":"B. Krishnamurty. Short proofs for tricky formulas. Acta informatica, (22):253\u2013275, 1985.","journal-title":"Acta informatica"},{"key":"6_CR14","volume-title":"PhD thesis","author":"L. Oxusoff","year":"1989","unstructured":"L. Oxusoff and A. Rauzy. L'\u00e9valuation s\u00e9mantique en calcul propositionnel. PhD thesis, GIA-Luminy (Marseille), 1989."}],"container-title":["Lecture Notes in Computer Science","STACS 94"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57785-8_132.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:13:52Z","timestamp":1605647632000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57785-8_132"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540577850","9783540483328"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-57785-8_132","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}