Volume •Abstracts •Preface •Authors •Keywords •BibTex Entries

PxTP 2013: Volume Information

PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving

Editors: Jasmin Christian Blanchette and Josef Urban

EPiC Series in Computing•Volume 14

12 articles•132 pages•Published: May 26, 2013

Papers

External Tools for the Formal Proof of the Kepler Conjecture

Thomas C. Hales

1

LEO-II Version 1.5

Christoph Benzmüller and Nik Sultana

2-10

Redirecting Proofs by Contradiction

Jasmin Christian Blanchette

11-26

From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction

Chad E. Brown and Christine Rizkallah

27-42

A Shallow Embedding of Resolution and Superposition Proofs into the $\lambda\Pi$-Calculus Modulo

Guillaume Burel

43-57

Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract)

Zakaria Chihani, Dale Miller and Fabien Renaud

58-66

Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs

Nada Habli and Amy P. Felty

67-76

Initial Experiments on Deriving a Complete HOL Simplification Set

Cezary Kaliszyk and Thomas Sternagel

77-86

Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution

Cezary Kaliszyk and Josef Urban

87-95

Extended Resolution as Certificates for Propositional Logic

96-109

Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4

110-116

Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs

Steffen Juilf Smolka and Jasmin Christian Blanchette

117-132

Keyphrases

analytic tableaux², automatic theorem provers⁵, Binary Decision Diagrams, Certificates², classical, completion, Coq, direct proofs, Extended Resolution, extensional, feature weighting, Flyspeck², higher-order abstract syntax, higher-order logic⁷, HOL Light⁴, HOL4, Hybrid, intensional, Interoperability, Intuitionistic, Isabelle/HOL², Kepler Conjecture, large theories, linear programming, machine learning, OpenTheory, proof assistants³, proof checking², proof theory², proof transport, prover cooperation, Reasoning framework, resolution², rewriting², simple type theory⁵, Skolemization, Sledgehammer², Strategy evolution, structured proofs, syntax translation, tableaux².