{"entities":{"Q1916976":{"pageid":1927718,"ns":120,"title":"Item:Q1916976","lastrevid":71155746,"modified":"2026-04-13T19:51:19Z","type":"item","id":"Q1916976","labels":{"en":{"language":"en","value":"Mechanising the theory of intervals using OBJ3"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 902713"}},"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":"Q1916976$CCC56C81-2883-4BBB-8DD4-DACD0741BE9F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b5eda76f2c11652b356571902ab89d375d6c5828","datavalue":{"value":{"text":"Mechanising the theory of intervals using OBJ3","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1916976$22723F85-80F1-440F-86FA-1ED08934BDAE","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b7378db4e8c114af1e683aaa14e9ae875d934dc2","datavalue":{"value":"0855.65048","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1916976$B83CEE1C-0EC0-444D-9C85-48F31A3E3BE8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"389b54df42618dc746a9ccf1f40c0a51e53550ef","datavalue":{"value":"10.1007/BF02425910","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1916976$E83869E2-3747-4E11-A945-EA34F1DD22C6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7cf7d6c0c56a0a07029fa41cbfc07c219b42b0fe","datavalue":{"value":{"entity-type":"item","numeric-id":382432,"id":"Q382432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1916976$FD0218DB-9114-4739-A109-A811FDCF101E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f98a6fdc4ebcefbbd3979701deb01ce817be9a62","datavalue":{"value":{"entity-type":"item","numeric-id":175412,"id":"Q175412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1916976$FB8C00D2-2B11-44DE-8D49-B93227394B50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d448ba730ebc19c6dfd77fffbc61ea9fac61e051","datavalue":{"value":{"entity-type":"item","numeric-id":1916975,"id":"Q1916975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1916976$26883E76-782F-4041-B749-83B5A9A8AE33","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"c7999e3e01d43838ac559f475f3b198149793512","datavalue":{"value":{"entity-type":"item","numeric-id":163536,"id":"Q163536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1916976$CD1632FF-6D5C-4CCF-B421-DF0FF77358B6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7823159750286ceb8fb958b098cc6a2dd3d7eb26","datavalue":{"value":{"time":"+1997-02-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1916976$82959127-3360-4D19-83C2-8185877BD230","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"690b5e425ca6eb024f6dcd739d85f5ba3d659323","datavalue":{"value":"OBJ3 is a general purpose declarative language, which was introduced by \\textit{J. Goguen, T. Winkler, J. Meseguer, K. Futatsigi} and \\textit{J. Jouannaud} (Technical Report, SRI International, 1993, to appear). OBJ3 may be used for specifications (being a collection of modules of type ``theories'' and ``objects'') and for prototyping. A mechanism for theorem proving is included. -- The aim of the paper is to formalize the type ``interval'' within OBJ3 by means of arithmetic and set theoretical properties of intervals.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1916976$66EF2F50-758A-43AF-B162-BD33354C59AD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"4d2aa49789d35e35613e1a84ce4788bfee1559e6","datavalue":{"value":"65G30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1916976$9BBF90BC-3F57-41C3-AAF5-8A0EA11D785E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1916976$C6196FDB-9A04-46BB-A91F-694F355ADA6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1916976$1BE16B53-BC5D-44FE-91C0-A67F245B2B10","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1a483d4f27e0d8417faf08436e3799aa674e11c0","datavalue":{"value":"902713","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1916976$43D44C96-4A80-44FB-B0EE-B7D505F96499","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"537db87ac57c0458b36f228e7b0d5f1fe1bf929b","datavalue":{"value":"theory of intervals","type":"string"},"datatype":"string"},"type":"statement","id":"Q1916976$AFDA6BC2-BA8A-45C1-8577-09F516C3ADC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b44e0460de8b89a3695e54806f9b749b49a67a49","datavalue":{"value":"interval arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1916976$8631568B-8D6F-48FB-A8DB-54D12EA29B57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01cffe274754d3f0894dd6ccf7c1cd2e68b69ed5","datavalue":{"value":"OBJ3","type":"string"},"datatype":"string"},"type":"statement","id":"Q1916976$49C4443C-F97D-4970-B42F-E3795A9312CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6bf40ac459cd4020f968693e2461e7f6d3cdeaea","datavalue":{"value":"collection of modules","type":"string"},"datatype":"string"},"type":"statement","id":"Q1916976$5FF90496-C919-4194-8020-1ACF5F12609A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1916976$7EC68503-C85A-4D75-9F85-86FD479C1273","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"9cc9b08ea134d5bef9e23d7e8fde5198cfcf8933","datavalue":{"value":{"entity-type":"item","numeric-id":593285,"id":"Q593285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1916976$2BB3D7C5-861D-444A-ADEE-A402C6432F24","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4840352b17217b124b50c88ee4bd6bcc958c902f","datavalue":{"value":{"entity-type":"item","numeric-id":17510,"id":"Q17510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1916976$5C308B12-ADEC-42B5-B929-011454926F31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1916976$1E48A38C-C9D6-4F85-8BC9-1AEA881ADAE4","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":"Q1916976$AE0DDBE3-F8C6-4B5D-88E2-6AAFB1ABFFD3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d096ad35c32662be4596601668d001e2923907a5","datavalue":{"value":{"entity-type":"item","numeric-id":3345690,"id":"Q3345690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1916976$0CD10E73-0504-4A52-9004-5B9BAE3FC176","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98898e99aa694a75fb295451e61cabd488dc68c4","datavalue":{"value":{"entity-type":"item","numeric-id":3139684,"id":"Q3139684"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1916976$45E469E9-6501-40E2-B22F-BA04F8C69D47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d0f40612567eb3c4338b5bf29ae6d0e125fe7fe","datavalue":{"value":{"entity-type":"item","numeric-id":3948528,"id":"Q3948528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1916976$EE3BDFDA-1D9B-477D-A5FB-1A4665C76100","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"954402668be555381ad11e6bd32fc3ca1b5efed0","datavalue":{"value":{"entity-type":"item","numeric-id":3139687,"id":"Q3139687"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1916976$2A0BFBA8-A601-4AD5-B9D4-250D9D3A75DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ee1ed35e24533712b2c078b403f2fce7e51b332f","datavalue":{"value":{"entity-type":"item","numeric-id":3207999,"id":"Q3207999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1916976$AA7A763F-F3F7-4D52-8CD3-86233A052658","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"085f2f402bb0aaa918a693e06aa64da16c2193f2","datavalue":{"value":{"entity-type":"item","numeric-id":5687569,"id":"Q5687569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1916976$F5A72ED8-8627-4F9A-9029-5E8C0EECECD0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c339fc15a98a4acaaaae58d26f1d8ae94bcf4dd9","datavalue":{"value":"https://doi.org/10.1007/bf02425910","type":"string"},"datatype":"url"},"type":"statement","id":"Q1916976$CE503E51-64DD-4796-ACD2-6A3CED01625D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"187f1369ad5f9b2adc13279efad1d25a167018c4","datavalue":{"value":"W374151798","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1916976$34B42AED-CC43-4361-BA4E-DE09F16DB5B9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"df6fb301ee8c878a64f904ffcb2ba27cd84c2c73","datavalue":{"value":{"entity-type":"item","numeric-id":2765417,"id":"Q2765417"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a2a6ecc949bf0ee55e40bd5a7ba8f73794a1b527","datavalue":{"value":{"amount":"+0.8164175","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1916976$9CF1CB64-4D3A-42B0-BE15-48F4B52B2141","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"65d93be551571fbd2006578c2e21f2db64e5d69a","datavalue":{"value":{"entity-type":"item","numeric-id":3196626,"id":"Q3196626"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1a95184e3dd323e74865abdaee85168b21eed84e","datavalue":{"value":{"amount":"+0.80830914","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1916976$3B0701BB-95E7-401D-A793-36486CF4D8B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d051599a92a778760c32010d66f8e2784220f6f0","datavalue":{"value":{"entity-type":"item","numeric-id":2352502,"id":"Q2352502"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e80d90591afe941189ae3c45b61be0a08eb60a44","datavalue":{"value":{"amount":"+0.8030886","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1916976$28770B2C-874E-4E8C-A62F-AEB37C39AD6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d4a51be5dd4754ab7cfe947795356b25fa671d5","datavalue":{"value":{"entity-type":"item","numeric-id":4011815,"id":"Q4011815"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8afe821d0695066a0aa64478ed3470f0e5fcfbc3","datavalue":{"value":{"amount":"+0.801874","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1916976$8C2F92E7-A402-45EB-B93E-BA81ECD1A787","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5ec8f0a3ccfaacd2d21e3b4396b399bee7ba906d","datavalue":{"value":{"entity-type":"item","numeric-id":2387757,"id":"Q2387757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c92e946d3e2549f03d23f13e18a261f8f77da0c8","datavalue":{"value":{"amount":"+0.80056655","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1916976$37C282FE-7804-418E-8F76-C508F6079309","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"de015fe15561fa42827e5a499bf3d815a4145f74","datavalue":{"value":{"entity-type":"item","numeric-id":4885383,"id":"Q4885383"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"71fb42ef4c8b10abbf5bf1be73cb59350edeba18","datavalue":{"value":{"amount":"+0.79876","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1916976$388B2D0A-8143-4520-8B21-19066C5A42F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"45b5c3dc6f6a47084589950377b71b90c7e5bebc","datavalue":{"value":{"entity-type":"item","numeric-id":4312456,"id":"Q4312456"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e3b2cc49f4298dcd7538d6425e1646f3ce0a9d8f","datavalue":{"value":{"amount":"+0.7973019","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1916976$D9F4F81E-F446-4F62-9291-90DE129DE6DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"075b17ea134b2e51c3a96f08bcf6adfa3d861b86","datavalue":{"value":{"entity-type":"item","numeric-id":3323147,"id":"Q3323147"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e8f02a7501d6c495e13f436ce2cba918001c7caf","datavalue":{"value":{"amount":"+0.79511875","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1916976$C8178281-E3D2-4530-A9FE-19C2CC480CE4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Mechanising the theory of intervals using OBJ3","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Mechanising_the_theory_of_intervals_using_OBJ3"}}}}}