{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:04:37Z","timestamp":1773655477668,"version":"3.50.1"},"reference-count":8,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2011,12,1]],"date-time":"2011-12-01T00:00:00Z","timestamp":1322697600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2011,12,1]],"date-time":"2011-12-01T00:00:00Z","timestamp":1322697600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Aut. Conrol Comp. Sci."],"published-print":{"date-parts":[[2011,12]]},"DOI":"10.3103\/s0146411611070054","type":"journal-article","created":{"date-parts":[[2012,1,5]],"date-time":"2012-01-05T17:57:59Z","timestamp":1325786279000},"page":"402-407","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["On the calculus of positively constructed formulas for automated theorem proving"],"prefix":"10.3103","volume":"45","author":[{"given":"A. V.","family":"Davydov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. A.","family":"Larionov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"E. A.","family":"Cherkashin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1627","published-online":{"date-parts":[[2012,1,6]]},"reference":[{"key":"6166_CR1","volume-title":"Intellektnoe upravlenie dinamicheskimi sistemami","author":"S.N. Vasil\u2019ev","year":"2000","unstructured":"Vasil\u2019ev, S.N., Zherlov, A.K., Fedunov, E.A., and Fedosov, V.E., Intellektnoe upravlenie dinamicheskimi sistemami (Intellectual Management of Dynamical Systems), Moscow: Fizmatlit, 2000."},{"key":"6166_CR2","unstructured":"Zherlov, A.K. and Vasil\u2019ev, S.N., Calculation of Positive-Oriented Formulae, in Aktual\u2019nye problemy informatiki, prikladnoi matematiki i mekhaniki: Sb. nauchnykh trudov (Actual Problems of Informatics, Applied Mathematics and Mechanics. Collection of Scientific Papers), Krasnoyarsk, 1996, part 1."},{"key":"6166_CR3","doi-asserted-by":"crossref","unstructured":"Robinson, J.A., A Machine-Oriented Logic Based on Resolution Principle, J. ACM, 1965, no. 1, pp. 23\u201341.","DOI":"10.1145\/321250.321253"},{"key":"6166_CR4","doi-asserted-by":"crossref","unstructured":"Graf, P., Substitution Tree Indexing, Proc. 6th Int. Conf. on Rewriting Techniques and Applications, 1995, pp. 117\u2013131.","DOI":"10.1007\/3-540-59200-8_52"},{"key":"6166_CR5","volume-title":"Technical Note no.473","author":"M. Stickel","year":"1989","unstructured":"Stickel, M., The Path-Indexing Method for Indexing Terms, Technical Note no.473, Artificial Intelligence Center, SRI International, Menlo Park, US, 1989."},{"key":"6166_CR6","first-page":"102","volume":"13","author":"E.A. Cherkashin","year":"2008","unstructured":"Cherkashin, E.A., Splittable Data Structures in System of Automatic Theorem Proving KVANT\/3, Vych. Tekhnol., 2008, vol. 13, pp. 102\u2013107.","journal-title":"Vych. Tekhnol."},{"issue":"2","key":"6166_CR7","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W.W. McCune","year":"1992","unstructured":"McCune, W.W., Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval, J. Autom. Reasoning, 1992, vol. 9, no. 2, pp. 147\u2013167.","journal-title":"J. Autom. Reasoning"},{"key":"6166_CR8","volume-title":"Prikladnye algoritmy v diskretnom analize: sb. nauch. tr.","author":"A.V. Davydov","year":"2008","unstructured":"Davydov, A.V., The Calculus of Positively Constructed Formulae with Functional Symbols, in Prikladnye algoritmy v diskretnom analize: sb. nauch. tr., (Applied Algorithms in Discrete Analysis. Collection of Scientific papers), Korol\u2019kov, Yu.D., Ed., Irkutsk: Irkutsk. Gos. Univ., 2008."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411611070054.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411611070054","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411611070054","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411611070054.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T21:57:17Z","timestamp":1773611837000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411611070054"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12]]},"references-count":8,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2011,12]]}},"alternative-id":["6166"],"URL":"https:\/\/doi.org\/10.3103\/s0146411611070054","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,12]]},"assertion":[{"value":"18 October 2010","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 January 2012","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}