{"entities":{"Q928668":{"pageid":930516,"ns":120,"title":"Item:Q928668","lastrevid":65442843,"modified":"2026-04-12T02:38:01Z","type":"item","id":"Q928668","labels":{"en":{"language":"en","value":"Rewriting with equivalence relations in ACL2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5287722"}},"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":"Q928668$451E07C6-D8B2-4C5D-8782-8EF6D1AB7B8A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e3c9d51b4c3887e92408f8940abb1408300bf411","datavalue":{"value":{"text":"Rewriting with equivalence relations in ACL2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q928668$35C4BA2C-C379-4DFD-8FAF-1B63A587C769","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"89a9acddef04c8564039b8f6057800d47fb20c19","datavalue":{"value":"1140.68029","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928668$6C4936AE-74A2-4CC6-AB82-08871301DA3F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e6bbab2ea230ef82cf7d72bee404dd827d5aaeed","datavalue":{"value":{"entity-type":"item","numeric-id":230814,"id":"Q230814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928668$350A800E-F418-4C3F-A14C-884684E4D06F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b0d384413a2d1b8185eb46b74e5b2c74244e0aac","datavalue":{"value":{"entity-type":"item","numeric-id":928667,"id":"Q928667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928668$51ED674C-C7DF-4331-9046-5A69BACF4D4F","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":"Q928668$5691D877-4DAE-4197-BA8A-8F3707E431A0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9f1c0b93a352a714c61ccd46766a52600d36f8c2","datavalue":{"value":{"time":"+2008-06-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q928668$00CEAE20-D757-4232-8410-1BB6FBCBA831","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928668$E44160F7-63B7-4762-8926-9A6BC94247BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928668$C2FF173A-7F75-4D8A-BAD2-91C20C0472B4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cbf245af08dd6043b85250f7f7db2e53320f88da","datavalue":{"value":"5287722","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928668$1E46DEF6-E044-439D-9FEF-A8E42F92EFDD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"856cbb3a1dd9e116f4ff19f1aee6ebcdf5acff8f","datavalue":{"value":"Rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q928668$476993E6-7C8B-4D52-9825-EF570E15A652","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d2592d1c5d529255aa98dde84e15a8a127fc5f8e","datavalue":{"value":"Congruence","type":"string"},"datatype":"string"},"type":"statement","id":"Q928668$C108A2B7-317B-45DC-BC08-E7429A113C98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"85d59bf82e97527eb9562f81cd04cfa26499244e","datavalue":{"value":"Equivalence relations","type":"string"},"datatype":"string"},"type":"statement","id":"Q928668$48622516-2704-4D81-8EA0-51FA8C1F44D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d9d7a91cce9317b5dfedb3fde9933f83259b7348","datavalue":{"value":"Refinement","type":"string"},"datatype":"string"},"type":"statement","id":"Q928668$B69A9D07-D83B-442A-8238-2606A6C904F0","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928668$EB126EF1-4813-45D4-B7FC-DB9299682AC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928668$882BC33A-E3E1-4DB0-8EE6-430E33AC5AEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928668$93681BE9-4A36-4635-B00E-A4CA093BC329","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":"Q928668$F9F2501C-4B8E-43E2-8D0E-7566FFF8F948","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"96aa799788b98e9d74b0c258cb58c80cd9a63b5d","datavalue":{"value":"https://doi.org/10.1007/s10817-007-9095-9","type":"string"},"datatype":"url"},"type":"statement","id":"Q928668$FCAF6D4E-52D9-4EC3-B413-BDBF5CC885C1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7c0f80b301679f50bada7c1fda39635a29a9abb1","datavalue":{"value":"W1966353549","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928668$060133B0-1D85-4BCA-8158-C08D73327B30","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"283b457c1aa928df8cba388628638010a8a9e043","datavalue":{"value":{"entity-type":"item","numeric-id":4016540,"id":"Q4016540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928668$A3C6947B-D633-4302-9FF1-B5DF4C1B9578","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0aad2711eb9c64a58dada485191047b8af29959d","datavalue":{"value":{"entity-type":"item","numeric-id":4040283,"id":"Q4040283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928668$DD28E739-57D6-44A5-9E45-16C1EA790684","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6496304f13783e82d12a275120aa4626825ea47b","datavalue":{"value":{"entity-type":"item","numeric-id":4231030,"id":"Q4231030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928668$7A0AB9C6-D78B-4CAB-9FBA-FE80F58E471D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca6926d9a2864657c63c8ba6d81f03198b036942","datavalue":{"value":{"entity-type":"item","numeric-id":1595929,"id":"Q1595929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928668$8D354AFA-6F4B-40C3-BD54-E8C5089A1D8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"63ad2ed6b7262bc4aaf760dd16acb7d192abb88c","datavalue":{"value":{"entity-type":"item","numeric-id":3777497,"id":"Q3777497"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928668$4EA07B50-2432-4BBD-85E6-D8DDA4D1CE2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928668$27305142-5005-4816-8D27-19F393179E6E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"525744c38b3fa3b34eea43c43491dc12603b21cc","datavalue":{"value":"10.1007/S10817-007-9095-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928668$ECD7C3E7-27F1-48D3-91D5-F14653C675CF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e236e4ff991212a443641dfc990b384c05eae60c","datavalue":{"value":{"entity-type":"item","numeric-id":2879275,"id":"Q2879275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7af955aa95f2a65f2f28b482c527caadcb9d631d","datavalue":{"value":{"amount":"+0.8420643210411072","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":"Q928668$509E965D-A7AF-461B-86DC-76295E50A9BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d5fba29b8c33e16e6b5e17d1279d611ec3082c9f","datavalue":{"value":{"entity-type":"item","numeric-id":1065790,"id":"Q1065790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a9baf29fb9ba86b32e6e7de3d63ef49795d81784","datavalue":{"value":{"amount":"+0.7687579989433289","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":"Q928668$F0206B54-9829-434E-8306-D6A5C28D4C3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"067b9ee5d1759bf8dfdf5a7d76851fcc9c0894c5","datavalue":{"value":{"entity-type":"item","numeric-id":1610218,"id":"Q1610218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"00b3160885750f39d3d4ff039858a6e1ece06392","datavalue":{"value":{"amount":"+0.7549715638160706","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":"Q928668$382D17A0-6C57-4B0D-8FFA-31383309DC23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c19118d14a947e6af33fd309a7fbe5f1fab42df4","datavalue":{"value":{"entity-type":"item","numeric-id":4449180,"id":"Q4449180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8097fffa7bc4c183b036c8a050724f6174e3565d","datavalue":{"value":{"amount":"+0.754041850566864","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":"Q928668$69D3E042-8D46-487F-9C8C-8D4B7D665EE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4ed4452b88de96217fce2d9ac9f739d7aa5dcc1e","datavalue":{"value":{"entity-type":"item","numeric-id":3719825,"id":"Q3719825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cc39c68d2fa6fe64f36a96309e0c75c8e3954a40","datavalue":{"value":{"amount":"+0.7539247870445251","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":"Q928668$CDD98970-9E57-42D6-A307-2A9557E8D2BB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Rewriting with equivalence relations in ACL2","badges":[]}}}}}