{"entities":{"Q802317":{"pageid":804165,"ns":120,"title":"Item:Q802317","lastrevid":64486623,"modified":"2026-04-11T20:12:44Z","type":"item","id":"Q802317","labels":{"en":{"language":"en","value":"Refutational theorem proving using term-rewriting systems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3890764"}},"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":"Q802317$7576EDCC-9DCF-4FB7-B310-5C6B3F663864","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2757aec707732290422672bb87ce9b53e054afdf","datavalue":{"value":{"text":"Refutational theorem proving using term-rewriting systems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q802317$08473C3A-90B6-47EC-8613-F5C6F277ADB2","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"387be85e0011b5cd75855206157f25094a7e5009","datavalue":{"value":"0558.68072","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q802317$020BBAF9-8A23-44B1-8CBF-B3FDCDEE0E03","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"509525d3e1777909773b9e943155ec092581a079","datavalue":{"value":"10.1016/0004-3702(85)90074-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q802317$112F233D-EBAC-4410-93FF-9B33C122B7E5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5584b61080269b096f785173ffd49061cb7d63a9","datavalue":{"value":{"entity-type":"item","numeric-id":673133,"id":"Q673133"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$A175824E-3ECB-400F-98DD-BA369D552B4D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"984e6510ec40a363d20e607cce2cc2f8b07918ae","datavalue":{"value":{"entity-type":"item","numeric-id":72340,"id":"Q72340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$3B16A77C-7D6C-42CE-9117-39B4F9B3D040","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3c94df5c9af0ede578c52141befd29044de13172","datavalue":{"value":{"time":"+1985-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q802317$B7381E18-AF76-4F17-9587-13E1EC82121A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"47d0b16ab21c9aa00f76cbbc6070d57c11d33e94","datavalue":{"value":"http://ntur.lib.ntu.edu.tw/bitstream/246246/118462/-1/20.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q802317$A8C311A9-2B1B-4EEE-A187-7B2D5641051B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"edb70de29a647b507b9737d509e89a59fb6c475c","datavalue":{"value":"The paper proposes a new approach to theorem proving in first-order logic based on term-rewriting systems. First, for propositional calculus a canonical term-rewriting system for Boolean algebra is introduced. The key point enabling successful construction of the canonical term- rewriting system (in contrast with all the previous attempts that failed due to the fact that the prime implicant representation of Boolean terms is not unique) consists in choosing exclusive or instead of or. The canonical system for Boolean algebra enables transformation of the first- order calculus into a form of equational logic and to develop several complete strategies (both clausal and nonclausal) for first-order theories based on the Knuth-Bendix completion algorithm. These strategies deal with predicate logic and built-in (equational) theories in a uniform and quite efficient way.    Comparison of implementation of a theorem prover based on term-rewriting with other theorem provers based on locking reduction or natural deduction shows that the method proposed is in general much more efficient then the methods based on resolution. Great efficiency and easy modifiability of a theorem prover based on the term-rewriting method makes the method a serious counterpart to resolution and it will probably have significant impact on theorem proving.","type":"string"},"datatype":"string"},"type":"statement","id":"Q802317$CA973AE7-17D9-4958-A070-98FD1E562ECB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q802317$B2200AE3-942E-431F-985A-F6E0B2BFFDEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"13841f0b96793f178ce9a7dcac9f232220625aee","datavalue":{"value":"03B30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q802317$5CF77D0C-7DD7-4755-9266-B546CD8D9602","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q802317$1C9D14D5-D5BF-453B-92CA-CB89E3381F51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c06e0874e30722381d620ef69fb36c407a01cb04","datavalue":{"value":"03B10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q802317$F06B9071-013C-4D81-B29E-CC723866E42C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ac7dbdc6439da3df4db829af9393786bef4c8ea7","datavalue":{"value":"06E20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q802317$F160A863-937D-466C-8637-7A74B55F0C25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c2c1bc14cfdc7229fee5c71b5c4e5c4888c771b2","datavalue":{"value":"08A50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q802317$64740549-A758-4E65-9B10-1BC3200AE316","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6fbf677f70fdc0126e61aaeed7a99756c9f2ce89","datavalue":{"value":"3890764","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q802317$1E0DA967-C5D7-48AE-B8B5-419166E9B584","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2e80a7123e4ea6d0418cb24d37b1837f13e3514","datavalue":{"value":"first-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q802317$6B10BB89-BBB6-4011-908A-0CE60E6436A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0b79c0d46aaed6ae08d529961c9f16b783e44803","datavalue":{"value":"Boolean algebra","type":"string"},"datatype":"string"},"type":"statement","id":"Q802317$0CA5D8F1-0B44-4C0C-AB4B-CB90AF1A425D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"744fd5f6b592344bd2a87ac1816bb7847861172e","datavalue":{"value":"equational logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q802317$D64FC52C-394B-4A21-B45A-11CC59D21202","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"f44a9da04c992cb9b4dcf5d40b88ac5ae56ad1d5","datavalue":{"value":"Q56039144","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q802317$2648D55C-B201-4C7F-AFD0-6A41F149E5B8","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"828dfc38786d2049fd79af4c315ff0a16e6bc429","datavalue":{"value":{"entity-type":"item","numeric-id":1188836,"id":"Q1188836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$16BD5B00-E616-4421-83EE-35C3AF184693","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cdc09159c3d9e35e53ef549059a47b095580c647","datavalue":{"value":{"entity-type":"item","numeric-id":40621,"id":"Q40621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$D01E891B-FBAA-4EFE-9AF2-02EDBCDA74AB","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":"Q802317$D34C56E9-2CA3-4761-B10D-634A6B9C29DC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c0db1b363fb82419cd08f0154b4106655dc619e3","datavalue":{"value":"W2019751493","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q802317$D8DB55D2-6062-4326-BD81-9AA2230BB516","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e857e95d91a8e9f3746c9aca423c534197fa21d","datavalue":{"value":{"entity-type":"item","numeric-id":1238434,"id":"Q1238434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$0586DDAE-1BEC-4880-AAC8-D04AD0D9C6BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4fb53dc30cdc46111c93a6e7de143f2e9b39160","datavalue":{"value":{"entity-type":"item","numeric-id":4099229,"id":"Q4099229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$A0929404-4491-4725-A7BB-14289841948B","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":"Q802317$D2AE8FF0-AF42-47D6-936F-D9C82160A7D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef757ecac8e00102e8fe2d81d7657ee3391ff698","datavalue":{"value":{"entity-type":"item","numeric-id":4138187,"id":"Q4138187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$47776A6D-322B-48AA-8275-078FAF1DE428","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"378088a63ec20245823db74d6a8845609e39ce21","datavalue":{"value":{"entity-type":"item","numeric-id":593789,"id":"Q593789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$FFBC8509-E82A-4C01-82F5-C062534E1C92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"052186b747d379b95536dd183092a6d28a9a4c59","datavalue":{"value":{"entity-type":"item","numeric-id":3338216,"id":"Q3338216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$AE11B90D-2F75-4B46-A0CF-B79228F168F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7dd076536f3668f703f8f8e17b2cfee8106654e","datavalue":{"value":{"entity-type":"item","numeric-id":1154801,"id":"Q1154801"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$2D5E3557-D25A-4E8F-BDD4-07834CF3125F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e9acb750b5a1fcf5fe08b591fc6df182dd9e5e0","datavalue":{"value":{"entity-type":"item","numeric-id":3883561,"id":"Q3883561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$F142A119-5E4A-4F88-9E68-48D7341195F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"89e6b612eb3cb0e65ff83e8cd8762940dc520785","datavalue":{"value":{"entity-type":"item","numeric-id":3659124,"id":"Q3659124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$DACA1FB8-27E6-472E-93A8-82CD131050E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"849241baa6b3c56591969b2586e51dae90f667cf","datavalue":{"value":{"entity-type":"item","numeric-id":3816048,"id":"Q3816048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$1ACD46B8-68E3-4918-AF7D-97CD6B249937","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cae74153e0f085b8cfa1b39a51e5c7aa9c26c82d","datavalue":{"value":{"entity-type":"item","numeric-id":3338225,"id":"Q3338225"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$FDCE3CAB-8E2F-4D86-A260-916D735AFB54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1e0b4fc54e8c62a86959e50d4b1b27d9d9a092c","datavalue":{"value":{"entity-type":"item","numeric-id":5581665,"id":"Q5581665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$B0CC0B30-2457-4DF7-AFD0-AAAC3642D5DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f09c8478424162622e2e11cbade44966513eb5d","datavalue":{"value":{"entity-type":"item","numeric-id":5621960,"id":"Q5621960"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$ECCE077D-D8A7-4791-8C75-C782DF107311","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e57dada08276bdfd975413149fdc809775588d67","datavalue":{"value":{"entity-type":"item","numeric-id":1147232,"id":"Q1147232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$5D71F3E0-4366-4414-8FCC-7D749B3461A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"914ef8719678eb4ee59028ba65b4741c8aa1bc8e","datavalue":{"value":{"entity-type":"item","numeric-id":4124327,"id":"Q4124327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$9B3C7E45-6F19-4D80-AEFE-C4D445D71A06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8670a1cb5138f59a7607a06c6c33e9eef7f2c9ea","datavalue":{"value":{"entity-type":"item","numeric-id":3938536,"id":"Q3938536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$A625E752-362D-409D-8DF7-346699B497DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0001ddf29143e230db9061e7c9cfd72aed8db985","datavalue":{"value":{"entity-type":"item","numeric-id":1170894,"id":"Q1170894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$0BB1A94C-FC12-47A4-B07E-CBB255056B6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10514d04294539f6b18e653ffed15729ce3e519b","datavalue":{"value":{"entity-type":"item","numeric-id":5678447,"id":"Q5678447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$8B4A11FE-7CAF-4AA7-A79A-72C1EFB6322D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"adbfa02ab4b7e0bb252f5a5604936a94deac79e9","datavalue":{"value":{"entity-type":"item","numeric-id":3847756,"id":"Q3847756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$3E391755-ADA3-4537-A307-9CB6B4445A34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$FA43A77A-24BF-45CA-A605-A8304AEF9A52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3e169af1b2927cc066a8cc188c6dd43f7cce9298","datavalue":{"value":{"entity-type":"item","numeric-id":5591533,"id":"Q5591533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$15BE8DA9-1718-44E2-A828-F86BA388469B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65a7d163034968b8b573af486389b73d9c031e2e","datavalue":{"value":{"entity-type":"item","numeric-id":3707399,"id":"Q3707399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$43627BE1-1DD9-424B-929C-41456970B8FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aebb937bb36aec0ca90e44ba3165ce327e365d7e","datavalue":{"value":{"entity-type":"item","numeric-id":3214440,"id":"Q3214440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$14D81EA7-991D-49D0-BB0D-3681EE18B45C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"031d93ba0f0d59696b935bd9707e0c0dc3b5aa4f","datavalue":{"value":{"entity-type":"item","numeric-id":4050191,"id":"Q4050191"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$1DC1C659-A1B5-44FE-AD56-C8B9999B80A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1669261077901413d76dc0f7072dfdae93141a3b","datavalue":{"value":{"entity-type":"item","numeric-id":3912070,"id":"Q3912070"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$52FB850D-7557-48BD-902D-22E2BB5915C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f6ad112ebffaa9a776bbfff7378f1f9e15f848a","datavalue":{"value":{"entity-type":"item","numeric-id":3905286,"id":"Q3905286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$B506AF6A-E745-457A-AC7A-66CF65D25FF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27e2d761ccb0b052ed932a9e25e1934d9433dace","datavalue":{"value":{"entity-type":"item","numeric-id":3745825,"id":"Q3745825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q802317$A9A86EC1-590D-4C40-B741-B9BB6B8BA043","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cbd992a4ea49d90c3a3d4107b2bd75678de75673","datavalue":{"value":{"entity-type":"item","numeric-id":3703311,"id":"Q3703311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f7d2011457fc48a4372229c4cd1b0992b9e510af","datavalue":{"value":{"amount":"+0.872933030128479","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":"Q802317$85E25F48-E4F4-47B5-AADC-FA57C574321F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"05e0ae67cdbc70bd6bbf9d5c308e1a1c2edd6844","datavalue":{"value":{"entity-type":"item","numeric-id":757071,"id":"Q757071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb4cc00ce44433e30b20b9657c10d70b74913950","datavalue":{"value":{"amount":"+0.83173006772995","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":"Q802317$99CCA7D7-5E9C-48B3-8146-1871C4BFFEFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8f1c70ed659205385e458fe3a28df7787e8c7705","datavalue":{"value":{"entity-type":"item","numeric-id":3805956,"id":"Q3805956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"254244f4fe5831ceb97dcd84f443134265fd5187","datavalue":{"value":{"amount":"+0.8312833905220032","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":"Q802317$FAA06F0D-21FB-415F-B0BE-381536B4F393","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5079de2b33777a53071eb4a1f8e4e5ae8a87c664","datavalue":{"value":{"entity-type":"item","numeric-id":5881190,"id":"Q5881190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2d465798e2f76b43e47b755f752e2b92080e4385","datavalue":{"value":{"amount":"+0.8226960301399231","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":"Q802317$8A3BAABE-21D0-42D5-8488-FBA0F47BD5E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a53d408684bc2b1b88fdd4e98d3b61a6b8ac3ab8","datavalue":{"value":{"entity-type":"item","numeric-id":3352542,"id":"Q3352542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f522cb1473648507b78dbf01909f15852776309d","datavalue":{"value":{"amount":"+0.8188787698745728","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":"Q802317$241FC566-C248-4F85-9F67-992744039F18","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Refutational theorem proving using term-rewriting systems","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Refutational_theorem_proving_using_term-rewriting_systems"}}}}}