{"entities":{"Q1697332":{"pageid":1708073,"ns":120,"title":"Item:Q1697332","lastrevid":68207418,"modified":"2026-04-12T22:08:50Z","type":"item","id":"Q1697332","labels":{"en":{"language":"en","value":"Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6840665"}},"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":"Q1697332$C4A5C403-14DE-4B91-8889-3F036D43E04D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6360b18fa2e3e777fead4b05c93cb0230d9d628a","datavalue":{"value":{"text":"Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1697332$1B81E852-83DE-45B8-A361-EE8620871F02","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"43837fe0e717236891f58f0a2f8ec19a86305fa5","datavalue":{"value":"1387.03007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1697332$C83209F6-E4DA-4DA8-8BEA-C01C1A984868","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"89f7d4fe21e22bb47f8af2be9af5b124c53cf779","datavalue":{"value":{"entity-type":"item","numeric-id":274401,"id":"Q274401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$047474D1-0569-4B33-BFDF-47E08D2357A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1ce8850632b90b69a6c289735cc288ece6fb9e1a","datavalue":{"value":{"entity-type":"item","numeric-id":352975,"id":"Q352975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$8C582DF5-827F-495F-8DE6-433411FA39D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"625e9c8b1a752241c65bb5aab85211ac194e9690","datavalue":{"value":{"entity-type":"item","numeric-id":606911,"id":"Q606911"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$A8CDFC9E-2CAD-484C-BDB8-37FDD80F7BFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"588ee65877f0d3e81836f8c13b96426bc0fd83a2","datavalue":{"value":{"entity-type":"item","numeric-id":487631,"id":"Q487631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$2A96DE87-B368-4627-A7CE-2FA75D2761CA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"784d2dc06e2a3bb008e6a3a15801a0f0231d6262","datavalue":{"value":{"entity-type":"item","numeric-id":65161,"id":"Q65161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$5A25D761-BDA2-4B62-AE55-652E62CC76F1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f287bdf783f35305500eed531b35fb7e704778e5","datavalue":{"value":{"time":"+2018-02-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1697332$968E11CC-CD05-455A-99F1-E13AAD323240","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"678beee0128c02acea4a89908220fa05e5248975","datavalue":{"value":"Many-valued (propositional) logics have been studied for many years and important examples are the logics by G\u00f6del and \u0141ukasiewicz, which come as logics with finitely many or infinitely many truth values, for instance, as finitely many integer values, or as rational values between 0 and 1 (both included) in the finite case, or as all the real numbers in the interval \\([0,1]\\) in the infinite case. The connectives are defined, for instance, in G\u00f6del logics, so that conjunction corresponds to the minimum and disjunction to the maximum function. In addition to these two families of logics, the paper studies product logic in which the truth value of conjunction is defined as the product of the component values. Properties and calculi for such logics have been studied since the early 20th century. More towards the end of the 20th century actual theorem provers have been developed. The authors study the application of general purpose SMT solvers as theorem provers for these many valued logics. SMT solvers are satisfiability modulo theories solvers and have successfully been used in many areas. The authors give straightforward translations from problems of many-valued logics to formulations readable by SMT solvers. Essentially, each propositional logic variable can take only one of the different truth values, the connectives correspond to functions on numbers, and the formulae are translated into arithmetic expressions. Then, satisfiability is checked. If no model is found then the formulae are unsatisfiable.  The efficiency of the approach is tested with respect to certain benchmark problems and different encodings are compared. The tests are done for finite numbers of truth values from 3 through 21 with 5 to 50 variables. For some tests with infinite logics, the number of variables is 500. The general approach has a very good performance. The usual pattern of SAT solvers is reproduced that with a small number or a high number of clauses the problem is typically easily shown to be solvable or unsolvable, respectively; and that in the transition area between solvability and unsolvability the computational complexity is high.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1697332$7B9BB3D4-838B-4675-A2DF-E949335B1176","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"80e987276e122a41f9b91b8b2fac713fac5a8dbb","datavalue":{"value":{"entity-type":"item","numeric-id":504392,"id":"Q504392"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$30E3490B-148A-4C2E-B80B-5D1A7751B82B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1697332$1CF2CFE1-E020-4112-A7C5-A2B6758B269A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"bf715f882d7ad0c07303aa3e6e3ac3725da52515","datavalue":{"value":"03B50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1697332$805FF329-9D5E-4F7F-8AA7-1FC3917B15A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1697332$8AF0D825-0E45-4754-B41A-B3A0E3833295","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bdf9dfa91fec658218e41ce3f2435f265450c59d","datavalue":{"value":"6840665","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1697332$6DD3163D-6063-4AB8-94F3-ABE2F09EF309","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4ef70beaae1d548d6d32bb08ac016112f60132c8","datavalue":{"value":"multiple-valued logics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1697332$AD49D3CB-CF13-4E26-9234-A658301B1FC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d1585ca8380d459cc6fef1e6ce4a61850ace366","datavalue":{"value":"automated theorem provers","type":"string"},"datatype":"string"},"type":"statement","id":"Q1697332$C6380E1D-1BBB-470F-AD0E-CABA7EF184ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc37cf6bf1a4fd159f089028e999146e64828fa8","datavalue":{"value":"SMT","type":"string"},"datatype":"string"},"type":"statement","id":"Q1697332$D71F5735-6886-472D-A17D-BF233F87D1A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"82a3ae76578a4d5d88a56c0f8805a0ae043ff05e","datavalue":{"value":"benchmarks","type":"string"},"datatype":"string"},"type":"statement","id":"Q1697332$118457A7-E4A0-4816-AD41-2C9241BC6673","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$E6C8EB89-FFC1-4AC9-A785-5AF56A8EBC3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"eb2681abb3bba434415e4fc739b2d99830a88472","datavalue":{"value":{"entity-type":"item","numeric-id":16731,"id":"Q16731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$A1C9B0AE-2D61-482E-B083-7171F8CC9185","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"85575b60ef4d0a8413d3c895be2530b8915bc3fb","datavalue":{"value":{"entity-type":"item","numeric-id":16612,"id":"Q16612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$7DAD5A3C-BC37-40CE-984E-05BB6DF14310","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$58D218B4-85BF-40D2-AB24-5C6A8C2518E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4e14f074ee164d24d4b809703cdb143cd929239f","datavalue":{"value":{"entity-type":"item","numeric-id":36167,"id":"Q36167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$F9B89A14-9832-4A23-91EB-38A275171E06","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":"Q1697332$4D6EDE81-4D23-4048-B850-6BB3BE08E0E5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"bd1bcdf85aa6ac823f20fd28ec8aeb0405e4b43b","datavalue":{"value":"https://doi.org/10.1016/j.fss.2015.04.011","type":"string"},"datatype":"url"},"type":"statement","id":"Q1697332$7DB9B995-9B09-4576-A1AE-E598B3F67E25","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"cda8ce7e2fae680186616fa074bbb774dd0bd9c4","datavalue":{"value":"W2040193103","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1697332$EDB3CD5E-456B-433E-9F96-6A54F9B97F4C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"67cf68921371c49adfce9cf0f6418582fd911685","datavalue":{"value":{"entity-type":"item","numeric-id":816857,"id":"Q816857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$56A0C0C5-3037-443C-9B8D-8898C6CC7F0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"75695a8beeb327509bdf451e6c8d3a3f23213ec0","datavalue":{"value":{"entity-type":"item","numeric-id":1897558,"id":"Q1897558"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$C221606E-BACA-4321-802F-04BCA795D0E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9989951ff92c915f90cbf709c10f8e9530978961","datavalue":{"value":{"entity-type":"item","numeric-id":2701980,"id":"Q2701980"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$B5D4617F-F095-4C74-9C87-9EC3EE3D49A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"efb8206136bb1a3e3206c15b8c3fd64eecf1b0ab","datavalue":{"value":{"entity-type":"item","numeric-id":2757760,"id":"Q2757760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$E2C64E7D-148A-48D2-A6C1-42AAEA78CDB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea01880b69c90c2b0398b4f30dea89c1d6a90b9d","datavalue":{"value":{"entity-type":"item","numeric-id":3503741,"id":"Q3503741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$0E250CB4-6F11-4824-A567-5A8F8FD77C5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9f421884f879ae4e0048a14b487c578b45714b0b","datavalue":{"value":{"entity-type":"item","numeric-id":1307301,"id":"Q1307301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$B28F23E5-A680-4653-96EC-0EA1AD962F7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85d15b281639a533f93923258f76c1790cae10de","datavalue":{"value":{"entity-type":"item","numeric-id":2519539,"id":"Q2519539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$CCD87D69-3D0F-49EA-B5A0-7CF9B88B8AF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2894a726d38017dcebd287aa2e92de0e26e04dcd","datavalue":{"value":{"entity-type":"item","numeric-id":4323008,"id":"Q4323008"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$DA741BD4-E8F0-49A0-87DE-1511ACA42897","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7516fc65ecac37755fe011fe1711991dc2a48599","datavalue":{"value":{"entity-type":"item","numeric-id":3184605,"id":"Q3184605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$FA2C7963-F07B-4645-A72B-1BAD9ABFEF33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4990d1da40f41df63d1b1cf33b30e19f9a38eba0","datavalue":{"value":{"entity-type":"item","numeric-id":5705945,"id":"Q5705945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$58BEFB83-23CB-4EAD-B81E-F93198AE83B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dfee219cc0c5fd53fb1efbec9c727171ee1defd4","datavalue":{"value":{"entity-type":"item","numeric-id":1868241,"id":"Q1868241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$8B5CA7C6-78C6-421D-8BC6-A80E013B8AE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e1410ecec3958d62bfe99f41a838a65fe28d2a62","datavalue":{"value":{"entity-type":"item","numeric-id":352963,"id":"Q352963"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$BD57DFE5-BF5A-4455-A7C0-B58334249B45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"569927fbe93407529f06d41b68d2ef6209ff2db6","datavalue":{"value":{"entity-type":"item","numeric-id":1924752,"id":"Q1924752"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$0CB4CA91-D413-4F2A-B3FA-73C87F44EA1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4dca4e376739e90cb915f405694b6ab7c37e738c","datavalue":{"value":{"entity-type":"item","numeric-id":773072,"id":"Q773072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$6E124B6A-4673-45BB-AE1D-EA568D792FE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7b1ef4c8566673a8a5c94d00ea3fc5ee04078d8e","datavalue":{"value":{"entity-type":"item","numeric-id":3506045,"id":"Q3506045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$379F663E-C434-4ED4-AAAF-7459091A7F72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e6a5a8514c16b27cd5b5f9310f33915f3161eb75","datavalue":{"value":{"entity-type":"item","numeric-id":4512929,"id":"Q4512929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1697332$77E6948E-C023-4C0C-8BAA-C8EF6AB9495B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e8611ffa9ff0b599368492c2720c88f8e24f193f","datavalue":{"value":"10.1016/J.FSS.2015.04.011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1697332$73639E37-1C8D-4A4F-9CCC-A72804197DA5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c71f74b44fa2dc93a921567998bd6aaf85c32fb7","datavalue":{"value":{"entity-type":"item","numeric-id":2751372,"id":"Q2751372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e9d66cd973858b956932ddae61f450a7e40a6863","datavalue":{"value":{"amount":"+0.92886597","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1697332$5A8051D0-C931-45E8-B49F-6423DF3E449D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fc47d5d7bda03aa5f81bd804c6f977624a87a40a","datavalue":{"value":{"entity-type":"item","numeric-id":4289327,"id":"Q4289327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d01d544e1eee9f7ece11fd492cb206217f63a5f5","datavalue":{"value":{"amount":"+0.92815286","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1697332$6CF7D018-7C25-421E-818D-484E3B791957","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"af54a7870ca0d13931e6592961d66440dbdf3adc","datavalue":{"value":{"entity-type":"item","numeric-id":4380155,"id":"Q4380155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7d73fc368e1494a785f2a2dbffa3db8a03edfbd","datavalue":{"value":{"amount":"+0.92804617","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1697332$D92CB24A-50C5-47BD-9ED0-3ED86BE13B04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0a53649f9e1f1ac44c131be79504c0ce2156903f","datavalue":{"value":{"entity-type":"item","numeric-id":1272603,"id":"Q1272603"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dbcce1313e6d93c2f569a48897995efb03b7f85a","datavalue":{"value":{"amount":"+0.91847664","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1697332$884C4C80-C843-4575-BB6A-9547894CE474","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"88123805737055ce53c54ee2f23d3afc276626d8","datavalue":{"value":{"entity-type":"item","numeric-id":5881275,"id":"Q5881275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"16c1405810a5f451eda03ebae653826b91f89e29","datavalue":{"value":{"amount":"+0.9137321","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1697332$BEF2CCE1-31CD-4346-AAEF-BD7445785AE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"be055b314b934e40a3d60a53755f0ad33613a859","datavalue":{"value":{"entity-type":"item","numeric-id":4212163,"id":"Q4212163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2e62c11bf670e8c77a82a975837889287dac677a","datavalue":{"value":{"amount":"+0.8968615","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1697332$88AFB167-0A98-4E4E-AB7E-8C76BB8EC4FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d9f84eb722ed0dd098a9ae5e18a01ba6fb1ba759","datavalue":{"value":{"entity-type":"item","numeric-id":3726086,"id":"Q3726086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"612e34638bdb95a2f1833bce3feedb13cdd9ac64","datavalue":{"value":{"amount":"+0.89343035","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1697332$0D5B3470-96E8-4284-9894-5E43C5AF4DDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0db453cf8548b5472a0f96e220cc76294e6cf410","datavalue":{"value":{"entity-type":"item","numeric-id":4544342,"id":"Q4544342"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f46f6c68610bcb960b2eecb3db80858ba4d0cf64","datavalue":{"value":{"amount":"+0.8913151","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1697332$1ABA390C-9399-48AC-9557-C4740BC1843D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6021f70475ec456907b1059df7b91dfa79a09357","datavalue":{"value":{"entity-type":"item","numeric-id":1897558,"id":"Q1897558"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"58a2ec2922680ffb0770edeaf718ea0154df32f0","datavalue":{"value":{"amount":"+0.8904349","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1697332$5C34A65C-6DD6-4A2A-9ECC-4E07C9A5BDA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"455dc3c61ba2eacddf023338317bf5e053474959","datavalue":{"value":{"entity-type":"item","numeric-id":6488523,"id":"Q6488523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"81aa6ad07c10f80348b320b53fbee09d264d7122","datavalue":{"value":{"amount":"+0.89037263","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1697332$020113D5-79B7-40A5-AFB4-F75B7E9F986F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Automated_theorem_provers_for_multiple-valued_logics_with_satisfiability_modulo_theory_solvers"}}}}}