{"entities":{"Q909488":{"pageid":911336,"ns":120,"title":"Item:Q909488","lastrevid":65275383,"modified":"2026-04-12T01:29:25Z","type":"item","id":"Q909488","labels":{"en":{"language":"en","value":"Term rewriting and beyond -- theorem proving in Isabelle"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4137349"}},"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":"Q909488$7043FA14-8D99-405B-AD36-DE48B832B73E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"64f69eb034d8a3e1e9c40373964eb98187baff07","datavalue":{"value":{"text":"Term rewriting and beyond -- theorem proving in Isabelle","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q909488$5E0E17FD-9B1E-494B-97A3-94E5C5929C61","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b3772e09e8578adf90b4f5818e2701129b95c3eb","datavalue":{"value":"0694.68059","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q909488$060DD664-1527-4EE1-971E-79D1162E7D8D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"34bc7b31dc1e9e9ee3f0e96a3e5a9ec2f00ded7c","datavalue":{"value":"10.1007/BF01887212","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q909488$3AC35174-AC36-4B01-BC1F-551E334BD7C1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bd39997decddd4925a8ef09cbbffc4f41d2b1f00","datavalue":{"value":{"entity-type":"item","numeric-id":670700,"id":"Q670700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q909488$ED82565D-D99D-4D07-9739-4A41804EBF45","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d9925518446645d219093152a820aba790417b61","datavalue":{"value":{"entity-type":"item","numeric-id":164203,"id":"Q164203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q909488$68025759-D49E-4F3B-ABDC-5C2F1768D9A6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7211ad5ca16eb0d22cd0051fff3d0f3af254ceb6","datavalue":{"value":{"time":"+1989-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":"Q909488$ED8C1579-C38E-47B3-BA53-FC73E2FB5BF6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q909488$D917E1E2-5374-4ED2-81C5-6D2347C5F130","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q909488$437AB61B-70BA-4607-A40A-C9BC9F02A221","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3f97694d44af155a68434cb72eabc6a4d5dd5227","datavalue":{"value":"68P10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q909488$A66425DB-2F99-4BFE-8222-F365E3EB89E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6be78f1bad1f2f19058dbde65eb124c0430a7d27","datavalue":{"value":"68W30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q909488$4F4B3309-CA43-41CF-8ABE-2018B757BEB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"21699a423435669f291d1bd1ba3da28fa1465b3f","datavalue":{"value":"03D03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q909488$72541030-087C-4EBF-9667-2FF4AF8E2840","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"913b8bbd1347f714f758af1f48fff402896f8d2f","datavalue":{"value":"4137349","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q909488$983E5B4D-648C-4F72-A8E0-0F3F87C3D682","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5a664fc87eb2216b1fad976387dcf6ff589b12b5","datavalue":{"value":"term rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q909488$5588A90F-E07D-40AC-8591-CEBBB1DF9338","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q909488$8BA4AC44-C47D-436C-87FB-C78E2DB83E09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q909488$45A13B4A-5448-4A9C-8F24-FFB5F54ABF9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bbea74bea78fb379c705a66bfbc4d6cf8cdd3408","datavalue":{"value":"quicksort","type":"string"},"datatype":"string"},"type":"statement","id":"Q909488$BB8FAB67-B526-4180-83E0-509D4A1D2BAB","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":"Q909488$8FCED863-DF32-467B-8744-5331610BC982","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"91328e3ac5dfce9b45d01b607b8d8c272a5b6733","datavalue":{"value":{"entity-type":"item","numeric-id":14670,"id":"Q14670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q909488$F83E72E5-28E7-479A-BF06-F22706750DEA","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":"Q909488$A291F78F-FE56-434E-9894-BDFECC603958","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":"Q909488$A309E8E0-0FB5-4C91-965E-ECFCC822001E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"becf5f4cc735947b117fb82f7aabc6a54df59ef2","datavalue":{"value":{"entity-type":"item","numeric-id":1099615,"id":"Q1099615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q909488$15E600B8-80A5-4129-AC86-1B142E88F0F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c5ae7e408b1d1201c271e00762d47096e39a012","datavalue":{"value":{"entity-type":"item","numeric-id":4111080,"id":"Q4111080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q909488$4F52FB7F-BAFB-4350-93F9-43FCE47D48C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc8abb92210655a5bd4143cbbadd6eadb52d635","datavalue":{"value":{"entity-type":"item","numeric-id":1801222,"id":"Q1801222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q909488$65EC62ED-191B-455D-8123-01C92588A726","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a9d0de0ba52048b2594da38e4815945e3a42363a","datavalue":{"value":{"entity-type":"item","numeric-id":1251063,"id":"Q1251063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q909488$80B81DE6-FEFB-46A7-BFA4-D50B0CA5D081","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0e4e03f3dd8f7362d729507ad34add946ab883b","datavalue":{"value":{"entity-type":"item","numeric-id":3674088,"id":"Q3674088"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q909488$ACDBAE95-DF6D-4257-9406-44A0A007D61C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c9465d6417bb77bd19e652eaf6c381784d12e8b","datavalue":{"value":{"entity-type":"item","numeric-id":3936229,"id":"Q3936229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q909488$62C78E35-5DFE-4277-9941-CCBE8589295D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5809a6684c365442525c649f10f3cfd46627fcb","datavalue":{"value":{"entity-type":"item","numeric-id":1825045,"id":"Q1825045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q909488$FF2A952E-822E-446C-ACEA-9CA54AF86B6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b553ff2ef333f88214bff06cd1a2385f42e0b76","datavalue":{"value":{"entity-type":"item","numeric-id":3827551,"id":"Q3827551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q909488$D79970E5-2715-4286-A876-269E26BF5C77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"35852691e725c71cf8e921b7748b4e2b09da6624","datavalue":{"value":{"entity-type":"item","numeric-id":800739,"id":"Q800739"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q909488$825D0B4D-5D86-4FBB-B731-FBD8607563C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab8d7dcc337f0f7083d889ef5fbd195dbcbfcdc2","datavalue":{"value":{"entity-type":"item","numeric-id":4720797,"id":"Q4720797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q909488$254C65C1-A866-4980-9220-CA95519702F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"777f1902a1127b94884ae1ddc89768860f054a6e","datavalue":{"value":{"entity-type":"item","numeric-id":3789060,"id":"Q3789060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q909488$B4ADACB7-9F14-4F75-9251-D32AF5E15831","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1404903fbb3450c69ae4b46e148487834232fe43","datavalue":{"value":{"entity-type":"item","numeric-id":1823013,"id":"Q1823013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q909488$A06F2739-BBA3-4B8A-B5D1-CCC6EB291644","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b619d0dda2dd02de39ac79d3bfdbb57ce02cf9a4","datavalue":{"value":"https://doi.org/10.1007/bf01887212","type":"string"},"datatype":"url"},"type":"statement","id":"Q909488$371B8FFF-7061-476B-9D4F-7AEF771E9929","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d593b74dc2c84eaa5f7c34a521fb2493595a6a9b","datavalue":{"value":"W2129384986","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q909488$750DC2AD-C3C8-456E-8B36-46D6F3121E49","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4975addb4905a856dc84fcaa166c071e9d04c5e7","datavalue":{"value":{"entity-type":"item","numeric-id":800739,"id":"Q800739"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4d296eb42d7cbe8556176bb4e5173911ca532556","datavalue":{"value":{"amount":"+0.8279831409454346","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":"Q909488$53D58EF5-5458-43DB-9BD9-33D71E5FE618","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e9d46345375cf30c0ce392ba2457e734405cc9d7","datavalue":{"value":{"entity-type":"item","numeric-id":5096184,"id":"Q5096184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6c4a21d6dc011d7ac74d7e40be64b3bc5fcebacf","datavalue":{"value":{"amount":"+0.800305962562561","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":"Q909488$79731069-A2C4-435E-812D-F7D34609DA0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0db0fc7f44189aaffeb910455ec48d98d1e35fe6","datavalue":{"value":{"entity-type":"item","numeric-id":5901573,"id":"Q5901573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ef7b3234da1c5ac2e054aea31f3b65b2425fa265","datavalue":{"value":{"amount":"+0.7960807681083679","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":"Q909488$93959728-3230-4AA6-8C2D-39760450CB14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b41219a08974f1820b6a934c8c33bf903d59a40e","datavalue":{"value":{"entity-type":"item","numeric-id":3088004,"id":"Q3088004"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0550a7f3f215fb93906d59e7ba2d28623c019505","datavalue":{"value":{"amount":"+0.7940559983253479","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":"Q909488$953C8C98-5482-4531-974D-3EB6D8FAFEA2","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":"979a2c0114e24ebfe3dda8cd3fc381d007cc8a96","datavalue":{"value":{"amount":"+0.7925293445587158","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":"Q909488$73EBA1D3-F1CE-49B6-9E1F-9C1B74D312BA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Term rewriting and beyond -- theorem proving in Isabelle","badges":[]}}}}}