|
|
PxTP 2013: Author Index| Author | Papers |
|---|
| B | | Benzmüller, Christoph | LEO-II Version 1.5 | | Blanchette, Jasmin Christian | Redirecting Proofs by Contradiction Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs | | Brown, Chad | From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction | | Burel, Guillaume | A Shallow Embedding of Resolution and Superposition Proofs into the $\lambda\Pi$-Calculus Modulo | | C | | Chihani, Zakaria | Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract) | | F | | Felty, Amy | Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs | | H | | Habli, Nada | Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs | | Hales, Thomas | External Tools for the Formal Proof of the Kepler Conjecture | | K | | Kaliszyk, Cezary | Initial Experiments on Deriving a Complete HOL Simplification Set Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution | | Keller, Chantal | Extended Resolution as Certificates for Propositional Logic | | Kumar, Ramana | Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4 | | M | | Miller, Dale | Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract) | | R | | Renaud, Fabien | Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract) | | Rizkallah, Christine | From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction | | S | | Smolka, Steffen Juilf | Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs | | Sternagel, Thomas | Initial Experiments on Deriving a Complete HOL Simplification Set | | Sultana, Nik | LEO-II Version 1.5 | | U | | Urban, Josef | Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution |
|
|
|