{"entities":{"Q429591":{"pageid":431358,"ns":120,"title":"Item:Q429591","lastrevid":61773429,"modified":"2026-04-11T01:33:44Z","type":"item","id":"Q429591","labels":{"en":{"language":"en","value":"Incremental variable splitting"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6048192"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$5F9BF71F-D1A6-45B3-A1E3-41E90693B56E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d397ff604345d58fdc7ba01de9406da0955e5ddb","datavalue":{"value":{"text":"Incremental variable splitting","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q429591$E96CEEF6-C8F3-4316-97A3-F403C9CE786E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b197be790537bb6cf644dcc29affb3ee4b12de88","datavalue":{"value":"1266.03023","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q429591$927E1BF7-56BE-483F-8175-CCDCBB0E16BA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"286a1e1b841f1519bfb322646f84a7383b08063c","datavalue":{"value":{"entity-type":"item","numeric-id":429587,"id":"Q429587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$8CA1614A-F74F-4DC9-B49E-CB90332C13A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f38528512dff7c891b5663c62e7395ccfc785a83","datavalue":{"value":{"entity-type":"item","numeric-id":429588,"id":"Q429588"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$D484E711-71DF-4DD2-98EE-A89B47FCAC23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5df924d051f54b4edc39c13db0d8832fba30377e","datavalue":{"value":{"entity-type":"item","numeric-id":429589,"id":"Q429589"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$50E91B04-2804-4231-9761-C05BF122DFED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fc43334de395ad582a62ad990c60c53a86ecfe8f","datavalue":{"value":{"entity-type":"item","numeric-id":429590,"id":"Q429590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$E4F7FD28-6B36-4C02-9C5D-0E14F71DB4FB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$DF3176E7-CD71-4A6F-B51B-B2910898CC2A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f318557c66fd6d7ed4e56cf07066ee7032aec4a0","datavalue":{"value":{"time":"+2012-06-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q429591$B08C571C-5987-448C-AE7A-AE7883DA4BE8","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"895d5fc798d777f77a43df1e1b11857e28584cdd","datavalue":{"value":{"entity-type":"item","numeric-id":592080,"id":"Q592080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$17826704-AD50-4DCC-B30E-2B8A85A591C7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q429591$4CDBBE90-3B81-498E-A35C-281D59427717","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q429591$1C353390-3E84-4A12-ACCB-F15320794535","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c79f50f87e0c59449243b7e1d63a92b4f8a2c63b","datavalue":{"value":"6048192","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q429591$C86870D0-3B24-4DAF-AF75-E1F8198D9B00","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q429591$1268BA1F-2B7B-44EF-A511-0CEDC354AFB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"45ba0550e07e04a3326d1cb7dbe398ac3d7c209d","datavalue":{"value":"tableaux","type":"string"},"datatype":"string"},"type":"statement","id":"Q429591$70617319-595E-498C-BAEF-A1CA5003C6A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"456c8ab6cb059b66495728c609fbcbde72b2d22f","datavalue":{"value":"incremental closure","type":"string"},"datatype":"string"},"type":"statement","id":"Q429591$1D144B29-E8DA-4CC0-9B08-9685E11D7D51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e326d3386967640031d129bba72118f715d65302","datavalue":{"value":"variable splitting","type":"string"},"datatype":"string"},"type":"statement","id":"Q429591$B69B9B71-5E7D-4AB4-A567-E753ED9C67CD","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$32E5B7AA-14EF-4E0D-B615-C6BEBB7D7DBC","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$46B9E675-8C55-43FF-AAAD-7D1E7BCBB3BD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ed2b0da84e7f98df70210eb192ee7afb57a84afc","datavalue":{"value":"https://doi.org/10.1016/j.jsc.2011.12.032","type":"string"},"datatype":"url"},"type":"statement","id":"Q429591$37D13E04-F3BB-487E-8735-567236F53810","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fff2604b7e29b33ed9faaa4956065b9f2ab3ed7e","datavalue":{"value":"W1998457088","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q429591$2E2F128C-4DB8-49A7-B670-D0E2784BECF9","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"569a99853be0b332a9c966c8585f47b516e2d811","datavalue":{"value":{"entity-type":"item","numeric-id":5479267,"id":"Q5479267"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$0BCEA53D-E421-499F-A891-69451B7DA0AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d62ceab5ff2c6c9158c5feebe26fb307387e8861","datavalue":{"value":{"entity-type":"item","numeric-id":3608770,"id":"Q3608770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$E8A8DD1A-C7AF-4675-988F-A3378C96A97E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"45107b9470fcc9d21eee7884b1b56bba5b3073b2","datavalue":{"value":{"entity-type":"item","numeric-id":877894,"id":"Q877894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$E1C96C62-89D9-461A-A81B-25F78CC6D0A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"29abb5a7232f6e8dd451e3b515a2566e5399de3c","datavalue":{"value":{"entity-type":"item","numeric-id":4282596,"id":"Q4282596"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$F7665088-557E-40A3-8719-7675741E76D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dbb4aa8dad638334a86cbf0de6c1439e4250b0ce","datavalue":{"value":{"entity-type":"item","numeric-id":4692618,"id":"Q4692618"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$FF604D7C-3F24-45D6-9C4C-FFCB40FC429E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54f43ba0602b4cd1c084d968b0e23d7b8d967cdd","datavalue":{"value":{"entity-type":"item","numeric-id":2762629,"id":"Q2762629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$6C5C1B29-EEFE-4AC2-A7BE-9BAD5D4F3E4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ad2e3e71fd34316c4d5dca241131f17edc1acca","datavalue":{"value":{"entity-type":"item","numeric-id":4863622,"id":"Q4863622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$F2398F64-DA5F-4AE4-9F6B-7C3E9E3CEF0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f33c7e2fc71303fd900c50bc37fd6728d3f12f3","datavalue":{"value":{"entity-type":"item","numeric-id":4539640,"id":"Q4539640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$F116D46B-27C8-4247-8515-394248725F81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8918b138e0301b7fb7013f51e3914c9e9e6a4da4","datavalue":{"value":{"entity-type":"item","numeric-id":1344882,"id":"Q1344882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$AB447D6F-C9E0-4696-90CD-586D76A857A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dffc16544718d83a4fdaaf484258616599c048b4","datavalue":{"value":{"entity-type":"item","numeric-id":4520768,"id":"Q4520768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$6E0B7BCC-24E8-4015-B98D-B13CA87A80A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"565b160089cdc5b3036b02090a5d1494987eb47d","datavalue":{"value":{"entity-type":"item","numeric-id":3010371,"id":"Q3010371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$E35C2E8F-1F0D-4564-9FDA-48DBB4923C2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"febba330446bda559f2952d624c63d67c91597ef","datavalue":{"value":{"entity-type":"item","numeric-id":5560258,"id":"Q5560258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$C371ABC0-DCC4-4254-9BBC-1555CCFA777C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16c58bccac3eb8e167d77acc1c92ca853e7a5fcc","datavalue":{"value":{"entity-type":"item","numeric-id":2655326,"id":"Q2655326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$FE168D64-0126-40E4-8ED8-0A11286A009B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"079d26960fbad67a47fb78241cb8cbf2b682033c","datavalue":{"value":{"entity-type":"item","numeric-id":3999539,"id":"Q3999539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q429591$913EE735-0986-41BE-ABF8-14E24E01C5A9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1b02dea362e35fbd3fc7de5be0ccd0c21039ac0c","datavalue":{"value":"10.1016/J.JSC.2011.12.032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q429591$477B0512-C16C-4B12-B18B-254AC0450C0F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"845ae4510db3b57cb14c275f85c261d76fe24a9d","datavalue":{"value":"The main contribution of this paper is to adapt the incremental closure framework for free variables to variable splitting tableaux.NEWLINENEWLINEThe variable splitting method for free-variable tableau calculi provides an admissibility condition under which the same free variables can be assigned values independently on different branches. While this can be very useful for automated proof search, a direct implementation of this condition is impractical.NEWLINENEWLINEIn this paper it is shown how the incremental closure approach can be extended to provide an incremental, and therefore tractable, evaluation of the global closure criterion of the variable splitting calculus. The admissibility condition for closing substitutions is expressed as a constraint satisfaction problem. This allows one to devise a mechanism which checks the existence of an admissible closing substitution incrementally, during the construction of a proof. A rule-based algorithm for testing satisfiability of constraints that accounts for split variables is specified. Experimental results -- based on a prototype variable splitting theorem prover implemented in Java -- are provided.","type":"string"},"datatype":"string"},"type":"statement","id":"Q429591$433A9BE3-2340-4B09-A3B3-F8A3D6EFADE7","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4bded643ae6751a387a21154075af5631e592d3a","datavalue":{"value":{"entity-type":"item","numeric-id":877894,"id":"Q877894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"075bf70572f5bc06814a086043db19802dfe3ac9","datavalue":{"value":{"amount":"+0.8636692762374878","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q429591$9CAF04DB-28EE-4EAC-A83C-45F1733DD50E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6acd4fc550178d64221bcd100aa84d03046c3234","datavalue":{"value":{"entity-type":"item","numeric-id":5187869,"id":"Q5187869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1bd9badc37fc57a5651ad4d5211fdc4b7d5371dc","datavalue":{"value":{"amount":"+0.7893269062042236","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q429591$1EA58AC2-326D-470A-9AE1-E28C5207E6DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4066116d16c7984b60dd9a8ca8526524f0f98c05","datavalue":{"value":{"entity-type":"item","numeric-id":5479267,"id":"Q5479267"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"655f3a5b737187cf1eb5fd31a9dba7eb93c70024","datavalue":{"value":{"amount":"+0.7672387361526489","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q429591$C5AC1746-1C66-4CDE-BB07-ABFBA71075CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2c16fdd5ea0a8e5a4024d53122320d331b1e5fec","datavalue":{"value":{"entity-type":"item","numeric-id":4928460,"id":"Q4928460"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a8812ea84575224933ce59bc88241dc25781b261","datavalue":{"value":{"amount":"+0.7550187110900879","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q429591$46A25EB8-3E9A-4AF3-B717-AD31DDF3FB80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1d683ef670cfe0396ca25a3659cc0c6554128d7","datavalue":{"value":{"entity-type":"item","numeric-id":4539640,"id":"Q4539640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6f78311f54727ec25eb70cd71cb9829a71e443d4","datavalue":{"value":{"amount":"+0.7482309341430664","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q429591$40739624-4A33-4588-8F39-FF00357761CF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Incremental variable splitting","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Incremental_variable_splitting"}}}}}