{"entities":{"Q1389909":{"pageid":1400649,"ns":120,"title":"Item:Q1389909","lastrevid":43076129,"modified":"2025-07-17T12:02:41Z","type":"item","id":"Q1389909","labels":{"en":{"language":"en","value":"Automated deduction - CADE-15. 15th international conference, Lindau, Germany, July 5--10, 1998. Proceedings"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1174014"}},"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":"Q1389909$85295C41-A98E-40BF-9F91-DE59F2EA7A44","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e5f4247ea3842bf8018734e0fe5292be002b7781","datavalue":{"value":{"text":"Automated deduction - CADE-15. 15th international conference, Lindau, Germany, July 5--10, 1998. Proceedings","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1389909$8AD07523-A427-4EC2-8A91-23F7DC601DF7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6ae0d3b370e1ded05bb48038e0f548ece28367c7","datavalue":{"value":"0892.00047","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1389909$E7FA96F1-BEDA-4B42-B8A5-834AC1E509A0","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1389909$9C835F45-BBDC-4562-BD6E-0AC5042C51FB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"abaf01d431243fb03e12c2c18b9d3362e56420e2","datavalue":{"value":{"time":"+1998-07-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":"Q1389909$5C56E4ED-14CA-4DF7-8EC7-D2F31ECA7D3B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"43252f04d5069714b46956a2e10f40c1a790042a","datavalue":{"value":"The articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1415.68038].  Indexed articles:  \\textit{Fleuriot, Jacques D.; Paulson, Lawrence C.}, A combination of nonstandard analysis and geometry theorem proving, with application to Newton's Principia, 3-16 [Zbl 0924.03022]  \\textit{F\u00e8vre, St\u00e9phane; Wang, Dongming}, Proving geometric theorems using Clifford algebra and rewrite rules, 17-32 [Zbl 0924.03021]  \\textit{Benzm\u00fcller, Christoph; Kohlhase, Michael}, Extensional higher-order resolution, 56-71 [Zbl 0928.03004]  \\textit{Pagano, Bruno}, X. R. S. : Explicit reduction systems -- A first-order calculus for higher-order calculi, 72-87 [Zbl 0924.03047]  \\textit{Boudet, Alexandre; Contejean, Evelyne}, About the confluence of equational pattern rewrite systems, 88-102 [Zbl 0924.03041]  \\textit{Beeson, Michael}, Unification in lambda-calculi with if-then-else, 103-118 [Zbl 0924.03018]  \\textit{Waldmann, Uwe}, Superposition for divisible torsion-free abelian groups, 144-159 [Zbl 0924.03026]  \\textit{Bachmair, Leo; Ganzinger, Harald}, Strict basic superposition, 160-174 [Zbl 0924.03017]  \\textit{Bachmair, Leo; Ganzinger, Harald; Voronkov, Andrei}, Elimination of equality via transformation with ordering constraints, 175-190 [Zbl 0926.03006]  \\textit{de Nivelle, Hans}, A resolution decision procedure for the guarded fragment, 191-204 [Zbl 0927.03027]  \\textit{Ohlbach, Hans J\u00fcrgen}, Combining Hilbert style and semantic reasoning in a resolution framework, 205-219 [Zbl 0928.03011]  \\textit{Crary, Karl}, Admissibility of fixpoint induction over partial types, 270-285 [Zbl 0924.03019]  \\textit{Sch\u00fcrmann, Carsten; Pfenning, Frank}, Automated theorem proving in a simple meta-logic for LF, 286-300 [Zbl 0924.03024]  \\textit{Ohta, Yoshihiko; Inoue, Katsumi; Hasegawa, Ryuzo}, On the relationship between non-Horn magic sets and relevancy testing, 333-348 [Zbl 0926.03008]  \\textit{Th\u00e9ry, Laurent}, A certified version of Buchberger's algorithm, 349-364 [Zbl 0924.03025]  \\textit{Nonnengart, Andreas; Rock, Georg; Weidenbach, Christoph}, On generating small clause normal forms, 397-411 [Zbl 0924.03023]  \\textit{Horton, J. D.; Spencer, Bruce}, Rank/activity: A canonical form for binary resolution, 412-426 [Zbl 0926.03007]","type":"string"},"datatype":"string"},"type":"statement","id":"Q1389909$84A7F946-B943-45F8-B919-33588E55854C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6f2c17db95e93f9a5a19ff6c68b3a1df8b0c021e","datavalue":{"value":"00B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1389909$6F1EC7F9-0044-483A-943C-98BCE77A258C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f1971b12f93143b2604d15a1750f495d71fae62d","datavalue":{"value":"03-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1389909$DDDFF4CB-2141-42B5-9045-8E3E79B35924","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1389909$13C74211-F5B3-406F-B17A-2F53D8FB03E1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fd91383b794c6cb5df33671aae5afefa814d30e6","datavalue":{"value":"1174014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1389909$8C380C7F-26F5-401F-B61A-2680992A4743","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2e6b3499db8436fac016d9a7f90c829fb3b4ae3d","datavalue":{"value":"Lindau (Germany)","type":"string"},"datatype":"string"},"type":"statement","id":"Q1389909$F805DFB7-8C9A-4CB2-881C-0A8975D662E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5c4c4bb5a86a0fdf66f908b603f2f6975f5ef6fc","datavalue":{"value":"Proceedings","type":"string"},"datatype":"string"},"type":"statement","id":"Q1389909$B98CA100-F544-4FC3-9B9F-FFAC2C185BF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d83ae477e518ffecea78688f13a2aaaeca13299","datavalue":{"value":"Conference","type":"string"},"datatype":"string"},"type":"statement","id":"Q1389909$2D6C6A05-85BF-4DAE-9691-E4C32BE1D2F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3ef59ecdd8e09dd11bf544780b60e72b7f8ba84d","datavalue":{"value":"CADE-15","type":"string"},"datatype":"string"},"type":"statement","id":"Q1389909$F20F9D0E-E825-4DAE-8C25-57AC84AFE1C0","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":"Q1389909$160A6798-A32B-4D8F-BC8A-D1F24CECC535","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"674d1c64447f4d04406ffddf86857469324fd744","datavalue":{"value":"10.1007/BFB0054239","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1389909$EB5AE14C-1714-4738-AB45-9ADACEB92B45","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1389909","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1389909"}}}}}