{"entities":{"Q6535381":{"pageid":14146524,"ns":120,"title":"Item:Q6535381","lastrevid":57344322,"modified":"2026-03-30T14:08:04Z","type":"item","id":"Q6535381","labels":{"en":{"language":"en","value":"ALASCA: reasoning in quantified linear arithmetic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7777328"}},"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":"Q6535381$6AAB2248-97F5-41B8-9AAE-1CA572054B9B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"89e45a6db537452d3e6c211d8aacacb0c1eb090d","datavalue":{"value":{"text":"ALASCA: reasoning in quantified linear arithmetic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6535381$1F73593F-F4A8-44B0-B61B-161328DD8165","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a5d6235f18905dc9276ffbe1a2b391e375d1f97b","datavalue":{"value":"1543.68406","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535381$B529DCE1-D791-4F98-9F8A-391327A82563","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"172f584536068790ceaf1f9473523d6054056606","datavalue":{"value":"10.1007/978-3-031-30823-9_33","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535381$AFE9C8B0-C67D-4268-ACD6-560E9E03921A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ce9e1735095a7237c0c699c31f4c0eb57566d709","datavalue":{"value":{"entity-type":"item","numeric-id":1401931,"id":"Q1401931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$275DD43E-1BF7-4490-90C7-8DCEFA32A709","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f17059e6c6c8a57972334867cc4d511b5d1368f5","datavalue":{"value":{"entity-type":"item","numeric-id":507357,"id":"Q507357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$BA7D3C05-4D71-4E4B-839C-F4D49FA9AC70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"395a9171f6bae9b8af4e7440aa83cc44ae6e3948","datavalue":{"value":{"entity-type":"item","numeric-id":2075783,"id":"Q2075783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$AEB60C74-CF2E-4038-82AE-11BA9EAE9974","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4356e07e26c819aaf28872c09ac7d0a6f42a7b72","datavalue":{"value":{"entity-type":"item","numeric-id":2128806,"id":"Q2128806"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$3E02BD5E-81F1-4113-A216-5085506CF5CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bab2dfee53655d9cc8087a652185465cb178825e","datavalue":{"value":{"entity-type":"item","numeric-id":229754,"id":"Q229754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$ED36B43B-32E2-41D8-9C68-6C6B0A94F028","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"370dd048328bd35e66746fcb16650fb884273700","datavalue":{"value":{"time":"+2023-12-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6535381$AD20F686-6797-45F0-969E-3A4AF87E69FF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535381$315E3880-5D00-45D9-B1F9-70700AEB711A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535381$E560E493-16EC-4001-A09D-7222F0EE3BF4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c6b1251d1ea6af23da7e5b6a632342d3295b332a","datavalue":{"value":"7777328","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535381$0CCE6C27-8918-4F5E-A68F-EA59C0DAC2ED","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535381$01C6AF25-949A-4AB2-BB6E-A7D8633D739C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"312ed6497197fe722552104318fb5c842ebebed4","datavalue":{"value":"linear arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535381$EB5741E3-448D-4766-87E4-720A193966DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc37cf6bf1a4fd159f089028e999146e64828fa8","datavalue":{"value":"SMT","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535381$558739DB-9DF2-455B-96BD-048ECA8E7F90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8fe9e5661a5e008bfc5ffdb1b0c6a7e4f50f0322","datavalue":{"value":"quantified first-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535381$ED7BDEE2-98C8-472A-9A21-78FA6E06BDFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535381$77889869-F154-45B3-ACE3-7FBD38B75EB2","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":"Q6535381$7A6AB443-B4A9-45A1-B7A1-133200134E13","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4d2cf835bd77f96d03dced45b87a25996d25db85","datavalue":{"value":{"entity-type":"item","numeric-id":3158528,"id":"Q3158528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$14D838D2-2BB7-44A5-9A58-1DF4D4633966","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b1137cf78c4cad0e217f70ec321f2a593915490","datavalue":{"value":{"entity-type":"item","numeric-id":2751353,"id":"Q2751353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$B3EF459C-D55E-40DA-B5D1-6EA6C834331B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0b77a4e29d4d4695946227ed1b94a36174d5d1ac","datavalue":{"value":{"entity-type":"item","numeric-id":3454107,"id":"Q3454107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$B23E695B-0B84-405C-8221-B343F698D347","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f942974cb95506daf6c9f8a39d7c2f272d4faa3d","datavalue":{"value":{"entity-type":"item","numeric-id":2405239,"id":"Q2405239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$78B24490-2015-419E-A1A2-C495E2D7165E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f69b87d5186b1c7652ae794e22c225d266af5e9","datavalue":{"value":{"entity-type":"item","numeric-id":2305409,"id":"Q2305409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$73B84F71-6178-4B8F-B757-1A72FA2169FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bac46cadd391b69a8eb2eb17270bc333130444c","datavalue":{"value":{"entity-type":"item","numeric-id":6572540,"id":"Q6572540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$9E495ABE-1331-4ACC-9899-C50B58169663","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0b945f2840d1c2d5e46ba120dbb78eb02edc11ef","datavalue":{"value":{"entity-type":"item","numeric-id":5049017,"id":"Q5049017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$CE93953F-631D-49B1-B3DB-C80225F6EB95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27230ad583fb6c91e5e0b2ed04e15a2a06ba4a72","datavalue":{"value":{"entity-type":"item","numeric-id":3182526,"id":"Q3182526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$D8378E54-5A7B-4649-BE1C-EFD424352DFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d784e9c182b8b03311b797512c2cc1543da28ba","datavalue":{"value":{"entity-type":"item","numeric-id":5900709,"id":"Q5900709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$EE292E04-FE4D-45FB-B0B5-13343906EF5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"817ee4f5358d83048f7143c1c798ef96590ad2ef","datavalue":{"value":{"entity-type":"item","numeric-id":3608415,"id":"Q3608415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$39BB1F0E-E93B-454B-B93B-985ECBF3B6E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b4f714dbb33bba32b50777c1d77c1cb7ff5fe56","datavalue":{"value":{"entity-type":"item","numeric-id":3608773,"id":"Q3608773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$E7CB1EC1-6E28-4FC6-B350-4F46CCFA3A11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ddeddf292e13fd796c5c20e153357856b636f89","datavalue":{"value":{"entity-type":"item","numeric-id":2926635,"id":"Q2926635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$50842516-E908-46AE-8CC3-1A21C6A36308","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f14878b4342799995051ac9bc54cd21c98efc98","datavalue":{"value":{"entity-type":"item","numeric-id":2751359,"id":"Q2751359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$70C09D0B-D3A8-49A4-AFC4-B107794D521D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"727bf6303f28578cce92a2bdc6c0d3c263a24381","datavalue":{"value":{"entity-type":"item","numeric-id":2324203,"id":"Q2324203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$45F98B78-090F-46C3-B3EB-707A7142928E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d3f5b196c0df4a4076dad9269fa5296f4cdaaab","datavalue":{"value":{"entity-type":"item","numeric-id":1688537,"id":"Q1688537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$BFEB8772-D0C4-428A-ABF8-F372FC613610","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9297b6a91a7c29eb2b70ce4159ebd40915c17240","datavalue":{"value":{"entity-type":"item","numeric-id":2305435,"id":"Q2305435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$9C0C8BD5-699E-42FB-B210-90822DD4EE72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aa6750f3149d248c4e232f6fdbdc36d7bc86e39","datavalue":{"value":{"entity-type":"item","numeric-id":2920991,"id":"Q2920991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$249B26B8-A991-4192-A24D-41A8D9EE60B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f896fa3dc9f9364c6a3e5a4ed841544b0b726d19","datavalue":{"value":{"entity-type":"item","numeric-id":293311,"id":"Q293311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$80AD0A87-22B3-49DA-A059-BBB2D03B24D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d50b2a66f661d583355130e48334b74efaaf1f7d","datavalue":{"value":{"entity-type":"item","numeric-id":4249895,"id":"Q4249895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$86E6A170-2972-4FE2-A557-18899C7CFA8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e8c3a4c26c963f6c6f654bf4bf0d5a58922ee01","datavalue":{"value":{"entity-type":"item","numeric-id":4593023,"id":"Q4593023"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$4888553D-1581-446F-B62C-2CAC072A4461","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bad6694bc84bc7db2a7b91bbc531be7915baee7d","datavalue":{"value":{"entity-type":"item","numeric-id":3655193,"id":"Q3655193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d2c5bb21c9ba309b0024e3682e4c8238bcee9f75","datavalue":{"value":{"amount":"+0.7817951440811157","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":"Q6535381$84EEB0CE-8527-4B27-8D61-33DAE66FD147","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fa8e3a6abe8f8c4a26042826c88255c7940305fd","datavalue":{"value":{"entity-type":"item","numeric-id":3608415,"id":"Q3608415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"81967a79af019447ee38ab8870241ef3e5b56a88","datavalue":{"value":{"amount":"+0.7724915146827698","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":"Q6535381$3BD5C76F-5A13-40D8-94A9-02054CCEE981","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7fea8cffeb6abad3b55e3109223e71303a17a4d0","datavalue":{"value":{"entity-type":"item","numeric-id":5505559,"id":"Q5505559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"00ee5225b57696f8f70b6841ffc5834ac3b775a6","datavalue":{"value":{"amount":"+0.7626867890357971","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":"Q6535381$499A254B-6106-4335-B227-97FB7CA17A8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f92de1a09822e0e115caba8c3d664e95defabd96","datavalue":{"value":{"entity-type":"item","numeric-id":2185457,"id":"Q2185457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7ff5128b1152ccb999aade7918fac4a98198ec4f","datavalue":{"value":{"amount":"+0.7294318079948425","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":"Q6535381$F3447FB5-B799-462C-84D6-DBDFF62F2C4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"00058f037f22647676255159cc8be291fdf1cc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5505560,"id":"Q5505560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31f2710bff015c0dbef060e4897aeda1603745ad","datavalue":{"value":{"amount":"+0.727647602558136","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":"Q6535381$AFCB71C5-C7AA-4F08-AA15-5AD2C1A523DA","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535381$73C31E23-6F86-4742-AB8F-68CF3CB3146B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6535381","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6535381"}}}}}