{"entities":{"Q1581359":{"pageid":1592099,"ns":120,"title":"Item:Q1581359","lastrevid":78006218,"modified":"2026-05-06T10:33:29Z","type":"item","id":"Q1581359","labels":{"en":{"language":"en","value":"Automated deduction. A basis for applications. Vol. 2: Systems and implementation techniques"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1508656"}},"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":"Q1581359$0313607E-F9E6-4ECE-8F97-ECA9C7B72443","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9b93049f44ccbd51df990cabe941caea930b9c6f","datavalue":{"value":{"text":"Automated deduction. A basis for applications. Vol. 2: Systems and implementation techniques","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1581359$B7D9F29C-770C-49F7-991F-C6F01B584636","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"301a1e77f76e3ac138964abb3ac9b121f934a70e","datavalue":{"value":"0948.00014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1581359$77EF6746-C9D9-4D3D-9041-F1AB7A104589","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":"Q1581359$3F3B9973-2F9C-48C6-969F-5E35FAD20668","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":"Q1581359$D2402D19-C023-4F29-A1B4-9D85842BE886","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"018b72b523e5271a1c45b73dd940350f6ccb52c5","datavalue":{"value":"The articles of this volume will be reviewed individually. For Vol. 1 see Zbl 0948.00014.  Indexed articles:  \\textit{Reif, Wolfgang; Schellhorn, Gerhard; Stenzel, Kurt; Balser, Michael}, Structured specifications and interactive proofs with KIV, 13-39 [Zbl 0970.68149]  \\textit{Benl, Holger; Berger, Ulrich; Schwichtenberg, Helmut; Seisenberger, Monika; Zuber, Wolfgang}, Proof theory at work: Program development in the minlog system, 41-71 [Zbl 1015.68177]  \\textit{Strecker, Martin; Luther, Marko; von Henke, Friedrich}, Interactive and automated proof construction in type theory, 73-96 [Zbl 0970.68150]  \\textit{Ahrendt, Wolfgang; Beckert, Bernhard; H\u00e4hnle, Reiner; Menzel, Wolfram; Reif, Wolfgang; Schellhorn, Gerhard; Schmitt, Peter H.}, Integrating automated and interactive theorem proving, 97-123 [Zbl 0970.68151]  \\textit{Graf, Peter; Fehrer, Detlef}, Term indexing, 125-147 [Zbl 0970.68152]  \\textit{Fehrer, Detlef}, Developing deduction systems: The toolbox style, 149-166 [Zbl 0970.68153]  \\textit{Neugebauer, Gerd; Petermann, Uwe}, Specifications of inference rules: Extensions of the PTTP technique, 167-188 [Zbl 0973.68212]  \\textit{Kolbe, Thomas; Walther, Christoph}, Proof analysis, generalization and reuse, 189-229 [Zbl 0970.68154]  \\textit{B\u00fcndgen, Reinhard; G\u00f6bel, Manfred; K\u00fcchlin, Wolfgang; Weber, Andreas}, Parallel term rewriting with PaReDuX, 231-259 [Zbl 0973.68109]  \\textit{Schumann, Johann; Wolf, Andreas; Suttner, Christian}, Parallel theorem provers based on SETHEO, 261-290 [Zbl 0970.68155]  \\textit{Bornscheuer, Sven-Erik; H\u00f6lldobler, Steffen; Kalinke, Yvonne; Strohmaier, Antje}, Massively parallel reasoning, 291-329 [Zbl 1015.68541]  \\textit{Baaz, Matthias; Egly, Uwe; Leitsch, Alexander}, Extension methods in automated deduction, 331-359 [Zbl 0973.68214]  \\textit{Denzinger, J\u00f6rg; Fuchs, Matthias}, A comparison of equality reasoning heuristics, 361-382 [Zbl 0970.68156]  \\textit{Denzinger, J\u00f6rg; Dahn, Ingo}, Cooperating theorem provers, 383-416 [Zbl 0970.68157]","type":"string"},"datatype":"string"},"type":"statement","id":"Q1581359$1299214F-6D82-4991-B0ED-43090CD2F1D1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"342a6161f41187e2c595daa41b09cee10ab1ace9","datavalue":{"value":"00B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1581359$C00B17D2-A317-496E-8022-992016394D24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1581359$638B2600-C38D-432E-ACA5-25F5487896DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1581359$D2E9329D-B091-43C0-BD28-FF20FB802242","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1581359$9F4F15B2-6722-4251-8A20-68C633D0C6B2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ff29f2ba9844973a3dd70eeb6e8b11671de07d3d","datavalue":{"value":"1508656","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1581359$7631DF95-FF45-40CF-B99D-28FE9AF6AE8B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0bf4f74c129274c74f2df90abe98591d25c9e4a0","datavalue":{"value":"Automated deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1581359$9D1EEE17-E32C-4A1F-BD6D-C5B3FA72B7C0","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c845b927c7c8299e3e10848fbe9373f51ae3559b","datavalue":{"value":{"entity-type":"item","numeric-id":13461,"id":"Q13461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1581359$546BD555-3721-42E8-B33E-3396020D1E3D","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":"Q1581359$BD62A355-587A-41EA-A0B9-19BEDB18AA10","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4a436e39424d4de5050852a51ddc6f7407279cc9","datavalue":{"value":{"entity-type":"item","numeric-id":1581358,"id":"Q1581358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"75d2bb1eac061bf5a160ee020f39a0f7da301204","datavalue":{"value":{"amount":"+0.9469338","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1581359$CD814811-9ABB-4534-93AC-EDBA2CF05C0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"56dc41a482d581b626b7dd5659f501a4f829d4e8","datavalue":{"value":{"entity-type":"item","numeric-id":1581357,"id":"Q1581357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d5daf48ef9a9d590e2f601ab98769640f6ad22d0","datavalue":{"value":{"amount":"+0.94383895","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1581359$3EA5F813-A56F-47D8-927B-CB86E876DEAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13c39ceb87b78fa19ce5077c814a791a68af5067","datavalue":{"value":{"entity-type":"item","numeric-id":4941841,"id":"Q4941841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"538c35cdac8b44ad10f409704e02477524027fea","datavalue":{"value":{"amount":"+0.87914944","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1581359$1C765976-FEDB-4D09-8813-E14C62DB1127","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e2e9bc12af77f729148531e73535cb6003772aa5","datavalue":{"value":{"entity-type":"item","numeric-id":2724150,"id":"Q2724150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5b4902aa784e773e2617a6bdcd9f3878e5c5b644","datavalue":{"value":{"amount":"+0.8655464","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1581359$21617861-852F-40C2-B1FD-F87D45BF9E6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ebe565df6165b9510c766c488ed0bc020dc42945","datavalue":{"value":{"entity-type":"item","numeric-id":4317906,"id":"Q4317906"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1527bb7326c315faaeb212259ad90ba6e3bad8a0","datavalue":{"value":{"amount":"+0.86297125","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1581359$24B7D69D-0E33-4415-9592-4BEF5EE0580E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a1cfc853f4f5e9b8d94062b825701b06d4af5a08","datavalue":{"value":{"entity-type":"item","numeric-id":3738607,"id":"Q3738607"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f392cf3a9bcdda0e85d632186cb656f7c845e9ff","datavalue":{"value":{"amount":"+0.86171484","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1581359$019A011E-4815-40DA-8021-ACC9AC4E34F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"77229aad62351eaf3942d148080cf5957561f26c","datavalue":{"value":{"entity-type":"item","numeric-id":3829089,"id":"Q3829089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8d5975f6b4f9b224cc5143b1d97416c959b7aa2f","datavalue":{"value":{"amount":"+0.8611218","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1581359$60AB0AD3-9EBD-4AC1-A1E9-399A2FB227C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"acd3c744af8b6efaaaee01302a992e76d5e635c3","datavalue":{"value":{"entity-type":"item","numeric-id":1967066,"id":"Q1967066"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f0e341fcc129cdde6a0d92290957a744757955d2","datavalue":{"value":{"amount":"+0.860196","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1581359$1A9033B7-ED4C-499B-A8BB-0EEF2675D248","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"66acb868ea1a2aa0d1375cd1f0e361572a721f88","datavalue":{"value":{"entity-type":"item","numeric-id":4040458,"id":"Q4040458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0cab5d8608da0929e276d788ac020c3b957a6fac","datavalue":{"value":{"amount":"+0.8511869","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1581359$9F7C19B2-89F9-42FA-8A46-9F9388DF1F0A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automated deduction. A basis for applications. Vol. 2: Systems and implementation techniques","badges":[]}}}}}