{"entities":{"Q1613678":{"pageid":1624418,"ns":120,"title":"Item:Q1613678","lastrevid":72344778,"modified":"2026-04-14T04:16:34Z","type":"item","id":"Q1613678","labels":{"en":{"language":"en","value":"Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27--30, 2002. Proceedings"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1793870"}},"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":"Q1613678$91D988ED-7061-45F4-8D7F-98960AE3EA94","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"92c06234f907f5908963ea9e3bb4bea2a44ad854","datavalue":{"value":{"text":"Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27--30, 2002. Proceedings","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1613678$FD45AF7D-A2D5-4E7E-98E3-C564AC8C5F5B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"034f4405f8afe125e472e145d20a3f5fdbc83f65","datavalue":{"value":"0993.00050","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1613678$4ECADF77-DFA6-4C3D-B2B6-19A9B0640A60","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f184aae9498452c1263c3d6f182bf5b4b4346727","datavalue":{"value":"10.1007/3-540-45620-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1613678$78892EDA-E024-4059-9398-5692C7726FEB","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":"Q1613678$03EC5E47-A0F9-4A3D-98E1-36522C5FD605","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"53fcb96a7cb4f5e8cbd012770cf049a4dffd75df","datavalue":{"value":{"time":"+2002-09-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1613678$BD708942-E3BA-4BCE-AB04-8373AFBF34FB","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"053b6d0069d8fc787320c870d96478b9eb4958f5","datavalue":{"value":"The articles of mathematical interest will be reviewed individually. The preceding conference (17th, 2000) has been reviewed (see Zbl 0939.00024).  Indexed articles:  \\textit{Horrocks, Ian}, Reasoning with expressive description logics: Theory and practice, 1-15 [Zbl 1072.68577]  \\textit{Pan, Guoqiang; Sattler, Ulrike; Vardi, Moshe Y.}, BDD-based decision procedures for \\({\\mathcal K}\\), 16-30 [Zbl 1072.68585]  \\textit{Bernard, Andrew; Lee, Peter}, Temporal logic for proof-carrying code, 31-46 [Zbl 1072.68563]  \\textit{Schneck, Robert R.; Necula, George C.}, A gradual approach to a more trustworthy, yet scalable, proof-carrying code, 47-62 [Zbl 1072.68589]  \\textit{Strecker, Martin}, Formal verification of a Java compiler in Isabelle, 63-77 [Zbl 1072.68593]  \\textit{Egly, Uwe}, Embedding lax logic into intuitionistic logic, 78-93 [Zbl 1072.03013]  \\textit{Larchey-Wendling, Dominique}, Combining proof-search and counter-model construction for deciding G\u00f6del-Dummett logic, 94-110 [Zbl 1072.03010]  \\textit{Galmiche, Didier; M\u00e9ry, Daniel}, Connection-based proof search in propositional BI logic, 111-128 [Zbl 1072.68571]  \\textit{M\u00f8ller, Jesper B.}, DDDLIB: A library for solving quantified difference inequalities, 129-133 [Zbl 1072.68583]  \\textit{Hurd, Joe}, An lCF-style interface between HOL and first-order logic, 134-138 [Zbl 1072.68578]  \\textit{Zimmer, J\u00fcrgen; Kohlhase, Michael}, System description: The MathWeb software bus for distributed mathematical reasoning, 139-143 [Zbl 1072.68601]  \\textit{Siekmann, J\u00f6rg; Benzm\u00fcller, Christoph; Brezhnev, Vladimir; Cheikhrouhou, Lassaad; Fiedler, Armin; Franke, Andreas; Horacek, Helmut; Kohlhase, Michael; Meier, Andreas; Melis, Erica; Moschner, Markus; Normann, Immanuel; Pollet, Martin; Sorge, Volker; Ullrich, Carsten; Wirth, Claus-Peter; Zimmer, J\u00fcrgen}, Proof development with \\(\\Omega\\)MEGA, 144-149 [Zbl 1072.68591]  \\textit{Jamnik, Mateja; Kerber, Manfred; Pollet, Martin}, Learn\\(\\Omega\\)matic: System description, 150-155 [Zbl 1072.68579]  \\textit{Areces, Carlos; Heguiabehere, Juan}, HyLoRes 1.0: Direct resolution for hybrid logics, 156-160 [Zbl 1072.68560]  \\textit{Goldberg, Eugene}, Testing satisfiability of CNF formulas by computing a stable set of points, 161-180 [Zbl 1072.68574]  \\textit{Boy de la Tour, Thierry}, A note on symmetry heuristics in SEM, 181-194 [Zbl 1072.68565]  \\textit{Audemard, Gilles; Bertoli, Piergiorgio; Cimatti, Alessandro; Korni\u0142owicz, Artur; Sebastiani, Roberto}, A SAT based approach for solving formulas over Boolean and linear mathematical propositions, 195-210 [Zbl 1072.68562]  \\textit{Ahrendt, Wolfgang}, Deductive search for errors in free data type specifications using model generation, 211-225 [Zbl 1072.68558]  \\textit{Audemard, Gilles; Benhamou, Belaid}, Reasoning by symmetry and function ordering in finite model generation, 226-240 [Zbl 1072.68561]  \\textit{Gramlich, Bernhard; Pichler, Reinhard}, Algorithmic aspects of Herbrand models represented by ground atoms with ground equations, 241-259 [Zbl 1072.68575]  \\textit{Georgieva, Lilia; Hustadt, Ullrich; Schmidt, Renate A.}, A new clausal class decidable by hyperresolution, 260-274 [Zbl 1072.68573]  \\textit{Weidenbach, Christoph; Brahm, Uwe; Hillenbrand, Thomas; Keen, Enno; Theobald, Christian; Topi\u0107, Dalibor}, SPASS version 2.0, 275-279 [Zbl 1072.68596]  \\textit{Schulz, Stephan; Sutcliffe, Geoff}, System description: GrAnDe 1.0, 280-284 [Zbl 1072.68590]  \\textit{Colton, Simon}, The HR program for theorem generation, 285-289 [Zbl 1072.68567]  \\textit{Whalen, Michael; Schumann, Johann; Fischer, Bernd}, AutoBayes/CC -- combining program synthesis with automatic code certification -- system description, 290-294 [Zbl 1072.68597]  \\textit{Zhang, Lintao; Malik, Sharad}, The quest for efficient Boolean satisfiability solvers, 295-313 [Zbl 1072.68599]  \\textit{Borralleras, Cristina; Lucas, Salvador; Rubio, Albert}, Recursive path orderings can be context-sensitive, 314-331 [Zbl 1072.68537]  \\textit{Ganzinger, Harald}, Shostak light, 332-346 [Zbl 1072.68572]  \\textit{Ford, Jonathan; Shankar, Natarajan}, Formal verification of a combination decision procedure, 347-362 [Zbl 1072.68570]  \\textit{Zarba, Calogero G.}, Combining multisets with integers, 363-376 [Zbl 1072.68598]  \\textit{Paulson, Lawrence C.}, The reflection theorem: A study in meta-theoretic reasoning, 377-391 [Zbl 1072.68586]  \\textit{Stump, Aaron; Dill, David L.}, Faster proof checking in the Edinburgh Logical Framework, 392-407 [Zbl 1072.68594]  \\textit{Brown, Chad E.}, Solving for set variables in higher-order theorem proving, 408-422 [Zbl 1072.68566]  \\textit{Kupferman, Orna; Sattler, Ulrike; Vardi, Moshe Y.}, The complexity of the graded \\(\\mu\\)-calculus, 423-437 [Zbl 1072.03014]  \\textit{de Moura, Leonardo; Rue\u00df, Harald; Sorea, Maria}, Lazy theorem proving for bounded model checking over infinite domains, 438-455 [Zbl 1072.68602]  \\textit{Bofill, Miquel; Rubio, Albert}, Well-foundedness is sufficient for completeness of ordered paramodulation, 456-470 [Zbl 1072.68564]  \\textit{Lynch, Christopher; Morawska, Barbara}, Basic syntactic mutation, 471-485 [Zbl 1072.68581]  \\textit{Hillenbrand, Thomas; L\u00f6chner, Bernd}, The next WALDMEISTER loop, 486-500 [Zbl 1072.68576]  \\textit{Andreoli, Jean Marc}, Focussing proof-net construction as a middleware paradigm, 501-516 [Zbl 1072.68559]  \\textit{Baaz, Matthias}, Proof analysis by resolution, 517-531 [Zbl 1072.03516]","type":"string"},"datatype":"string"},"type":"statement","id":"Q1613678$62803AAA-DE8D-4D33-BE30-5B8B2D456057","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6f2c17db95e93f9a5a19ff6c68b3a1df8b0c021e","datavalue":{"value":"00B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1613678$B17E5141-E847-4561-884E-750598E6BAE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1613678$9DC448F3-83B2-4C1C-A52B-F0A826C30DBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f1971b12f93143b2604d15a1750f495d71fae62d","datavalue":{"value":"03-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1613678$D85FA6F9-6DE8-446D-9C45-9AB65554BD62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1613678$A0C8663B-CD9A-43C4-B136-2B2993D727BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1613678$AC9B40EE-9567-40BD-A666-5DE946AEE992","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3afab1f8f62892082fc0179e93c68aa157e6c364","datavalue":{"value":"1793870","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1613678$3E138EB6-54A3-4CE6-9D6A-2B058FF2A6D4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5bf536f4f878472585edc0063230901e80d68c8c","datavalue":{"value":"Copenhagen (Denmark)","type":"string"},"datatype":"string"},"type":"statement","id":"Q1613678$159D66EC-1743-463F-A5CF-3882545A8EA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5c4c4bb5a86a0fdf66f908b603f2f6975f5ef6fc","datavalue":{"value":"Proceedings","type":"string"},"datatype":"string"},"type":"statement","id":"Q1613678$236E051D-E2F4-43D5-9626-7812CE779C05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d83ae477e518ffecea78688f13a2aaaeca13299","datavalue":{"value":"Conference","type":"string"},"datatype":"string"},"type":"statement","id":"Q1613678$4CF7E7CB-C41F-4982-BCCC-F68A4C3B0E21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b3b268b507eecf51b6fcd6400b418dad17dc2be2","datavalue":{"value":"CADE-18","type":"string"},"datatype":"string"},"type":"statement","id":"Q1613678$077CF145-F3C3-42A0-A346-4E6F182A21ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0bf4f74c129274c74f2df90abe98591d25c9e4a0","datavalue":{"value":"Automated deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1613678$9961BECD-E315-430E-9F4C-8D0E2BCFD1A9","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c766f98bf98fe7cf06a05963cc75ed84be39ac3","datavalue":{"value":{"entity-type":"item","numeric-id":31394,"id":"Q31394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1613678$10C95342-C2BB-4CB2-9366-8642150D5B9F","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":"Q1613678$C4C6328B-B748-4FA0-AA58-974A5F8D658D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8d314198763d1d4a8049bf9d7a45f3e6a86207cd","datavalue":{"value":"https://doi.org/10.1007/3-540-45620-1","type":"string"},"datatype":"url"},"type":"statement","id":"Q1613678$93CDD892-F052-4A08-A6DE-13289516F42A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"49a1e182909753561da7aedd868987a66f7dba87","datavalue":{"value":"W2479999086","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1613678$0C413C3E-9231-400F-BCD6-C0E14A9962A8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27--30, 2002. Proceedings","badges":[]}}}}}