{"entities":{"Q1581357":{"pageid":1592097,"ns":120,"title":"Item:Q1581357","lastrevid":78006200,"modified":"2026-05-06T10:33:28Z","type":"item","id":"Q1581357","labels":{"en":{"language":"en","value":"Automated deduction. A basis for applications. Vol. III: Applications"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1508648"}},"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":"Q1581357$5108AE8F-1532-41BE-B3E0-2784D52C90CB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d07020040d6c0f4b4516d55f8953067fb4b9e546","datavalue":{"value":{"text":"Automated deduction. A basis for applications. Vol. III: Applications","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1581357$385AE447-FF6F-4C42-BD50-99AB77CDCDF7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1a4dc024142e95dc1634cbd248af92de560dab2f","datavalue":{"value":"0954.00010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1581357$B1296F7F-AA5A-42E4-AA8E-54A622E29569","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"059d67558a7cf3b6a152997163f7ee7dfecaafdd","datavalue":{"value":{"entity-type":"item","numeric-id":232650,"id":"Q232650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1581357$438A00B5-EA36-43D8-B3B8-D238E1886FEF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4d9916717d2b77c002542ea70b3a652323b0a04c","datavalue":{"value":{"time":"+2000-09-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1581357$0BF61A73-ECE5-41D5-8773-2596AC43B3F7","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4d10d15137ded9316c80554988023df48e4ee8a9","datavalue":{"value":"The articles of this volume will be reviewed individually.  Indexed articles:  \\textit{Dahn, Ingo}, Lattice-ordered groups in deduction, 9-29 [Zbl 0969.03021]  \\textit{Stuber, J\u00fcrgen}, Superposition theorem proving for commutative rings, 31-55 [Zbl 0970.03022]  \\textit{Ohlbach, Hans J\u00fcrgen; K\u00f6hler, Jana}, How to augment a formal system with a Boolean algebra component, 57-75 [Zbl 0967.03011]  \\textit{Kerber, Manfred}, Proof planning: A practical approach to mechanized reasoning in mathematics, 77-104 [Zbl 0967.03010]  \\textit{Kreitz, Christoph}, Program synthesis, 105-134 [Zbl 0972.68514]  \\textit{Giesl, J\u00fcrgen; Walther, Christoph; Brauburger, J\u00fcrgen}, Termination analysis for functional programs, 135-164 [Zbl 0972.68031]  \\textit{Schellhorn, Gerhard; Ahrendt, Wolfgang}, The WAM case study: Verifying compiler correctness for Prolog with KIV, 165-194 [Zbl 0977.68017]  \\textit{Dahn, Ingo; Schumann, Johann}, Using automated theorem provers in verification of protocols, 195-224 [Zbl 0972.68011]  \\textit{Reif, Wolfgang; Schellhorn, Gerhard}, Theorem proving in large theories, 225-241 [Zbl 0972.68520]  \\textit{Stolzenburg, Frieder; Thomas, Bernd}, Analyzing rule sets for the calculation of banking fees by a theorem prover with constraints, 243-264 [Zbl 0972.68144]  \\textit{Fischer, Bernd; Schumann, Johann; Snelting, Gregor}, Deduction-based software component retrieval, 265-292 [Zbl 0972.68042]  \\textit{B\u00fcndgen, Reinhard}, Rewrite based hardware verification with ReDuX, 293-316 [Zbl 0972.68145]","type":"string"},"datatype":"string"},"type":"statement","id":"Q1581357$5ACCCEF9-1C9B-464A-ACB8-2540E307A938","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"342a6161f41187e2c595daa41b09cee10ab1ace9","datavalue":{"value":"00B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1581357$2176DAB5-ED37-4E32-8BDB-0621876C1EB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f1971b12f93143b2604d15a1750f495d71fae62d","datavalue":{"value":"03-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1581357$07EBC952-4396-4616-A40F-FFEEECCC510F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1581357$0CB3B878-B7EC-4FCC-A0EB-BC579D666CE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1581357$8CAA90B0-899A-4680-84DD-4008E9F306C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1581357$F1C61CC1-8809-4C62-8272-A83E80DEF805","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a0560543bad4ed6bb72f7ba9c2fb29e0efd46650","datavalue":{"value":"1508648","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1581357$D9CB9223-21B2-48B5-A12D-CA7BF30D8B18","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0bf4f74c129274c74f2df90abe98591d25c9e4a0","datavalue":{"value":"Automated deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1581357$25DB126D-D285-4799-B7C9-1AC4BF74E9C8","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":"Q1581357$529C4D64-9EF6-4A9A-8B19-31D7F41D8CB6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automated deduction. A basis for applications. Vol. III: Applications","badges":[]}}}}}