{"entities":{"Q2785673":{"pageid":2796411,"ns":120,"title":"Item:Q2785673","lastrevid":47422369,"modified":"2026-01-01T17:09:08Z","type":"item","id":"Q2785673","labels":{"en":{"language":"en","value":"A-ordered tableaux"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 981818"}},"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":"Q2785673$18605AFB-6BCB-4C66-AFBF-B9675240A4A8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d06c86d4585318b723679c475ea7e4ea957d679d","datavalue":{"value":{"text":"A-ordered tableaux","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2785673$020F849B-F54E-4199-A87F-F6255029B22B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"83eb8367b10bf24c57d44eb00404156618f7fea6","datavalue":{"value":"0878.68110","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785673$35000BC9-3437-410D-A0D8-3591F732CA35","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7743279316f8ce0cdbb2e6d0842ac12b618ecbfa","datavalue":{"value":{"entity-type":"item","numeric-id":679246,"id":"Q679246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2785673$55B7CA12-D8A3-4754-8DB8-D541FE89F9F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a26166767a0ac443728404500e3c49feea585435","datavalue":{"value":{"entity-type":"item","numeric-id":2785672,"id":"Q2785672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2785673$35EF1F15-E163-4CC6-9368-108601269DA2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7e2dfb5d8700e631835334f9dc71e9b98ed5a53b","datavalue":{"value":{"time":"+1997-12-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2785673$CAD062CF-0F60-4E9B-8C5B-9BB73D67259C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3db1d14d27306035b001e030104eebb648df1623","datavalue":{"value":"https://semanticscholar.org/paper/87d0cca7df060daeb39119fd58278b604ce2de20","type":"string"},"datatype":"url"},"type":"statement","id":"Q2785673$75F94394-17D7-4A39-A81B-39626EDA25FD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785673$0C23E1EA-9BCC-4CB2-AB13-A2720D12419A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785673$BE450E2C-29A0-4209-9743-E3984041B285","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e61d1163606264f12b73ae219347172922eaa4e0","datavalue":{"value":"981818","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785673$39ED1E54-562B-4510-A256-7A63F3C9CDE9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"79990f5a133019dda4068781d3e7e96e9da9a400","datavalue":{"value":"A-orderings","type":"string"},"datatype":"string"},"type":"statement","id":"Q2785673$939EDBC6-E0C3-4174-B81C-7165F4C88B47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3c389b25212b5e7ff418a01048925abdf7a6f476","datavalue":{"value":"ground clause tableaux","type":"string"},"datatype":"string"},"type":"statement","id":"Q2785673$1F87BCFB-DA3B-4C6B-87EC-5887C3D0FECF","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":"Q2785673$BEEAA984-9A9E-40CB-9D63-5E7A36EF1950","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3eb1675747a303823c843d4649e1375e05dff3a9","datavalue":{"value":"W2118483827","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785673$00133FD6-19CE-4EEF-A0A1-630237B1525A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5f07d63c35f0f3092cc533d64d8b8fd6ec85aca7","datavalue":{"value":"10.1093/LOGCOM/6.6.819","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785673$8DAE2FB4-262F-439E-BB2D-DC3E52FDE594","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4e284497c1d95ed03031b32369f55bf404c9e002","datavalue":{"value":{"entity-type":"item","numeric-id":6768690,"id":"Q6768690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2785673$8FB398EE-E5B6-469E-98F1-95410253338E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8b9082e16a3375d287c7c377b6f177c6fcaade94","datavalue":{"value":"The main result of the paper is an extension of the resolution proof procedure based on A-orderings of literals (i.e., strict partial orderings respecting substitutions) to the tableau proof procedure. The authors give a simple completeness proof for A-ordered ground clause tableaux and then extend this technique to non-ground non-clausal formulas in the negation normal form by proving completeness of an A-ordered tableau procedure. It is noted that this procedure is not compatible with the connection method.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2785673$45300898-B822-4C6D-B141-AE0F35FB41CD","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"603f9ee8942cd3c164aaecde91e2743415201170","datavalue":{"value":{"entity-type":"item","numeric-id":1181481,"id":"Q1181481"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2785673$F12ADC6B-F989-4241-9B18-9CEAB29519A1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"54561236c3490b393112b0740cee6dbc40fe607a","datavalue":{"value":{"entity-type":"item","numeric-id":5210807,"id":"Q5210807"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0d5cb2b7f9a5776c85cb0306f9891143abe8ca36","datavalue":{"value":{"amount":"+0.8354475498199463","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":"Q2785673$2977B95A-927F-4047-AF36-38D01D2476DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3e5dc85744a58895b351d6c7f27ac3cdc3127642","datavalue":{"value":{"entity-type":"item","numeric-id":4610325,"id":"Q4610325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea3f39ee66f98183820155ec64c33a7567876517","datavalue":{"value":{"amount":"+0.8244775533676147","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":"Q2785673$C69F4393-89DD-4006-BB18-ED270ABC6199","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1376cc4d0d342d5e6ec6fc0ff12814b9a536361b","datavalue":{"value":{"entity-type":"item","numeric-id":1869611,"id":"Q1869611"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"89b51d5820d6ac7ddcbf441840608cc7547a5d73","datavalue":{"value":{"amount":"+0.7908986806869507","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":"Q2785673$A4DA0781-FF4D-435C-86F5-9BA758397833","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f67cf830e08fb9dd462bb8a64126e0aefb31f39b","datavalue":{"value":{"entity-type":"item","numeric-id":5434490,"id":"Q5434490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7afcf908166e7bee461c1cb2dd23c6e292dc0d5b","datavalue":{"value":{"amount":"+0.7848246693611145","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":"Q2785673$70FC488F-A38D-4F24-A111-1AB74750FFB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb4427de8d7fe4878160de2cbb9b24c5d18922ed","datavalue":{"value":{"entity-type":"item","numeric-id":4537439,"id":"Q4537439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fc9b09cfb29d1206b457690ae8373ca8bf30e4b9","datavalue":{"value":{"amount":"+0.7798165082931519","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":"Q2785673$326D6B6C-4447-407A-A598-BA32FBB9CE59","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2785673","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2785673"}}}}}