PxTP 2013: Keyword Index

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