| 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 |
