A |

analytic tableaux | From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction Extended Resolution as Certificates for Propositional Logic |

automatic theorem provers | LEO-II Version 1.5 Redirecting Proofs by Contradiction A Shallow Embedding of Resolution and Superposition Proofs into the $\lambda\Pi$-Calculus Modulo Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs |

B |

Binary Decision Diagrams | Extended Resolution as Certificates for Propositional Logic |

C |

Certificates | Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract) Extended Resolution as Certificates for Propositional Logic |

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

completion | Initial Experiments on Deriving a Complete HOL Simplification Set |

Coq | Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs |

D |

direct proofs | Redirecting Proofs by Contradiction |

E |

Extended Resolution | Extended Resolution as Certificates for Propositional Logic |

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

F |

feature weighting | Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution |

Flyspeck | External Tools for the Formal Proof of the Kepler Conjecture Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution |

H |

higher-order abstract syntax | Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs |

higher-order logic | External Tools for the Formal Proof of the Kepler Conjecture LEO-II Version 1.5 From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction Initial Experiments on Deriving a Complete HOL Simplification Set Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4 Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs |

HOL Light | External Tools for the Formal Proof of the Kepler Conjecture Initial Experiments on Deriving a Complete HOL Simplification Set Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4 |

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

Hybrid | Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs |

I |

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

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

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

Isabelle/HOL | Redirecting Proofs by Contradiction Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs |

K |

Kepler Conjecture | External Tools for the Formal Proof of the Kepler Conjecture |

L |

large theories | Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution |

linear programming | External Tools for the Formal Proof of the Kepler Conjecture |

M |

machine learning | Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution |

O |

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

P |

proof assistants | Redirecting Proofs by Contradiction Initial Experiments on Deriving a Complete HOL Simplification Set Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs |

proof checking | A Shallow Embedding of Resolution and Superposition Proofs into the $\lambda\Pi$-Calculus Modulo Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract) |

proof theory | From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract) |

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

prover cooperation | LEO-II Version 1.5 |

R |

Reasoning framework | Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs |

resolution | LEO-II Version 1.5 Redirecting Proofs by Contradiction |

rewriting | A Shallow Embedding of Resolution and Superposition Proofs into the $\lambda\Pi$-Calculus Modulo Initial Experiments on Deriving a Complete HOL Simplification Set |

S |

simple type theory | LEO-II Version 1.5 From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction Initial Experiments on Deriving a Complete HOL Simplification Set Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4 Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs |

Skolemization | Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs |

Sledgehammer | Redirecting Proofs by Contradiction Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs |

Strategy evolution | Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution |

structured proofs | Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs |

syntax translation | Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs |

T |

tableaux | From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction Extended Resolution as Certificates for Propositional Logic |