{"entities":{"Q2987065":{"pageid":2997789,"ns":120,"title":"Item:Q2987065","lastrevid":85742828,"modified":"2026-06-03T11:20:54Z","type":"item","id":"Q2987065","labels":{"en":{"language":"en","value":"A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6718430"}},"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":"Q2987065$CD3267E9-24C8-4797-BABD-059712B727E8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"73bdaa35e9d67aed748eda2ca9380324067adaa4","datavalue":{"value":{"text":"A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2987065$5511C096-F253-4B33-9450-DAFB2E35E1E1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"69f820004fdd794291d473cfca95cb34db3dd265","datavalue":{"value":"1361.68191","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2987065$12819FA4-25A8-44DC-B5D9-6389E7BB6DC0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"dbb66b347a8501d3e88bb4fc6db185a6021261a5","datavalue":{"value":{"entity-type":"item","numeric-id":167063,"id":"Q167063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2987065$FEC7273F-0F93-4498-9FDC-5E82CC56EC81","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"41be8a7ccb30ef6453be136c830247d17a0d171d","datavalue":{"value":{"time":"+2017-05-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2987065$F0D07A0E-F541-4F39-8297-624B332CB0BB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2987065$92951656-004E-479C-99D5-437008F5ED43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2987065$38D9E5B1-B2B5-4BC1-AF4A-6F09E0F9D645","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4534ad0477ad51517810ee5a31b6c88a5bd7c6d7","datavalue":{"value":"6718430","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2987065$DE9A93B7-0CE0-4A76-BAD3-090C3BD51FE5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2987065$F94C7ED9-71BC-4763-A59B-316EE5992179","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fa8a6101ff90bea77f851517b5a991ddcaf7286b","datavalue":{"value":"induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2987065$9C3B774A-76A2-4B1E-8307-882ABA2DE15D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"278ae012b8ea2374306dd75e442a10ace82830b0","datavalue":{"value":"schemas","type":"string"},"datatype":"string"},"type":"statement","id":"Q2987065$19B4043B-222E-4754-95E6-77D6F5DB1C55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5f84bfa4d35417b90f2a3d3973763cb89a42b0a1","datavalue":{"value":"paramodulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2987065$963996B7-D055-4FE1-9F30-4F36031D2700","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q2987065$7D82CE48-DDBC-422D-B341-9AF0AF99251C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"45702294177a39ee1ff9766c01d5d14dfb7896ef","datavalue":{"value":{"entity-type":"item","numeric-id":21425,"id":"Q21425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2987065$6BA8178B-5589-42D9-BB99-4777640AD5BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"82659ddd3b24a7f3c51a78eb5f25cc1e5d64df69","datavalue":{"value":{"entity-type":"item","numeric-id":17116,"id":"Q17116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2987065$3D68BFBB-DEF6-4712-95FA-93A2345E4EB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2987065$EE6F9A68-03BA-40CF-B88D-BAC3D3FE3CEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2207b0b201a95a431b254bcb1c01d869b9f41774","datavalue":{"value":{"entity-type":"item","numeric-id":18972,"id":"Q18972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2987065$6FDA5094-291A-4A9F-B4D6-C2F15E983FA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4eaad22b53ac96a08ad4d9f23a8db15f0cac4909","datavalue":{"value":{"entity-type":"item","numeric-id":32156,"id":"Q32156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2987065$34F69D59-AB53-49AF-93A8-21C402D3EEDE","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":"Q2987065$B421EBE1-0561-4E11-A039-FEA20BD52C98","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"61aafcc218f60482d4ba54b0e06f72e9f4f10551","datavalue":{"value":"https://doi.org/10.1093/logcom/exu078","type":"string"},"datatype":"url"},"type":"statement","id":"Q2987065$615D9C16-4B4C-411E-9B01-07554CA313B5","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5692adac7a9414addf4a3d44bfdfe76284ad549e","datavalue":{"value":"W4298955360","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2987065$AD0F7742-ED41-41E6-8BD0-B9031558B8CB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5daa7e97c45d97bc0b527c4a031fa6c6067d5ddd","datavalue":{"value":"10.1093/LOGCOM/EXU078","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2987065$5466C1CB-535B-47BD-91B6-4C14D180A739","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"9e6aedf3faf6964e0bbb1663882629f007284aa9","datavalue":{"value":{"entity-type":"item","numeric-id":2983390,"id":"Q2983390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2987065$76CCC1DB-A71E-49B8-8280-DA743F0A7243","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad2f8835ae0fa3bf52a8d1292f900f4719c491cc","datavalue":{"value":{"entity-type":"item","numeric-id":5403072,"id":"Q5403072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea1472dcf6d9776742a156ba880f5a95d9255380","datavalue":{"value":{"amount":"+0.84552276","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":"Q2987065$1ADD0198-FF4D-4197-B028-7F7607F36953","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0c8d3eb1a93bb447ee0cb2be30b8c24f2037cbe7","datavalue":{"value":{"entity-type":"item","numeric-id":3992233,"id":"Q3992233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"287a8915e45872d88ade11ef1709465f1ae6eac0","datavalue":{"value":{"amount":"+0.8412648","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":"Q2987065$64983D84-643B-40CF-83D9-CD20776E2747","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"296ba906405e57bb87f80c49aa12025f6804ee53","datavalue":{"value":{"entity-type":"item","numeric-id":3490950,"id":"Q3490950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"287a8915e45872d88ade11ef1709465f1ae6eac0","datavalue":{"value":{"amount":"+0.8412648","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":"Q2987065$7A255DC6-8A88-4F8E-8625-1628CE2D7025","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"95ac42d60317fde4c37666f10d986c26a4eaeea0","datavalue":{"value":{"entity-type":"item","numeric-id":4452605,"id":"Q4452605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5393aa2029259999da45ac92058dbe5e365b1398","datavalue":{"value":{"amount":"+0.83745193","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":"Q2987065$34729006-C2D6-439F-90DC-E171870CB9A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a9e040b69366aa385ecb7819d5a979d92c0954fb","datavalue":{"value":{"entity-type":"item","numeric-id":3805955,"id":"Q3805955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f724e6b842dac0fc92d387c6a6cdf163f5cd94c7","datavalue":{"value":{"amount":"+0.834146","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":"Q2987065$E79BE0C5-EA04-451D-8C24-8F502E7651ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18ecbedcfe3626185d0bb331b094353198a89395","datavalue":{"value":{"entity-type":"item","numeric-id":802317,"id":"Q802317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f724e6b842dac0fc92d387c6a6cdf163f5cd94c7","datavalue":{"value":{"amount":"+0.834146","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":"Q2987065$A9FBD1BB-25C2-497B-A837-0156FBC326D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d762ba8246b4840ca1c763bc6118e4a112406c12","datavalue":{"value":{"entity-type":"item","numeric-id":4808738,"id":"Q4808738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5044ab7d3dda68ab15393af776e5ea4425808fd5","datavalue":{"value":{"amount":"+0.83070934","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":"Q2987065$532F6414-C273-478A-B65E-761A04C62BD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3df9ad27cdee70d07b6ac3a133b5637ee50502ad","datavalue":{"value":{"entity-type":"item","numeric-id":2778866,"id":"Q2778866"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"14b466a36cdc149c7cafe8819d0350a6b984a3c2","datavalue":{"value":{"amount":"+0.8306176","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":"Q2987065$01BB3AC0-74DB-40EE-AB3F-14EBA11E879E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"983cd21deef8e8804b56013c2e7cdcc132ea1307","datavalue":{"value":{"entity-type":"item","numeric-id":2722043,"id":"Q2722043"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78ac7ccf55dce7751246774befb6928f976403ad","datavalue":{"value":{"amount":"+0.8304384","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":"Q2987065$DCEC5612-8123-4B3B-B0B7-91FE22670B82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"741e144fc1ecfbf1e7224efa792e8d6928401c6f","datavalue":{"value":{"entity-type":"item","numeric-id":3009336,"id":"Q3009336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"72c34fc51767dd6b52c5931ee3a89633a483e4b4","datavalue":{"value":{"amount":"+0.82862496","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":"Q2987065$264152C2-EB4D-47C3-9A90-34C5988D9FDE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules","badges":[]}}}}}