{"entities":{"Q783254":{"pageid":785103,"ns":120,"title":"Item:Q783254","lastrevid":64301184,"modified":"2026-04-11T18:56:45Z","type":"item","id":"Q783254","labels":{"en":{"language":"en","value":"Dealing with negative conditions in automated proving: tools and challenges. The unexpected consequences of Rabinowitsch's trick"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7232901"}},"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":"Q783254$8B1634C3-F8F9-4160-93A0-94718797017C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a5df39bb4cd750825575d4d673df78b6afe560cc","datavalue":{"value":{"text":"Dealing with negative conditions in automated proving: tools and challenges. The unexpected consequences of Rabinowitsch's trick","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q783254$6488BD8C-529E-4C04-98B5-F3083C89B86E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1e95d1c1811e43965f97c94ee14b222f61d64e48","datavalue":{"value":"1453.68209","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q783254$0CFB5016-0E35-453E-BCE9-FA136B969731","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1324e0a5db7963679ba50f0ef3f33006b70feb98","datavalue":{"value":{"entity-type":"item","numeric-id":417513,"id":"Q417513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$7BB144AC-5AC3-4B8E-9466-31AB9B02FA15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f38af8ba5976f05f33649fa7d838417db77b84a2","datavalue":{"value":{"entity-type":"item","numeric-id":783253,"id":"Q783253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$2BAEFC95-586E-4BA9-A711-53A1032BFC0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"59d44f3333e2f9dff43dcfba05e4d5cf19ad4778","datavalue":{"value":{"entity-type":"item","numeric-id":286778,"id":"Q286778"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$454EF160-806B-4C1A-BB8B-C5B89C0DA3B1","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"5478ede943fb911760ea7d60e42b6d499b786ce8","datavalue":{"value":{"entity-type":"item","numeric-id":259732,"id":"Q259732"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$65CBF0AE-9BE6-4985-81CD-46D58C99C5B1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9a0601910279d3cd6e6f45d9bc6255b7f45b2ef8","datavalue":{"value":{"time":"+2020-08-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q783254$9F29D114-091E-46C6-ABCD-841B0DE465CD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q783254$E9AF285F-BEB0-4813-9777-402B6BCF0F2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"65ef089ab6dd31e83c3611c992a3cfd8973b58bb","datavalue":{"value":"14Q20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q783254$EFB2700F-6123-4571-9646-3D00B70644B9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5164f23a4505131f7ad14f41438fdf1652aa38f7","datavalue":{"value":"7232901","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q783254$BA1120F7-0146-445E-BAE7-63AF05CFB06A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e5cb0ee4d64eeecc8a076e8bdecb84e8ad122015","datavalue":{"value":"automated proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q783254$8E03C0FA-4ACB-4434-81F2-3E294AB59D5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3e80597159aa4300afd51c237340620818697197","datavalue":{"value":"automated discovery","type":"string"},"datatype":"string"},"type":"statement","id":"Q783254$EBBDAFD4-73C7-4463-8F31-5DCBC159E20B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bf6baecdff04b766340aa66602224b795281b56b","datavalue":{"value":"non-degeneracy conditions","type":"string"},"datatype":"string"},"type":"statement","id":"Q783254$A6664399-CFF1-4172-BE0B-CEDF13D1C769","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9dca20729e130026ebee88b156ab795c31b38cd6","datavalue":{"value":"Rabinowitsch's trick","type":"string"},"datatype":"string"},"type":"statement","id":"Q783254$29C7D82F-DBC8-4196-8EB4-4086A46131F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b6739fba16acf61162defd709061e3d3f6a05da4","datavalue":{"value":"saturation","type":"string"},"datatype":"string"},"type":"statement","id":"Q783254$9CF78BA3-B70B-42AE-9591-057C01859E9F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ef03848f41f59da431665c121436ac0a6bc94ac2","datavalue":{"value":{"entity-type":"item","numeric-id":13610,"id":"Q13610"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$9BEEA1C7-8C8F-4A8D-83B3-43EAE6F00789","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ebe2977d14a6006fa56768c0bbf4b09337d85306","datavalue":{"value":{"entity-type":"item","numeric-id":16387,"id":"Q16387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$7D945AFA-A842-47DC-87CF-BD1EBF127DCB","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":"Q783254$705FEE61-E15A-40E4-A13A-93976D9DB558","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d55393115c44d7cdc8a3dacb8dc0411fc9c85684","datavalue":{"value":"https://doi.org/10.1007/s13398-020-00874-8","type":"string"},"datatype":"url"},"type":"statement","id":"Q783254$EA3070D7-AB46-4D28-BFD1-859A831C016B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"664c87157735c8614572d3bcfdae27c1ddd6cc38","datavalue":{"value":"W3038289190","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q783254$2476D667-516B-45C7-8EAA-BB67691724B1","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9fd657fd4badf9c504d4532e58cfc4c53d43f2f","datavalue":{"value":{"entity-type":"item","numeric-id":5270196,"id":"Q5270196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$33F247EA-FC07-43C1-8C5F-EBF5585045C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a7455fc19ea84dbadf783a600d678ef33c290b6","datavalue":{"value":{"entity-type":"item","numeric-id":2819196,"id":"Q2819196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$070A398E-F6FB-40A0-8884-BBAE4CC531D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99b621ae7a796500fab9bf1938f7368cca8e38c2","datavalue":{"value":{"entity-type":"item","numeric-id":294370,"id":"Q294370"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$490CB3C6-D154-44DF-805E-824C347486D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"953e262a3244da8dda3464b2c191683b0afa692b","datavalue":{"value":{"entity-type":"item","numeric-id":3994509,"id":"Q3994509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$22D110CA-A01B-460F-BDBA-E94689841D32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf7e5ea8b887807f5a5d06a897412368d42a81e7","datavalue":{"value":{"entity-type":"item","numeric-id":5245268,"id":"Q5245268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$B50D59FA-7233-42E2-81D4-176624648778","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"61d81add882687483fd918df0010fcaf5b17ef28","datavalue":{"value":{"entity-type":"item","numeric-id":846167,"id":"Q846167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$4EB0D52D-C281-46E0-B525-96661D0361D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66f1b17812e6037d2b7d557b0a7606920332b887","datavalue":{"value":{"entity-type":"item","numeric-id":1124373,"id":"Q1124373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$322457AB-5897-4D11-BB9E-BC0A2B5B8985","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e7944f6e0c00248d4828a0ee37728d762d15cd6","datavalue":{"value":{"entity-type":"item","numeric-id":4610007,"id":"Q4610007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$606AC610-69FD-4244-9F4C-6DCA7A8DAD18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"31385ef3ca1eb53ed08bbfa48b8b91d2510acbaf","datavalue":{"value":{"entity-type":"item","numeric-id":4282674,"id":"Q4282674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$E1B67467-F30F-4013-9D6B-02B2CF605E9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37dc9d079f62f11e11b3699725f6db9b5cafdc26","datavalue":{"value":{"entity-type":"item","numeric-id":2229890,"id":"Q2229890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$B30D8FCF-4506-4D5C-8F24-5F7B5ECAE74A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"236ff075b6336e5a62a73c551fd46afb75eb22f7","datavalue":{"value":{"entity-type":"item","numeric-id":1808565,"id":"Q1808565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$A960A380-5363-45A9-ADED-744F32671EDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04f6f29cd2605e0323c7157f555ad2ecad61386b","datavalue":{"value":{"entity-type":"item","numeric-id":2912124,"id":"Q2912124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$BDB69EF9-7C54-473F-AE4F-7BC51228A2D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4d57db4d3216bc53e46ae99a268680181eb65b5a","datavalue":{"value":{"entity-type":"item","numeric-id":4153620,"id":"Q4153620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$924A8A77-492A-4BD4-97F9-7CE44A569C9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb831cf68ca0065f258dd35b1cfb7fc712479f89","datavalue":{"value":{"entity-type":"item","numeric-id":1701040,"id":"Q1701040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q783254$4D30FA84-0D5F-4671-A04F-BCA419CF0A73","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d6f0ffdcc4e37c851ad3bc6827157843884bf1f5","datavalue":{"value":"10.1007/S13398-020-00874-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q783254$275BEA85-65DB-4A77-B3AA-1A32D23F58B1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6a4e06313012192d035d58fc6b4bcc1469b28cdd","datavalue":{"value":{"entity-type":"item","numeric-id":4610007,"id":"Q4610007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f54c6122808dd156db5051324326b48b9eed1931","datavalue":{"value":{"amount":"+0.7007936239242554","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":"Q783254$01A3365B-9E59-4F58-9603-C665273E4DBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4542d4f6ee9ed97205b6e68ed988ac4f3df1a721","datavalue":{"value":{"entity-type":"item","numeric-id":4531856,"id":"Q4531856"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f7c4bbfe2142b69fdc7bd54fc60a15ffbe60977","datavalue":{"value":{"amount":"+0.6974920034408569","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":"Q783254$65806DF8-DD10-4930-A83C-C835F88A4D8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"71f3871c91d193182f24e1450a792f7ef1c194e7","datavalue":{"value":{"entity-type":"item","numeric-id":4332419,"id":"Q4332419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0a83d7e72f3531c249772aa590fc7d6edbb0300e","datavalue":{"value":{"amount":"+0.6933678984642029","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":"Q783254$4127AC81-0E7D-481F-9465-C5091170D36D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0c0be4ae12b77e548190d701dabce4695d6b5da7","datavalue":{"value":{"entity-type":"item","numeric-id":1272610,"id":"Q1272610"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d14a8f7384d5bb33f43d2d3a51228bb3620448d","datavalue":{"value":{"amount":"+0.6933673620223999","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":"Q783254$D58B82D8-C27B-4D74-BA26-CFD58B9924BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c38ed7db4da68b169366d285fc7baaf4b267fa11","datavalue":{"value":{"entity-type":"item","numeric-id":5490283,"id":"Q5490283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0cffb54eb297d7e5af2844c8dda85b3c1fb90bee","datavalue":{"value":{"amount":"+0.6836646199226379","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":"Q783254$7AD1CCD5-D2C1-4582-89E0-00442AD7474D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Dealing with negative conditions in automated proving: tools and challenges. The unexpected consequences of Rabinowitsch's trick","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Dealing_with_negative_conditions_in_automated_proving:_tools_and_challenges._The_unexpected_consequences_of_Rabinowitsch%27s_trick"}}}}}