Automated Reasoning

Invited Talks.- Mathematical Theory Exploration.- Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation.- Representing and Reasoning with Operational Semantics.- Session 1. Proofs.- Flyspeck I: Tame Graphs.- Automatic Construction and Verification of Isotopy Invariants.- Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms.- Using the TPTP Language for Writing Derivations and Finite Interpretations.- Session 2. Search.- Stratified Context Unification Is NP-Complete.- A Logical Characterization of Forward and Backward Chaining in the Inverse Method.- Connection Tableaux with Lazy Paramodulation.- Blocking and Other Enhancements for Bottom-Up Model Generation Methods.- Session 3. System Description 1.- The MathServe System for Semantic Web Reasoning Services.- System Description: GCLCprover + GeoThms.- A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms.- Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation.- Session 4. Higher-Order Logic.- Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics.- Towards Self-verification of HOL Light.- An Interpretation of Isabelle/HOL in HOL Light.- Combining Type Theory and Untyped Set Theory.- Session 5. Proof Theory.- Cut-Simulation in Impredicative Logics.- Interpolation in Local Theory Extensions.- Canonical Gentzen-Type Calculi with (n,k)-ary Quantifiers.- Dynamic Logic with Non-rigid Functions.- Session 6. System Description 2.- AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework.- CEL - A Polynomial-Time Reasoner for Life Science Ontologies.- FaCT++ Description Logic Reasoner: System Description.- Importing HOL into Isabelle/HOL.- Session 7. Search.- Geometric Resolution: A Proof Procedure Based on Finite Model Search.- A Powerful Technique to Eliminate Isomorphism in Finite Model Search.- Automation of Recursive Path Ordering