{"entities":{"Q3051901":{"pageid":3062617,"ns":120,"title":"Item:Q3051901","lastrevid":85578962,"modified":"2026-06-03T09:56:25Z","type":"item","id":"Q3051901","labels":{"en":{"language":"en","value":"A method for proving ITL theorem by using PVS"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5811673"}},"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":"Q3051901$F5C39374-61CE-4232-97C8-A9158891D3A7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a08cbe64079a296b8b9bda6542a5fb1e719ee512","datavalue":{"value":"1212.68036","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3051901$2FE82847-4F02-4B7F-9511-2E1CB9EC053D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b945e51e7351a8e7a2f446e2e70e5c495b7cfcc9","datavalue":{"value":{"entity-type":"item","numeric-id":1650139,"id":"Q1650139"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3051901$B5E2643C-8613-4538-BEE8-04C6A8F47163","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"036b0aa8d2375f179bf81681695e289fd25083f8","datavalue":{"value":{"entity-type":"item","numeric-id":474445,"id":"Q474445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3051901$8578E5F1-61FF-46EF-AAC0-C50CCE0C1CEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"375d61e6e57db7a54fe0c769e106bc7c3b879d9d","datavalue":{"value":{"entity-type":"item","numeric-id":1030459,"id":"Q1030459"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3051901$9F1BE755-2A61-4412-BB7E-8E3D3D48B17D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e207171999d8bccd08779f13059dd3836085b46a","datavalue":{"value":{"time":"+2010-11-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":"Q3051901$C5AA0B98-7A95-4A24-B0B2-46A4A711E593","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3051901$5D68708E-9B91-4910-A443-4E97E2799B50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3051901$4303EFC4-6757-48DA-AB1A-AAC7B39CF57C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a3b91a59f3fbc1764420a171cb38bab3a2161b10","datavalue":{"value":"5811673","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3051901$58FEAA19-D909-4488-AA18-49B8B339EB59","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4a7b19bbe93bbb6b0c4a06b7379f5542c9b34ea7","datavalue":{"value":"interval temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q3051901$6EC6C63C-3B90-47A4-B0CA-AA18D3F429F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e13bc8441d7666d4310a93839316ebef38c603a6","datavalue":{"value":"prototype verification system","type":"string"},"datatype":"string"},"type":"statement","id":"Q3051901$5D6EADB5-D34E-4849-BFEE-8A2812D68E36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3051901$B0F1D575-955F-43CF-833B-FF3999097C94","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3051901$F6E7C22E-A0B2-44DA-B2A3-17242F3ABAF1","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":"Q3051901$CB0901DF-E154-4687-A4FB-89457EB195DC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5c2a1beeb65f90db18752e8b6efdb742022359c2","datavalue":{"value":{"entity-type":"item","numeric-id":5305658,"id":"Q5305658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6835ec7fc712468b606c0bbbc8094a8b9c2cb670","datavalue":{"value":{"amount":"+0.7092452049255371","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":"Q3051901$2DF80209-1A53-4A51-9ABA-6B61418EF18F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"49451e82aef643ace89a93dfd8a95c933ab777e6","datavalue":{"value":{"entity-type":"item","numeric-id":2723435,"id":"Q2723435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7b3e3e898d18756c15a77264bdd86c87efea2157","datavalue":{"value":{"amount":"+0.7025489211082458","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":"Q3051901$3E757623-B222-4290-8D9E-6A5BEA0BB251","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"899e630ab1ca3ef753087abcf3e220b20d3b893a","datavalue":{"value":{"entity-type":"item","numeric-id":1603708,"id":"Q1603708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5e512a482f30fdce9f115eef81a9919a8be6d9d9","datavalue":{"value":{"amount":"+0.6996968388557434","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":"Q3051901$CFD12F90-92E1-493C-A5CD-E00166E42BFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c4a7012ca2bd562a7e57df0b315383bccdc5bda4","datavalue":{"value":{"entity-type":"item","numeric-id":2300079,"id":"Q2300079"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f68cb713979f02c45e1430d37133f25ec9d5a242","datavalue":{"value":{"amount":"+0.6996352076530457","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":"Q3051901$C9FF50D8-9C8F-4C1E-9701-2EBAFA052764","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"590389987854c62166aa437651a61e790abebe66","datavalue":{"value":{"entity-type":"item","numeric-id":2864359,"id":"Q2864359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4ed5be999c547bac98adc302c0817bfa37e07e70","datavalue":{"value":{"amount":"+0.6986685395240784","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":"Q3051901$AD47982D-95BA-42BB-8289-1E1A95802320","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A method for proving ITL theorem by using PVS","badges":[]}}}}}