{"entities":{"Q4015952":{"pageid":6045741,"ns":120,"title":"Item:Q4015952","lastrevid":55190023,"modified":"2026-02-04T15:02:16Z","type":"item","id":"Q4015952","labels":{"en":{"language":"en","value":"The term rewriting approach to automated theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 70121"}},"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":"Q4015952$193F6E67-4D4D-475A-B167-A7DD2E9C9BE9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"65bf9433981b9da6c621d4d4f7cf40fe1febb4fc","datavalue":{"value":{"text":"The term rewriting approach to automated theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4015952$E536B6C3-13E4-4681-AF34-F997FC5B9D09","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"72f58c4560098513ab419a738a45a14d3dd9831e","datavalue":{"value":"0754.68100","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4015952$C5BAE538-61B0-40F0-9D8C-1F8CE379DEDE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"57a1f2b79bbc454219265a77b3e4c4862707cd0b","datavalue":{"value":"10.1016/0743-1066(92)90047-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4015952$31F06F2E-1EFB-4BDB-B1B2-FB6FDAA6CB24","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":"Q4015952$7EFAD156-BF58-4F9D-A900-734DAB836E2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"318dcafa750fdebd097595276bc4d8a687f38a37","datavalue":{"value":{"entity-type":"item","numeric-id":271708,"id":"Q271708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4015952$E5D084E3-2CA0-47E7-8DAA-049C44B786CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f5fd864542907a2da8db322de1436438bd84c826","datavalue":{"value":{"entity-type":"item","numeric-id":579929,"id":"Q579929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4015952$74F59BF8-7880-42B7-9E56-A515A7F5FC3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d5450522126073beebe5b41bdc84b794c874c239","datavalue":{"value":{"entity-type":"item","numeric-id":437030,"id":"Q437030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4015952$09E6D360-E451-4E1F-A466-7ED0669C2EE8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7eb8fbff5b5a1996cd7eff3ff7a29f3a29661a8f","datavalue":{"value":{"entity-type":"item","numeric-id":3030270,"id":"Q3030270"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4015952$821612F6-16EE-442C-911C-6BAF78613B90","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b9688fba77d08b63334dc8de515e99dd360c4df1","datavalue":{"value":{"time":"+1992-11-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4015952$FC46C887-9847-4A2B-B790-68D72E5CE2FA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4015952$105DD331-1E65-4A3C-9A1A-07C315BD0841","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4015952$D2AFD32A-EDA7-40D6-9B7C-5CFB11F653ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"24aafcf24a21bd70cd3b62d3f5f72a6d0d82d816","datavalue":{"value":"68-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4015952$AB25298C-A230-4132-9EF1-EA12B35983E2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2449af0473bf2911b66a8ed96da3b1a848f6a35a","datavalue":{"value":"70121","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4015952$88B8774A-B8C7-4D64-A3A8-680FD456590E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"744fd5f6b592344bd2a87ac1816bb7847861172e","datavalue":{"value":"equational logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4015952$15A33EC4-775E-47AC-ADB2-881FE2A13945","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4befa4ca20f2beabcfa09e8a92ae13c21cb4934a","datavalue":{"value":"termination","type":"string"},"datatype":"string"},"type":"statement","id":"Q4015952$3B0013BE-F08E-4CC6-A8B0-7FA182ACB5ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"41b8ab866f2130f494e3b07bc4d1da4f4429a9e0","datavalue":{"value":"completion","type":"string"},"datatype":"string"},"type":"statement","id":"Q4015952$B06C4689-41F6-41C9-A240-151939835BDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"69c49ae5993a82349675ff861d2f7b0436bc2db5","datavalue":{"value":"inductive theorems","type":"string"},"datatype":"string"},"type":"statement","id":"Q4015952$32440A72-FBDB-42A3-891A-1CDCF6E37672","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfd627145ce1a54d764595f41fb2e8e4d193d8a5","datavalue":{"value":"equational rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q4015952$01AC422D-D4EE-4B9B-B9FF-B783676A7438","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a24053463d3d09db0bb37e1821671cf0c98e2fe7","datavalue":{"value":"equational unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q4015952$52D7473D-F737-445F-BF4C-CA9A423AAC50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"11ed6d65754dcf52b4b65748c1dc4b1ed8990ffd","datavalue":{"value":"Horn clause logic with equality","type":"string"},"datatype":"string"},"type":"statement","id":"Q4015952$2A383300-005E-4E63-82F9-B9BB7E6EAA0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c2b32aca426b78b5f53b98e17acd6efaca9a8ca4","datavalue":{"value":"conditional rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q4015952$7413F672-DA58-428E-92CA-48700AC78E08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6c78685aea0a7d91e6d41499c27d1163c6afe98","datavalue":{"value":"refutation","type":"string"},"datatype":"string"},"type":"statement","id":"Q4015952$76F9D3B0-8D6B-4BEC-9315-A8479975EE4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9dc07a7e6f3b66ad29b7cda7dad0506ee5e93396","datavalue":{"value":"first order logic with equality","type":"string"},"datatype":"string"},"type":"statement","id":"Q4015952$8D869DC3-57B0-4CE7-8A24-9A19EF689455","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5f84bfa4d35417b90f2a3d3973763cb89a42b0a1","datavalue":{"value":"paramodulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q4015952$99D02952-A15A-4437-BB0D-3E0F2B8A1894","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3a8387c88a33b804751ee89e9f8712ef76782979","datavalue":{"value":"Boolean ring","type":"string"},"datatype":"string"},"type":"statement","id":"Q4015952$DB18B3A3-A23B-47D0-B95C-A71C0435C853","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":"Q4015952$C99A33BB-18CF-4CE7-B20C-D10B06242D6B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"47f68257298d21c20a9c30f1bb7aa12b4adfb9b2","datavalue":{"value":"https://doi.org/10.1016/0743-1066(92)90047-7","type":"string"},"datatype":"url"},"type":"statement","id":"Q4015952$975667CE-17BD-4D67-B1CD-46307AAC1540","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"abe9dc67c1da9096a8c87043ac8290cab76da724","datavalue":{"value":"W2037405229","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4015952$D13C4BCF-E2D5-43B5-9456-0A723FE106AC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4015952","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4015952"}}}}}