The crisis in finite mathematics: Automated reasoning as cause and cure -- A divergence critic -- Synthesis of induction orderings for existence proofs -- Lazy generation of induction hypotheses -- The search efficiency of theorem proving strategies -- A method for building models automatically. Experiments with an extension of OTTER -- Model elimination without contrapositives -- Induction using term orderings -- Mechanizable inductive proofs for a class of ? ? formulas -- On the connection between narrowing and proof by consistency -- A fixedpoint approach to implementing (Co)inductive definitions -- On notions of inductive validity for first-order equational clauses -- A new application for explanation-based generalisation within automated deduction -- Semantically guided first-order theorem proving using hyper-linking -- The applicability of logic program analysis and transformation to theorem proving -- Detecting non-provable goals -- A mechanically proof-checked encyclopedia of mathematics: Should we build one? Can we? -- The TPTP problem library -- Combination techniques for non-disjoint equational theories -- Primal grammars and unification modulo a binary clause -- Conservative query normalization on parallel circumscription -- Bottom-up evaluation of Datalog programs with arithmetic constraints -- On intuitionistic query answering in description bases -- Deductive composition of astronomical software from subroutine libraries -- Proof script pragmatics in IMPS -- A mechanization of strong Kleene logic for partial functions -- Algebraic factoring and geometry theorem proving -- Mechanically proving geometry theorems using a combination of Wu's method and Collins' method -- Str?ve and integers -- What is a proof? -- Termination, geometry and invariants -- Ordered chaining for total orderings -- Simple termination revisited -- Termination orderings for rippling -- A novel asynchronous parallelism scheme for first-order logic -- Proving with BDDs and control of information -- Extended path-indexing -- Exporting and reflecting abstract metamathematics -- Associative-commutative deduction with constraints -- AC-superposition with constraints: No AC-unifiers needed -- The complexity of counting problems in equational matching -- Representing proof transformations for program optimization -- Exploring abstract algebra in constructive type theory -- Tactic theorem proving with refinement-tree proofs and metavariables -- Unification in an extensional lambda calculus with ordered function sorts and constant overloading -- Decidable higher-order unification problems -- Theory and practice of minimal modular higher-order E-unification -- A refined version of general E-unification -- A completion-based method for mixed universal and rigid E-unification -- On pot, pans and pudding or how to discover generalised critical Pairs -- Semantic tableaux with ordering restrictions -- Strongly analytic tableaux for normal modal logics -- Reconstructing proofs at the assertion level -- Problems on the generation of finite models -- Combining symbolic computation and theorem proving: Some problems of Ramanujan -- SCOTT: Semantically constrained otter system description -- Protein: A PROver with a Theory Extension INterface -- DELTA — A bottom-up preprocessor for top-down theorem provers -- SETHEO V3.2: Recent developments -- KoMeT -- ?-MKRP: A proof development environment -- LeanT A P: Lean tableau-based theorem proving -- FINDER: Finite domain enumerator system description -- Symlog automated advice in Fitch-style proof construction -- KEIM: A toolkit for automated deduction -- Elf: A meta-language for deductive systems -- EUODHILOS-II on top of GNU epoch -- Pi: An interactive derivation editor for the calculus of partial inductive definitions -- Mollusc a general proof-development shell for sequent-based logics -- KITP-93: An automated inference system for program analysis -- SPIKE: A system for sufficient completeness and parameterized inductive proofs -- Distributed theorem proving by Peers.

This volume contains the reviewed papers presented at the 12th International Conference on Automated Deduction (CADE-12) held at Nancy, France in June/July 1994. The 67 papers presented were selected from 177 submissions and document many of the most important research results in automated deduction since CADE-11 was held in June 1992. The volume is organized in chapters on heuristics, resolution systems, induction, controlling resolutions, ATP problems, unification, LP applications, special-purpose provers, rewrite rule termination, ATP efficiency, AC unification, higher-order theorem proving, natural systems, problem sets, and system descriptions.