Automated deduction -- CADE-19. 19th international conference on automated deduction, Miami Beach, FL, USA, July 28 -- August 2, 2003. Proceedings (Q1412856)

The articles of this volume will be reviewed individually. The preceding conference has been reviewed (see Zbl 0993.00050). Indexed articles: \textit{Meseguer, José; Palomino, Miguel; Martí-Oliet, Narciso}, Equational abstractions., 2-16 [Zbl 1278.68185] \textit{Giesl, Jürgen; Kapur, Deepak}, Deciding inductive validity of equations., 17-31 [Zbl 1278.68262] \textit{Hirokawa, Nao; Middeldorp, Aart}, Automating the dependency pair method., 32-46 [Zbl 1278.68264] \textit{Korovin, Konstantin; Voronkov, Andrei}, An AC-compatible Knuth-Bendix order., 47-59 [Zbl 1278.68268] \textit{Lutz, Carsten; Sattler, Ulrike; Tendera, Lidia}, The complexity of finite model reasoning in description logics., 60-74 [Zbl 1278.68288] \textit{Pan, Guoqiang; Vardi, Moshe Y.}, Optimizing a BDD-based modal solver., 75-89 [Zbl 1278.68277] \textit{Hladik, Jan; Sattler, Ulrike}, A translation of looping alternating automata into description logics., 90-105 [Zbl 1278.68265] \textit{Crary, Karl; Sarkar, Susmit}, Foundational certified code in a metalogical framework., 106-120 [Zbl 1278.68255] \textit{Mehta, Farhad; Nipkow, Tobias}, Proving pointer programs in higher-order logic., 121-135 [Zbl 1278.68274] \textit{Hendriks, Dimitri; van Oostrom, Vincent}, \(\rightthreetimes\), 136-150 [Zbl 1277.03011] \textit{Stump, Aaron}, Subset types and partial functions., 151-165 [Zbl 1278.03029] \textit{Gulwani, Sumit; Necula, George C.}, A randomized satisfiability procedure for arithmetic and uninterpreted function symbols., 167-181 [Zbl 1278.68342] \textit{Ganzinger, Harald; Hillenbrand, Thomas; Waldmann, Uwe}, Superposition modulo a Shostak theory., 182-196 [Zbl 1278.68260] \textit{Krstić, Sava; Conchon, Sylvain}, Canonization for disjoint unions of theories., 197-211 [Zbl 1278.68269] \textit{Ringeissen, Christophe}, Matching in a class of combined non-disjoint theories., 212-227 [Zbl 1278.68280] \textit{Belinfante, Johan Gijsbertus Frederik}, Reasoning about iteration in Gödel's class theory., 228-242 [Zbl 1260.68365] \textit{Manolios, Panagiotis; Vroon, Daron}, Algorithms for ordinal arithmetic., 243-257 [Zbl 1278.68272] \textit{Cohen, Arjeh; Murray, Scott H.; Pollet, Martin; Sorge, Volker}, Certifying solutions to permutation group problems., 258-273 [Zbl 1278.68254] \textit{Colton, Simon; Huczynska, Sophie}, The Homer system., 289-294 [Zbl 1214.68332] \textit{Deplagne, Eric; Kirchner, Claude; Kirchner, Hélène; Nguyen, Quang Huy}, Proof search and proof check for equational and inductive theorems., 297-316 [Zbl 1278.68257] \textit{Ganzinger, Harald; Stuber, Jürgen}, Superposition with equivalence reasoning and delayed clause normal form transformation., 335-349 [Zbl 1278.68261] \textit{Baumgartner, Peter; Tinelli, Cesare}, The model evolution calculus., 350-364 [Zbl 1278.68249] \textit{de Nivelle, Hans}, Translation of resolution proofs into short first-order proofs without choice axioms., 365-379 [Zbl 1278.03032] \textit{Degtyarev, Anatoly; Fisher, Michael; Konev, Boris}, Monodic temporal resolution., 397-411 [Zbl 1272.03090] \textit{Schmidt, Renate A.; Hustadt, Ullrich}, A principle for incorporating axioms into the first-order translation of modal formulae., 412-426 [Zbl 1278.03031] \textit{Lynch, Christopher}, Schematic saturation for decision and unification problems., 427-441 [Zbl 1278.68271] \textit{Anantharaman, Siva; Narendran, Paliath; Rusinowitch, Michael}, Unification modulo ACUI plus homomorphisms/distributivity., 442-457 [Zbl 1278.68246] \textit{Choppella, Venkatesh; Haynes, Christopher T.}, Source-tracking unification., 458-472 [Zbl 1278.68252] \textit{Pientka, Brigitte; Pfenning, Frank}, Optimizing higher-order pattern unification., 473-487 [Zbl 1278.68278] \textit{Schmidt-Schauß, Manfred}, Decidability of arity-bounded higher-order matching., 488-502 [Zbl 1278.68281]