Automated Deduction - CADE-11

The impossibility of the automation of logical reasoning.- Automatic proofs in mathematical logic and analysis.- Proving geometry statements of constructive type.- The central variable strategy of str?ve.- Unification in the union of disjoint equational theories: Combining decision procedures.- Reduction and unification in Lambda calculi with subtypes.- A combinatory logic approach to higher-order E-unification (extended abstract).- Cycle unification.- A parallel completion procedure for term rewriting systems.- Grammar rewriting.- Polynomial interpretations and the complexity of algorithms.- Uniform traversal combinators: Definition, use and properties.- Sorted unification using set constraints.- An abstract view of sorted unification.- Unification in order-sorted algebras with overloading.- Puzzles and paradoxes.- Experiments in automated deduction with condensed detachment.- Caching and lemmaizing in model elimination theorem provers.- LIM+ challenge problems by RUE hyper-resolution.- Computing prime implicates incrementally.- Linear-input subset analysis.- Theoretical study of symmetries in propositional calculus and applications.- Difference matching.- Using middle-out reasoning to control the synthesis of tail-recursive programs.- The use of proof plans to sum series.- Disproving conjectures.- An interval-based temporal logic in a multivalued setting.- A normal form for first-order temporal formulae.- Semantic entailment in non classical logics based on proofs found in classical logic.- Embedding negation as failure into a model generation theorem prover.- Automated correctness proofs of machine code programs for a commercial microprocessor.- Proving the Chinese remainder theorem by the cover set induction.- Automatic program optimization through proof transformation.- Proof search theory and practice in the (former) USSR (Tentative).- Basic paramodulation and superposition.- Theorem proving with ordering constrained clauses.- The special-relation rules are