Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27--30, 2002. Proceedings (Q1613678)

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ödel-Dummett logic, 94-110 [Zbl 1072.03010] \textit{Galmiche, Didier; Méry, Daniel}, Connection-based proof search in propositional BI logic, 111-128 [Zbl 1072.68571] \textit{Møller, 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ürgen; Kohlhase, Michael}, System description: The MathWeb software bus for distributed mathematical reasoning, 139-143 [Zbl 1072.68601] \textit{Siekmann, Jörg; Benzmüller, 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ürgen}, 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łowicz, 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ć, 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ß, 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öchner, 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]