{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T19:27:14Z","timestamp":1740166034004,"version":"3.37.3"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T00:00:00Z","timestamp":1620086400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T00:00:00Z","timestamp":1620086400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Prog Artif Intell"],"published-print":{"date-parts":[[2021,12]]},"DOI":"10.1007\/s13748-021-00240-8","type":"journal-article","created":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T21:02:50Z","timestamp":1620162170000},"page":"375-389","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["First-order logic as a constraint satisfaction problem"],"prefix":"10.1007","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6081-301X","authenticated-orcid":false,"given":"Hirohiko","family":"Kushida","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Haralick","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,5,4]]},"reference":[{"key":"240_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1023\/A:1004275029985","volume":"27","author":"H Andreka","year":"1998","unstructured":"Andreka, H., van Benthem, J., Nemeti, I.: Modal languages and bounded fragments of predicate logic. J. Philosoph. Logic 27, 217\u2013274 (1998)","journal-title":"J. Philosoph. Logic"},{"key":"240_CR2","doi-asserted-by":"crossref","unstructured":"Apt, K.R., Vermeulen, C.F.M.: First-Order Logic as a Constraint Programming Language. In: Baaz M., Voronkov A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR, : Lecture Notes in Computer Science, vol. 2514, p. 2002. Springer, Berlin, Heidelberg (2002)","DOI":"10.1007\/3-540-36078-6_2"},{"key":"240_CR3","doi-asserted-by":"crossref","unstructured":"Atserias, A., Kolaitis, P.G., Vardi, M.Y.: Constraint Propagation as a Proof System. In: Wallace, M. (ed.) Principles and Practice of Constraint Programming-CP 2004. Lecture Notes in Computer Science, vol. 3258. Springer, Berlin, Heidelberg (2004)","DOI":"10.1007\/978-3-540-30201-8_9"},{"issue":"3","key":"240_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2701414","volume":"62","author":"V Barany","year":"2015","unstructured":"Barany, V., Cate, B.T., Segoufin, L.: Guarded negation. J. ACM Assoc. Comput. Mach. 62(3), 1\u201326 (2015)","journal-title":"J. ACM Assoc. Comput. Mach."},{"key":"240_CR5","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1016\/0004-3702(88)90023-9","volume":"35","author":"W Bibel","year":"1988","unstructured":"Bibel, W.: Constraint satisfaction from a deductive viewpoint. Artif. Intell. 35, 401\u2013413 (1988)","journal-title":"Artif. Intell."},{"key":"240_CR6","unstructured":"Colmerauer, A.: Prolog II reference manual and theoretical model, Technical Report. Groupe d\u2019Intelligence Arificielle. Universit\u00e9 d\u2019Aix-Marseille II, Luminy (1982)"},{"key":"240_CR7","doi-asserted-by":"publisher","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning A new form of the Herbrand-Gentzen theorem. J. Symbol. Logic 22, 250\u2013268 (1957)","journal-title":"J. Symbol. Logic"},{"key":"240_CR8","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symbol. Logic 22, 269\u2013285 (1957)","journal-title":"J. Symbol. Logic"},{"issue":"1","key":"240_CR9","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/S0304-3975(00)00330-3","volume":"278","author":"M Fitting","year":"2002","unstructured":"Fitting, M.: Fixpoint semantics for logic programming: a survey. Theor. Comput. Sci. 278(1), 25\u201351 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"240_CR10","doi-asserted-by":"crossref","unstructured":"Freuder, E.C., Mackworth, A.K.: Constraint Satisfaction: An Emerging Paradigm, In: F. Rossi, P. van Beek and T. Walsh (ed.), Handbook of Constraint Programming, Elsevier (2006)","DOI":"10.1016\/S1574-6526(06)80006-4"},{"key":"240_CR11","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen I, II, Mathematische Zeitschrift, 39, pp. 176\u2013210; 405\u2013431, 1934, (1935)","DOI":"10.1007\/BF01201363"},{"key":"240_CR12","unstructured":"G\u00f6del, K.: \u00dcber die Vollst\u00e4ndigkeit des Logikkalk\u00fcks, PhD thesis, at Wien University, (1929)"},{"key":"240_CR13","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/0004-3702(80)90051-X","volume":"14","author":"R Haralick","year":"1980","unstructured":"Haralick, R., Elliott, G.L.: Increasing tree search efficiency for constraint satisfaction problems. Artif. Intell. 14, 263\u2013313 (1980)","journal-title":"Artif. Intell."},{"key":"240_CR14","doi-asserted-by":"crossref","unstructured":"Haralick, R., Liu, L., Misshula, E.: Relation Decomposition: The Theory, International Conference on Machine Learning and Data Mining, (MLDM), 2013, New York, July 22-25, (2013)","DOI":"10.1007\/978-3-642-39712-7_24"},{"key":"240_CR15","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Lassez, J.L.: Constraint logic programming, Technical report, Department of Computer Science, Monash University, (1986)","DOI":"10.1145\/41625.41635"},{"key":"240_CR16","doi-asserted-by":"crossref","unstructured":"Kolaitis, P.G., Vardi, M.Y.: A Logical Approach to Constraint Satisfaction. In: Creignou, N., Kolaitis, P.G., Vollmer, H. (eds.) Complexity of Constraints. Lecture Notes in Computer Science, vol. 5250. Springer, Berlin, Heidelberg (2007)","DOI":"10.1007\/978-3-540-92800-3_6"},{"key":"240_CR17","doi-asserted-by":"crossref","unstructured":"Liu, Y.A., Stoller, S.D.: Founded Semantics and Constraint Semantics of Logic Rules. In: Artemov S., Nerode A. (eds) Logical Foundations of Computer Science. LFCS 2018. Lecture Notes in Computer Science, vol 10703, Springer","DOI":"10.1007\/978-3-319-72056-2_14"},{"key":"240_CR18","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0004-3702(92)90003-G","volume":"58","author":"AK Mackworth","year":"1992","unstructured":"Mackworth, A.K.: The logic of constraint satisfaction. Artif. Intell. 58, 3\u201320 (1992)","journal-title":"Artif. Intell."},{"key":"240_CR19","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Applications of Craig Interpolation to Model Checking, In: Ciardo G., Darondeau P. (eds) Applications and Theory of Petri Nets, ICATPN 2005. Lecture Notes in Computer Science, vol. 3536. Springer, Berlin, Heidelberg (2005)","DOI":"10.1007\/11494744_2"},{"key":"240_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-66473-1","volume-title":"Proof Theory","author":"G Sch\u00fctte","year":"1977","unstructured":"Sch\u00fctte, G.: Proof Theory. Springer, Berlin (1977)"},{"key":"240_CR21","volume-title":"Proof Theory","author":"G Takeuti","year":"1987","unstructured":"Takeuti, G.: Proof Theory, 2nd edn. North-Holland, Amsterdam (1987)","edition":"2"},{"issue":"3","key":"240_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2499937.2499938","volume":"14","author":"J Wittocx","year":"2013","unstructured":"Wittocx, J., Denecker, M., Bruynooghe, M.: Constraint propagation for first-order logic and inductive definitions. ACM Trans. Comput. Logic 14(3), 1\u201345 (2013)","journal-title":"ACM Trans. Comput. Logic"},{"key":"240_CR23","unstructured":"Zhou, N.F.: Combinatorial Search With Picat, International Conference on Logic Programming (ICLP) 2014, Invited talk, (2014)"},{"key":"240_CR24","doi-asserted-by":"crossref","unstructured":"Zhou, N.F., Kjellerstrand, H., Fruhman, J.: Constraint Solving and Planning with Picat, Springer, ISBN:978-3-319-25881-2. (2015)","DOI":"10.1007\/978-3-319-25883-6"}],"container-title":["Progress in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s13748-021-00240-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s13748-021-00240-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s13748-021-00240-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,5]],"date-time":"2021-11-05T13:20:27Z","timestamp":1636118427000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s13748-021-00240-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,4]]},"references-count":24,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["240"],"URL":"https:\/\/doi.org\/10.1007\/s13748-021-00240-8","relation":{},"ISSN":["2192-6352","2192-6360"],"issn-type":[{"type":"print","value":"2192-6352"},{"type":"electronic","value":"2192-6360"}],"subject":[],"published":{"date-parts":[[2021,5,4]]},"assertion":[{"value":"13 September 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 March 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 May 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}