{"entities":{"Q1825045":{"pageid":1835787,"ns":120,"title":"Item:Q1825045","lastrevid":49318909,"modified":"2026-01-06T23:10:06Z","type":"item","id":"Q1825045","labels":{"en":{"language":"en","value":"Equational reasoning in Isabelle"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4119666"}},"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":"Q1825045$EABA9523-C6EB-4ECD-8159-D1A406B2CD3C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2904a2b327461ec93c00a30fc5125b94b033520f","datavalue":{"value":{"text":"Equational reasoning in Isabelle","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1825045$B1455882-FFCF-474A-932B-12A06C26015B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4eab4c977ebb01d51c80a649a10798123a4360be","datavalue":{"value":"0683.68081","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1825045$424DA640-AE20-4A7B-8AFF-D78C7C7BAE97","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b10a01c8aac49901676687b1c1d357c8e27f6867","datavalue":{"value":"10.1016/0167-6423(89)90038-5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1825045$D1118140-A953-4996-9133-B46B60ACDEF0","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":"Q1825045$B4990FEC-2C58-4CA8-A7F5-FEB034B05F4D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4082512e7d3530b9726df691c7c28e9fec542a8c","datavalue":{"value":{"entity-type":"item","numeric-id":169675,"id":"Q169675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1825045$A96DBEA9-4F52-4084-AE99-2EB8BD637EC9","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":"Q1825045$1AF45C2B-CDD9-48C8-9703-2FB405117A84","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"45e22dd7469e55a841241c69846adc5880a187af","datavalue":{"value":"Isabelle is an interactive theorem prover developed at the University of Cambridge. It differs from most other theorem provers in the fact that it can be parameterized by the object-logic to be used. This feature made it possible to carry out a case study in an equational logic - a fragment of the first-order predicate calculus. A number of used specific tactics, embodying theorem proving techniques in that logic, are described. Though an efficiency of the process is not discussed it proves feasibility of the selected approach.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1825045$AFCB281A-6DA6-4E4A-97F9-7F0831B01CB5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1825045$6D102B19-0925-4695-B872-C5CBA9FAD696","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"014c8e79cdd57a9e93737f7f81e168e2bd258a2b","datavalue":{"value":"4119666","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1825045$C4D35256-96C4-456D-81D4-4EF35CD6A445","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a71fe6392c09db6db9e6773c3ed8aad99a981365","datavalue":{"value":"reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q1825045$F636335B-0B23-4BAE-A8B2-C551C3E0DD49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1825045$F964D745-3514-4E03-B8C6-BB71D7E24A8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"744fd5f6b592344bd2a87ac1816bb7847861172e","datavalue":{"value":"equational logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1825045$47740D8B-6895-4955-AA47-AC70595197A2","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"56a1ca2701a8ace98397887a83075850e16781d0","datavalue":{"value":{"entity-type":"item","numeric-id":274436,"id":"Q274436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1825045$E8B9890E-B42C-4BDA-BE35-CDB5C3E7D5B7","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":"Q1825045$06473F97-A12A-4468-9653-B0E0CD81D47D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"78b4c4533f5fb3342dee702d4e8381a8d42cd411","datavalue":{"value":"https://doi.org/10.1016/0167-6423(89)90038-5","type":"string"},"datatype":"url"},"type":"statement","id":"Q1825045$2B764FA6-5A00-4A9C-B974-67A3A02F1ED1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8fbd4adecf7b5f09733415d562ae0a9c605534ad","datavalue":{"value":"W1980290268","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1825045$A1C09294-773B-4C62-9988-88B43018A8A9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a02b2bfea1c5f47cd601f5ce8d9525ee86d87fe","datavalue":{"value":{"entity-type":"item","numeric-id":5219926,"id":"Q5219926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"72dc3d0f92aaf34c5b4b5b325988a06867a6a2c8","datavalue":{"value":{"amount":"+0.7489650845527649","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":"Q1825045$4E0A667D-36A9-4477-AA8D-5115A629CC45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"619d07d39ad50d8b9a4d0bfcd8121f291b2fc77d","datavalue":{"value":{"entity-type":"item","numeric-id":4364537,"id":"Q4364537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ee026fac863dc2a6c9c5b4c32835490e0324d2a6","datavalue":{"value":{"amount":"+0.7488712668418884","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":"Q1825045$64BC2340-DBB1-43F5-B46F-C1CA6C56D5E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"027e66e493294de396e3f06701b232a3660c5eaa","datavalue":{"value":{"entity-type":"item","numeric-id":1823013,"id":"Q1823013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"20219a5d6c2fed254f8bd4c3dbc436a4d1d2ac2a","datavalue":{"value":{"amount":"+0.7423955798149109","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":"Q1825045$8E420E31-68E6-4AD3-8E97-AA826FF23419","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"20821278b54273bce32a61f8d97e3bf2e0967751","datavalue":{"value":{"entity-type":"item","numeric-id":5307074,"id":"Q5307074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"19fb1a2770025e23e2a5df0f80130e36103045ad","datavalue":{"value":{"amount":"+0.7416177988052368","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":"Q1825045$8C427D1B-1BE2-4CF4-B2EE-7ECCD1BD2039","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a0cc07b681385ffb864e3e24cf69f53f7eb1978e","datavalue":{"value":{"entity-type":"item","numeric-id":4933332,"id":"Q4933332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"22ce72491243dae90e6d138e02b1277cd9eecef6","datavalue":{"value":{"amount":"+0.7412963509559631","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":"Q1825045$79E49C51-10BD-48C5-ACA1-1310DDA46368","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1825045","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1825045"}}}}}