{"entities":{"Q352977":{"pageid":354744,"ns":120,"title":"Item:Q352977","lastrevid":61229289,"modified":"2026-04-10T22:00:15Z","type":"item","id":"Q352977","labels":{"en":{"language":"en","value":"Paramodulation with non-monotonic orderings and simplification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6184690"}},"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":"Q352977$9FF5D5B8-87DA-4801-BAB5-2356E7C61C4E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e71fb8cf50bf8ceacd64ee7095dff6495198cc4e","datavalue":{"value":{"text":"Paramodulation with non-monotonic orderings and simplification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q352977$9A2C83D0-F96C-4488-B32C-F7FFCDBBD9B1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0be445c2390652e4ba6842106ac09a15e079bd74","datavalue":{"value":"1315.03017","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q352977$0B588CD7-1579-4DCB-9985-A6354D82E56B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1ce8850632b90b69a6c289735cc288ece6fb9e1a","datavalue":{"value":{"entity-type":"item","numeric-id":352975,"id":"Q352975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$0995D252-7102-480E-BD04-6B03A91F53C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"076f42ceb107ac95ece0987fd254ab37feda8487","datavalue":{"value":{"entity-type":"item","numeric-id":352976,"id":"Q352976"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$C86D8C6D-24A4-4D22-AFCC-59FD09B58B70","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$25AA55A2-7F2B-4F1D-A3DC-DC4688E3632B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e553745941756c98d8238154d74f9ad7174c4d8e","datavalue":{"value":{"time":"+2013-07-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":"Q352977$C788FF4C-79A5-42A5-B8A0-EE2F7CB4FCB1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q352977$0FF732A9-CD3E-49B5-A53D-670A4797121C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q352977$E9056BF3-F2C3-42DD-9ABF-B4A0173A7240","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8680e21038c5cdc3e3977b13b0df49e1c2aaaab0","datavalue":{"value":"6184690","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q352977$3ACEF5C1-8149-46EC-A009-8766583F709F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q352977$662A09FE-C878-4AE1-B416-7FEE1E4B3B77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ca82b8126faca2bdab3ffa77f0c22600be2e10e6","datavalue":{"value":"equational reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q352977$B79838AC-FF3B-470F-A7C1-EF7F3B623F7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3e36f8bb3dd0b9402bfd5969f9133fc39993866c","datavalue":{"value":"ordered paramodulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q352977$00B3C922-7CE4-4421-9EDA-1E15A6F5318B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"019a6ed5982241abb5ad173ea9f0389406288f3d","datavalue":{"value":"Knuth-Bendix completion","type":"string"},"datatype":"string"},"type":"statement","id":"Q352977$366EB487-9E55-4EDB-ABB0-3498FCD6268F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4c5e63746f1155fa9146a08988f7e26222436fba","datavalue":{"value":{"entity-type":"item","numeric-id":21994,"id":"Q21994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$EF1E9E88-3295-4577-BE7B-4E7DBDAAF76C","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":"Q352977$6794A53E-4961-4375-9314-9AAD785522DF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4e7627d6cfedace4e1693b8e31e0426e6e7b8eb9","datavalue":{"value":"https://doi.org/10.1007/s10817-011-9244-z","type":"string"},"datatype":"url"},"type":"statement","id":"Q352977$D591C1BE-1B18-4967-B7A2-CF6811477FB2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1e827b5a1961a8cc2c4490f0b6962da8f40267cd","datavalue":{"value":"W2041375296","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q352977$52E1CB36-0BA2-40BB-AB8F-D0176654BF83","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ee132c4e5792ab38a0ff46d3d93155b8fcbe98d8","datavalue":{"value":{"entity-type":"item","numeric-id":1978641,"id":"Q1978641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$FBB9B290-C980-4BB6-80CF-D9B0AAB1532B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"819a2535befb2a67f49ee5e43432525215be36de","datavalue":{"value":{"entity-type":"item","numeric-id":4702972,"id":"Q4702972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$95BD04F3-9D98-4C36-AAF9-70893576695B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7aa3cb4eed92e572c0b080c767bbb92340713510","datavalue":{"value":{"entity-type":"item","numeric-id":4299008,"id":"Q4299008"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$5085888D-B791-4C15-8F42-3A6D0C33B411","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aefe5e0f2b827afb25f0a8067d25c4a893f91ca","datavalue":{"value":{"entity-type":"item","numeric-id":4304492,"id":"Q4304492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$E1E65F7F-386C-499A-BC4F-B9CA25079CBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"49666558e5a266f8c31a331a000db76b0e587406","datavalue":{"value":{"entity-type":"item","numeric-id":4524792,"id":"Q4524792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$33B21A31-FE96-42E7-BFB6-7F11067EFABC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ad7c23e8d7895495a33ef0a244c1d5f7a7d7e16","datavalue":{"value":{"entity-type":"item","numeric-id":1899908,"id":"Q1899908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$4ECC797E-7971-453F-865B-9C77E54F9512","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c16d7d2df2a108fcb7f312fef70d84ef9c206b3","datavalue":{"value":{"entity-type":"item","numeric-id":4809078,"id":"Q4809078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$705F2C8D-7A82-46B1-845F-A78A84021706","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7de8c98672a354edf1b70c44a0ad4ca38400899c","datavalue":{"value":{"entity-type":"item","numeric-id":5307052,"id":"Q5307052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$51FDC9E7-DED3-4929-B5BA-BA92CB3088E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64e4df724527c603aeeb06f78aff02723c091826","datavalue":{"value":{"entity-type":"item","numeric-id":3623219,"id":"Q3623219"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$392B1C6E-30C8-4661-B798-710A25D0D960","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"026ae6828ecda66ae5806f5536df3172b5fec9f9","datavalue":{"value":{"entity-type":"item","numeric-id":1810859,"id":"Q1810859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$4E1A5D0D-B15E-4215-9F9D-548F89990D0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f379c0c8372e5f5c3f6f1ec2ecbe2d16fde0f60","datavalue":{"value":{"entity-type":"item","numeric-id":2723431,"id":"Q2723431"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$B0628FCF-A33C-4CB7-89CA-2766BBB40559","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":"Q352977$CDB1AA2C-8CDB-464F-A2AF-2962E2B6EAA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a01d4a91dcf05e247efe3d36d8b1cf5c4792f88","datavalue":{"value":{"entity-type":"item","numeric-id":4385532,"id":"Q4385532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$4F2965B9-6BF8-4080-A93B-B41520C482EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b27d44a0e50fda314668a36654efb04ab5135cb3","datavalue":{"value":{"entity-type":"item","numeric-id":3868730,"id":"Q3868730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$B31D4A5B-C568-43C3-A954-85129A99FFAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7bc614fe187bd0295ec729cf32cb3675e34b7b37","datavalue":{"value":{"entity-type":"item","numeric-id":4302847,"id":"Q4302847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$E8F1459B-6EEF-4A42-86C6-8FE98AAF19B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"866329e622ae9c42939978c38ec9f1b061288e00","datavalue":{"value":{"entity-type":"item","numeric-id":4494366,"id":"Q4494366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$CA487124-7900-4B74-AE45-2346A0B742B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"78a8fb7c1504b4023b489475633410efba01eda3","datavalue":{"value":{"entity-type":"item","numeric-id":1897557,"id":"Q1897557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$A89DE683-63DF-40F9-850F-CF22DD4DFB33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f14878b4342799995051ac9bc54cd21c98efc98","datavalue":{"value":{"entity-type":"item","numeric-id":2751359,"id":"Q2751359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$06051130-3A23-4B35-BE4E-2DA3738AEFC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a60759639915f213cf6f47415adfbdbc33f70fa2","datavalue":{"value":{"entity-type":"item","numeric-id":3527302,"id":"Q3527302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$CD1CCBBC-EDF7-4011-B483-368307EC9BE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60d06c26862db1f7e59f700a6fed580956476040","datavalue":{"value":{"entity-type":"item","numeric-id":5747788,"id":"Q5747788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352977$BA0994D7-9029-47D4-B64E-4DFA93F92C16","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"35b345de3eebc383032212e922a564ad9202fefc","datavalue":{"value":"10.1007/S10817-011-9244-Z","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q352977$87DBF203-5CC2-47CE-A5E6-3668B8D827E2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"094f9b8a164df1e06a79f7a223e65f4a0e1c7749","datavalue":{"value":{"entity-type":"item","numeric-id":5307052,"id":"Q5307052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82320d1ee6b7bb79170f19bedc5b72c1a788b148","datavalue":{"value":{"amount":"+0.9400429129600524","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":"Q352977$18016547-82E4-46BD-A24C-E5409C715E86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f88a4c8426548476533bf257c9703ab16bb53b0f","datavalue":{"value":{"entity-type":"item","numeric-id":1810859,"id":"Q1810859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"37630b3cf1bed1b5d739af3eb73c217817843ae4","datavalue":{"value":{"amount":"+0.8875083923339844","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":"Q352977$32259830-8444-403B-8692-A0A646599418","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a8208072dd51e1bed16409f73faed688c572173b","datavalue":{"value":{"entity-type":"item","numeric-id":6488550,"id":"Q6488550"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"37630b3cf1bed1b5d739af3eb73c217817843ae4","datavalue":{"value":{"amount":"+0.8875083923339844","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":"Q352977$A165AE3F-E12C-4452-A7FB-244925067ACF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"678f52d20cbd1ed66863391105aef6e91c97f013","datavalue":{"value":{"entity-type":"item","numeric-id":3623219,"id":"Q3623219"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"735060784208660b2aed8a79138cf564d3870679","datavalue":{"value":{"amount":"+0.8353522419929504","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":"Q352977$F63F69F3-AE13-47FF-9F34-3FD495A32AA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"694aa61f99a25afa5a211a0321445f30285ce091","datavalue":{"value":{"entity-type":"item","numeric-id":6488549,"id":"Q6488549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0b6a4fda6bdab0f6c851bf58db07b9ebec0bec91","datavalue":{"value":{"amount":"+0.8175075650215149","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":"Q352977$824CDB2C-6DB9-462E-BFCF-38F9E4F426CB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Paramodulation with non-monotonic orderings and simplification","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Paramodulation_with_non-monotonic_orderings_and_simplification"}}}}}