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 proving in cancellative abelian monoids (extended abstract).- On the practical value of different definitional translations to normal form.- Converting non-classical matrix proofs into sequent-style systems.- Efficient model generation through compilation.- Algebra and automated deduction.- On Shostak's decision procedure for combinations of theories.- Ground resolution with group computations on semantic symmetries.- A new method for knowledge compilation: The achievement by cycle search.- Rewrite semantics for production rule systems: Theory and applications.- Experiments in the heuristic use of past proof experience.- Lemma discovery in automating induction.- Advanced indexing operations on substitution trees.- Semantic trees revisited: Some new completeness results.- Building decision procedures for modal logics from propositional decision procedures — The case study of modal K.- Resolution-based calculi for modal and temporal logics.- Tableaux and algorithms for Propositional Dynamic Logic with Converse.- Reflection of formal tactics in a deductive reflection framework.- Walther recursion.- Proof search with set variable instantiation in the Calculus of Constructions.- Search strategies for resolution in temporal logics.- Optimal axiomatizations for multiple-valued operators and quantifiers based on semi-lattices.- Grammar specification in categorial logics and theorem proving.- Path indexing for AC-theories.- More Church-Rosser proofs (in Isabelle/HOL).- Partitioning methods for satisfiability testing on large formulas.