{"entities":{"Q3075243":{"pageid":3085959,"ns":120,"title":"Item:Q3075243","lastrevid":86149982,"modified":"2026-06-03T15:39:10Z","type":"item","id":"Q3075243","labels":{"en":{"language":"en","value":"Basic first-order model theory in Mizar"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5850139"}},"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":"Q3075243$8E5C2490-A4A4-475A-A364-FD5016AF6706","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d2a5b8212fe5fa19335aa45e41be35fbc92e50f3","datavalue":{"value":"1211.03024","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3075243$74880338-BAD6-4007-A761-1BFC4C652F05","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"76c08091180089def748f7e20273d2f981bdee68","datavalue":{"value":{"time":"+2011-02-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3075243$F6E510E0-134B-4650-B2CF-E4301E6E616C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7eebdd380dc54ec4dd2a3bf2380de3d3abb23c30","datavalue":{"value":"http://jfr.cib.unibo.it/article/view/1974","type":"string"},"datatype":"url"},"type":"statement","id":"Q3075243$19BC0DFA-D239-4F97-AC0E-239D94086742","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3075243$15E7F510-EC52-4C8A-869D-1B93842F9333","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"abca938afd309309893053e8ee4f51374fed9de6","datavalue":{"value":"03C07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3075243$2D1F40BE-6536-4F05-92D8-F597DDB3927D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3075243$3EEFD684-10A9-4AA4-A888-6E2D96605B66","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"762c49ba40eb7429c38c9c2b5df41561f0c7800c","datavalue":{"value":"5850139","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3075243$0950D6CF-C65A-4869-ACCB-41726DF99D93","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3075243$4E5449FF-910A-45C0-AFED-63E0BE2D500D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1b3fcc21df8775948283a2fd666470875b573983","datavalue":{"value":"Mizar Mathematical Library","type":"string"},"datatype":"string"},"type":"statement","id":"Q3075243$7A882B88-5076-4385-A2BE-6A3EA626CF8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1bb0231f1bac92a09236c1dec00a1e9fbbf81047","datavalue":{"value":"classical first-order model theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q3075243$EB4E98C0-2D0A-4143-B6FA-3087DB43C8F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4a614927b0caf638748bb51c0de92c1b49104311","datavalue":{"value":"proof checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q3075243$3C2DCC4D-A382-417C-B2ED-DA31FEFD006E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cd203fcc0df99bfc5d96e5da8c712e14410da8f4","datavalue":{"value":{"entity-type":"item","numeric-id":1945909,"id":"Q1945909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3075243$C6F169BC-C319-4AA4-BA49-1D3E4DF31FF3","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9c2ac6c1c15bd263207487c53115a7cc6abe2547","datavalue":{"value":{"entity-type":"item","numeric-id":19033,"id":"Q19033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3075243$553FFFE9-A203-4018-8D98-40EBB97951D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3075243$0ADA9CC7-7EED-49C1-874B-4EC06474903E","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":"Q3075243$BC013CB1-A8D1-4D76-A02F-B4820A80E8C7","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"85445e218d9c7de34710abeb0c0c4584e4d8d5dc","datavalue":{"value":{"entity-type":"item","numeric-id":2865746,"id":"Q2865746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5263ac1a8e95699dfc414dceb498964a45193538","datavalue":{"value":{"amount":"+0.8358290195465088","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":"Q3075243$FCEFD5BF-69A5-4679-AA8C-1727753D66ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"587928473c713570802984c6d141de7df55a3c2d","datavalue":{"value":{"entity-type":"item","numeric-id":4247076,"id":"Q4247076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"97e63b994ea85ad11a549788d869d0c22c3e2b5c","datavalue":{"value":{"amount":"+0.7925159335136414","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":"Q3075243$C8E95AEE-3433-4C23-AD7E-073BFA9C0C72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d79e1519b0a7d33b73c5772d888b199f6824eca8","datavalue":{"value":{"entity-type":"item","numeric-id":4503907,"id":"Q4503907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f72e8aac96103b1956ba2a7b2f1886ff1404b72c","datavalue":{"value":{"amount":"+0.7925158739089966","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":"Q3075243$24C4C383-1A10-41B7-A298-EEFFB2DB2E85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ddf1e310d4319850dc53c03d715caa346851662f","datavalue":{"value":{"entity-type":"item","numeric-id":2865750,"id":"Q2865750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d84f1be5a3a1b3aa861250a1b3bb0356bd56ae48","datavalue":{"value":{"amount":"+0.7790896892547607","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":"Q3075243$1BCFDEF3-956B-4BC1-A9C4-CD54F4B0DB19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"33fab66fa4452b185827448d18b127de03bccdd3","datavalue":{"value":{"entity-type":"item","numeric-id":2852157,"id":"Q2852157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"69361ccd9a6af855f34d7e309ebcd5d07d48751c","datavalue":{"value":{"amount":"+0.7772589921951294","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":"Q3075243$56C05579-1822-4EDF-8294-8DC880882551","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Basic first-order model theory in Mizar","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Basic_first-order_model_theory_in_Mizar"}}}}}