{"entities":{"Q2908505":{"pageid":2919230,"ns":120,"title":"Item:Q2908505","lastrevid":58066077,"modified":"2026-04-03T16:20:25Z","type":"item","id":"Q2908505","labels":{"en":{"language":"en","value":"Tableaux modulo theories using superdeduction. An application to the verification of B proof rules with the Zenon automated theorem prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6076917"}},"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":"Q2908505$86FD6E8F-603D-4F89-A3D6-E496663CC1F6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"92607ea0bbb593da50d960039f3af1aa011e6359","datavalue":{"value":{"text":"Tableaux Modulo Theories Using Superdeduction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2908505$27C4601A-E1F0-4896-BCF8-9199B7F0142D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d59071b1d10f9c6406ded5886f2dbf005c4ba4c4","datavalue":{"value":"1358.68255","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2908505$F6CA692A-8701-4ED9-BA59-2D86F3CCF5C3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1da5570fbe056684d86ccfaaf14a0939c4e7fa81","datavalue":{"value":"10.1007/978-3-642-31365-3_26","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2908505$71BD523F-E327-4BB9-B0B8-0AD4400E547C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e6f0f3a64aeacf8071e0f9dbdba25c8a0eb127ea","datavalue":{"value":{"entity-type":"item","numeric-id":2908503,"id":"Q2908503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908505$75C44BF7-FC5C-449F-AF8D-CED8EF1393FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5c4c2fcb6c198441ad0b64612ab548e3aaf3782c","datavalue":{"value":{"entity-type":"item","numeric-id":2908504,"id":"Q2908504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908505$B7F8B7BF-1D91-41B6-974A-266A2E82A075","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"786f6c8f2a36da61e98b228bbd36b74e25ad6f92","datavalue":{"value":{"entity-type":"item","numeric-id":2104524,"id":"Q2104524"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908505$0715F261-2281-4077-A28B-88ECE65EB2CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f8c40e2cd3207dd1d19085f0b79e8fee7be86ced","datavalue":{"value":{"entity-type":"item","numeric-id":1624591,"id":"Q1624591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908505$91C19AA4-40A0-409E-A985-5BB76021EEC7","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3085facee3457e7f15d7356906b0165b8709b141","datavalue":{"value":{"entity-type":"item","numeric-id":2817907,"id":"Q2817907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908505$F209354F-B8CC-4079-A522-852EFCCD44A4","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"fd0374f9cee657eee67ac4dd9d79d96d1538c53a","datavalue":{"value":{"time":"+2012-09-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":"Q2908505$5C23F69D-1970-4469-8583-5E7F0793FBE9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5cc099ca0b790e2c87ba2d49e573c7ff0512a69f","datavalue":{"value":"https://arxiv.org/abs/1501.01301","type":"string"},"datatype":"url"},"type":"statement","id":"Q2908505$105D7A29-B94B-45D4-B031-E605561CA235","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2908505$1070A708-D0F2-4A59-8377-4EF045953EBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2908505$A9B96625-610D-429F-A32E-53D6C47B12CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2908505$BB3BBE9F-4661-486E-923A-F94806240A9E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4135f8c2fef765882a5ec088201fd41114c7d7e0","datavalue":{"value":"6076917","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2908505$FE887FA3-0D08-4DDD-86E2-C78352401416","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"45ba0550e07e04a3326d1cb7dbe398ac3d7c209d","datavalue":{"value":"tableaux","type":"string"},"datatype":"string"},"type":"statement","id":"Q2908505$18DE7482-BA63-4C24-88F8-B31AE799FB90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"97b7a46a360629d222476cac2c1e10d68334605a","datavalue":{"value":"superdeduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2908505$CACC5191-2CAA-4BAD-ADCF-C2C1127F6431","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"28123a0147c4696e26504aa90d2d325065e4032d","datavalue":{"value":"Zenon","type":"string"},"datatype":"string"},"type":"statement","id":"Q2908505$DACDC75C-613B-4DD6-A23A-8C780FB65C93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b36a4092864d39bf9c99c5936b3d1261e44b9950","datavalue":{"value":"set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2908505$7E08D967-2F02-4A00-9390-152D32E5C062","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ab5c99825fc3750d24a6d5e8f9dc34ef12c1bf4f","datavalue":{"value":"B method","type":"string"},"datatype":"string"},"type":"statement","id":"Q2908505$B635C4ED-E3FA-4B40-9832-D07DF322BE6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3719ed41893672db063f7cdecb5bcd68172db4a4","datavalue":{"value":"proof rules","type":"string"},"datatype":"string"},"type":"statement","id":"Q2908505$5EDF5C01-C27E-47C5-B070-9E018C4E83E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2908505$3D0503A7-E4D8-4406-8312-5D7FB9D04B8C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e3fa1be4925f6565903e34254fe3ce3cb99beabc","datavalue":{"value":{"entity-type":"item","numeric-id":18828,"id":"Q18828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908505$2B3D8977-A4F6-4207-8574-8434F07BDB04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"acd0a7f965bd7a2eea8391d50182b3fc185bc6de","datavalue":{"value":{"entity-type":"item","numeric-id":19144,"id":"Q19144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908505$BC710734-9E25-49CC-9598-AD7A639FA9E2","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":"Q2908505$8EE84848-7244-4811-906A-2C5E875BC57A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"09fe0bad35ab9fb905e90b459592f8d50149663c","datavalue":{"value":"W2949125183","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2908505$515E8457-2F7D-4897-91B8-19E3D883815A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fc21c36244ab247d119fae45e9eb4817fb00eb3d","datavalue":{"value":{"entity-type":"item","numeric-id":2870135,"id":"Q2870135"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec186fde573b5928acf3da853e31d049896a0c82","datavalue":{"value":{"amount":"+0.810484766960144","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":"Q2908505$285ADDBB-BD51-46BC-8494-6D3CC7102B5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b20eeaa6e73b5a30c13519c386169b5dc049a7a","datavalue":{"value":{"entity-type":"item","numeric-id":3498463,"id":"Q3498463"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9b245648118baafb83958c1f5c985a9103be7376","datavalue":{"value":{"amount":"+0.7786244750022888","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":"Q2908505$3B31D41B-83DA-48F4-96FE-1D33E0C76495","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"659f1715025c09fd42f29fb1a683227c1a598251","datavalue":{"value":{"entity-type":"item","numeric-id":2209546,"id":"Q2209546"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"857e6d39eb68e5c720f054f5423ae42b13ccee6a","datavalue":{"value":{"amount":"+0.7615800499916077","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":"Q2908505$9BA4C452-005B-4D1A-92E8-DD3513813B2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fcfcd51c2fbd2726dcf9a89335d8e7db15c01c4a","datavalue":{"value":{"entity-type":"item","numeric-id":3095242,"id":"Q3095242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"59e07dbcf1da6911ba1472d22614a1bfdc0f3412","datavalue":{"value":{"amount":"+0.7607758045196533","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":"Q2908505$D375E987-E036-4C5E-AE11-009E2C51B83E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"22967f8e1d8aeb6b49dc6c074f34841d779a3d48","datavalue":{"value":{"entity-type":"item","numeric-id":5307079,"id":"Q5307079"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f4430d45dcacab9b6d3cbda3cf88cd9d137d9e81","datavalue":{"value":{"amount":"+0.750223696231842","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":"Q2908505$FE2DC39D-26DB-4D11-95EC-1124BDD62239","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2908505","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2908505"}}}}}