|
|
PxTP 2013: Author IndexAuthor | 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 |
|
|
|