{"entities":{"Q687165":{"pageid":689014,"ns":120,"title":"Item:Q687165","lastrevid":42641304,"modified":"2025-07-07T14:54:16Z","type":"item","id":"Q687165","labels":{"en":{"language":"en","value":"The relative complexity of analytic tableaux and SL-resolution"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 429186"}},"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":"Q687165$D8842565-D22E-47C2-A490-5E2F883A906E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9fc37741e87ef2cd4b45730bff7503b2e7cf5c48","datavalue":{"value":{"text":"The relative complexity of analytic tableaux and SL-resolution","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q687165$63C7691B-EA00-4F28-99AC-202098B96D59","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"14c6cf159eacf68729b19f8d08511baa61b3d12f","datavalue":{"value":"0801.03010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q687165$BBE9B28D-3412-4F93-9DA2-89438D408F10","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"54feb89220aa74760cc2d9daaec9bb5b441a2740","datavalue":{"value":"10.1007/BF01058395","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q687165$29C12F22-3F04-44C9-A524-F191E37F2FE4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"dbef5fbf2c22ac7944dd98f586135acfd8baf7de","datavalue":{"value":{"entity-type":"item","numeric-id":687164,"id":"Q687164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q687165$2234D086-DE46-49B0-8149-4BCF1760DD50","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e34236ca73b92c6ee0bc17431d03c3537a7f0792","datavalue":{"value":{"entity-type":"item","numeric-id":195358,"id":"Q195358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q687165$1985806A-C99B-4FFB-9908-C221B576F223","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"639e2a3a6cef7461b2fe9383e8a717703cc7a062","datavalue":{"value":{"time":"+1994-12-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q687165$08CB5B58-FEE3-48BE-B566-14B35733167B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b0540d5b74bee422b0ca0634d12ed18419468b3d","datavalue":{"value":"The paper is intended to fill in the gaps in the literature concerning the polynomial simulation relation between proof systems. Roughly, a proof system \\(B\\) p-simulates a proof system \\(A\\) if any proof \\(\\alpha\\) of a tautology \\(\\tau\\) in \\(A\\) can be transformed into a proof \\(\\beta\\) in \\(B\\) such that the length of \\(\\beta\\) is a polynomial function of the length of \\(\\alpha\\). In the paper, Smullyan's analytic tableau method for propositional calculus is extended and improved to increase its efficiency in proving theorems and analyzing the complexity of proofs. The Improved Parent Clash Restricted (IPCR) method is defined and illustrated by appropriate examples. It is shown that the IPCR method is equivalent to SL-resolution and, hence, both methods p-simulate each other.","type":"string"},"datatype":"string"},"type":"statement","id":"Q687165$138C9FB6-995C-49B4-89AB-C10686DCBD59","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q687165$3C0EA1F6-B2EE-46A7-A0B4-9CF00D2C38A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q687165$D197598E-76C3-4473-8984-4D90E7564B89","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"87e746a368b2dfeca89c824fb013c456d2acdd26","datavalue":{"value":"429186","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q687165$FD12623C-85DE-466E-B2B1-773132CE3F6E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aec01526d2d3b0a65db74199fe9fb685282baf2c","datavalue":{"value":"polynomial simulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q687165$CC071331-D5AC-4593-A6BC-8F5EA1E71AD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"14a0dd3e1b83404196449aa90cc83aae915af1cf","datavalue":{"value":"proof system","type":"string"},"datatype":"string"},"type":"statement","id":"Q687165$87D93968-8852-45F0-A9BE-60AD8497AC8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb615bec1abc44941f8beb61414c460136ebde2c","datavalue":{"value":"analytic tableau","type":"string"},"datatype":"string"},"type":"statement","id":"Q687165$5F188D36-9D47-4073-8779-65A33BDDD618","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4ee539f3c66b5148353f42975573a39b50c5340f","datavalue":{"value":"complexity of proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q687165$98BB4B48-B380-4B91-A372-15B85A3D3259","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9cdde946ec30e9e08befb17f4233d6f7dd7dbe2b","datavalue":{"value":"SL-resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q687165$F28A8EA8-8E78-4F88-8E2A-41B6FCD3F8CB","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"be2a52757c5af513b7fb2d5e98fbd88a4a770b60","datavalue":{"value":{"entity-type":"item","numeric-id":1188640,"id":"Q1188640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q687165$65DAF963-4E7E-41E9-A7E4-1DCA5ED170E0","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":"Q687165$9DCE64F1-0D1B-48E4-98C5-20E3771748F5","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b2c2b382c3725436e250ac6e5f951d42a292c14","datavalue":{"value":{"entity-type":"item","numeric-id":3954845,"id":"Q3954845"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q687165$1D837831-3210-4596-B8C8-D4E6F56887E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4735154d50c08d584a8e28202802fa9d661654","datavalue":{"value":{"entity-type":"item","numeric-id":5679729,"id":"Q5679729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q687165$23A72963-5FF6-4DC5-9AD6-E3E770264519","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b7948d2ae997be513a92df2486b836c4e1eaa12","datavalue":{"value":{"entity-type":"item","numeric-id":5667480,"id":"Q5667480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q687165$123BDD48-886A-4A51-A46B-896F5F09AE12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bea75da9fa67a5f77faa9362cd4aa6c737c792a","datavalue":{"value":{"entity-type":"item","numeric-id":4194955,"id":"Q4194955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q687165$37EB677B-BEF7-49B1-BA1E-C9E291025176","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc6482fda869c7df0ed32fd6ade8f790a1ff04cc","datavalue":{"value":{"entity-type":"item","numeric-id":5585020,"id":"Q5585020"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q687165$738BF7E7-55C3-4B34-9E9F-B4CBC6C1D052","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2dbf5d4c6cedd5848e03816494729378cde53a8e","datavalue":{"value":{"entity-type":"item","numeric-id":2551698,"id":"Q2551698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q687165$A8DBD8FA-FE0A-442B-8EBB-992D7EA0B28B","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":"Q687165$69FC57A0-B966-4DCE-A30D-438236F438A6","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"90da4d6e7f8c4b5d2db00c0f177c40e4486aef67","datavalue":{"value":{"entity-type":"item","numeric-id":5175990,"id":"Q5175990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f944d63f41da6b002a80a117ef2ba5d209792479","datavalue":{"value":{"amount":"+0.9272721","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q687165$81AA777F-E8CA-48F4-B5FB-7E645B18E740","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b00f6ab09ffac905c84a51370c4bd3759562803","datavalue":{"value":{"entity-type":"item","numeric-id":1575658,"id":"Q1575658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"696c333edf0f42b6744b34188600067d2bae0e67","datavalue":{"value":{"amount":"+0.8691416","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q687165$388EDEF4-4005-4838-8DB3-3271B1888B40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7e92ac4d002f41976de84beeecd539f246e41ae5","datavalue":{"value":{"entity-type":"item","numeric-id":1353995,"id":"Q1353995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8f98cc3b66c55dcc4673eef34650b822ee659a56","datavalue":{"value":{"amount":"+0.85523474","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q687165$56736B93-996C-43CF-B590-D4EDE466C51A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d096b94fda2a0ccefd424b9e7dc5f320dbc9f1f","datavalue":{"value":{"entity-type":"item","numeric-id":1353988,"id":"Q1353988"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3f7dbfac8d8c0938844b8c46971f0cf1e5dc9c6f","datavalue":{"value":{"amount":"+0.8424725","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q687165$1B47F84B-731C-4C12-B68F-8D6DC61A0251","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d123bbfd917a0aa883002a4d39dd29f41e715e4","datavalue":{"value":{"entity-type":"item","numeric-id":2753606,"id":"Q2753606"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"630252539c1677055b89c6c22494272c0e634c4a","datavalue":{"value":{"amount":"+0.8380037","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q687165$694167FF-4886-499C-8013-558F1E0C639A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3c95c67a73d1ac1e74977f956452be45452b2929","datavalue":{"value":{"entity-type":"item","numeric-id":1043351,"id":"Q1043351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3e597fe2c2709f59f3c580ab170c57ea6a13bc61","datavalue":{"value":{"amount":"+0.836779","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q687165$E7D33D3E-9F3F-4077-B4C7-5FF4202B0F87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4b15022e34355f7fa0b7bec63329ad827c2ff435","datavalue":{"value":{"entity-type":"item","numeric-id":2843911,"id":"Q2843911"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0b1c40dfb031f373d54c086490eab13e5599178c","datavalue":{"value":{"amount":"+0.8339939","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q687165$E012BA7C-6724-4B71-A5C9-A11DADE99DC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c9fd136eda795574c5f822efd64c7d5f118ed14f","datavalue":{"value":{"entity-type":"item","numeric-id":4696742,"id":"Q4696742"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7df47148b1c431b17afe977fcc6271491634fb2a","datavalue":{"value":{"amount":"+0.8323848","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q687165$97731B47-3405-4CB4-9530-43C4510960C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dcc3dec04d7cfddc5ca864b3bea8b672a5635ec4","datavalue":{"value":{"entity-type":"item","numeric-id":4224087,"id":"Q4224087"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"92b3083c94ff08f319285f484b442376e4f1e50a","datavalue":{"value":{"amount":"+0.82948375","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q687165$15E1848C-B3D4-4A2E-8600-4A3120ED5F48","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:687165","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:687165"}}}}}