Automated Deduction - Cade-13

Saturation-based theorem proving: Past successes and future potential.- A resolution theorem prover for intuitionistic logic.- Proof-terms for classical and intuitionistic resolution.- Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification.- Extensions to a generalization critic for inductive proof.- Learning domain knowledge to improve theorem proving.- Patching faulty conjectures.- Internal analogy in theorem proving.- Termination of theorem proving by reuse.- Termination of algorithms over non-freely generated data types.- ABSFOL: A proof checker with abstraction.- SPASS & FLOTTER version 0.42.- The design of the CADE-13 ATP system competition.- SCAN-Elimination of predicate quantifiers.- GEOTHER: A geometry theorem prover.- Structuring metatheory on inductive definitions.- An embedding of Ruby in Isabelle.- Mechanical verification of mutually recursive procedures.- FasTraC a decentralized traffic control system based on logic programming.- Presenting machine-found proofs.- MUltlog 1.0: Towards an expert system for many-valued logics.- CtCoq: A system presentation.- An introduction to geometry expert.- SiCoTHEO: Simple competitive parallel theorem provers.- What can we hope to achieve from automated deduction?.- Unification algorithms cannot be combined in polynomial time.- Unification and matching modulo nilpotence.- An improved lower bound for the elementary theories of trees.- INKA: The next generation.- XRay: A prolog technology theorem prover for default reasoning: A system description.- IMPS: An updated system description.- The tableau-based theorem prover 3 T A P Version 4.0.- System description generating models by SEM.- Optimizing proof search in model elimination.- An abstract machine for fixed-order dynamically stratified programs.- Unification in pseudo-linear sort theories is decidable.- Theorem proving with group presentations: Examples and questions.- Transforming termination by self-labelling.- Theorem