PxTP 2013:Keyword Index

KeywordPapers
A
analytic tableauxFrom Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction
Extended Resolution as Certificates for Propositional Logic
automatic theorem proversLEO-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 DiagramsExtended Resolution as Certificates for Propositional Logic
C
CertificatesChecking Foundational Proof Certificates for First-Order Logic (Extended Abstract)
Extended Resolution as Certificates for Propositional Logic
classicalFrom Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction
completionInitial Experiments on Deriving a Complete HOL Simplification Set
CoqTranslating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs
D
direct proofsRedirecting Proofs by Contradiction
E
Extended ResolutionExtended Resolution as Certificates for Propositional Logic
extensionalFrom Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction
F
feature weightingStronger Automation for Flyspeck by Feature Weighting and Strategy Evolution
FlyspeckExternal Tools for the Formal Proof of the Kepler Conjecture
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution
H
higher-order abstract syntaxTranslating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs
higher-order logicExternal 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 LightExternal 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
HOL4Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4
HybridTranslating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs
I
intensionalFrom Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction
InteroperabilityA Shallow Embedding of Resolution and Superposition Proofs into the $\lambda\Pi$-Calculus Modulo
IntuitionisticFrom Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction
Isabelle/HOLRedirecting Proofs by Contradiction
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs
K
Kepler ConjectureExternal Tools for the Formal Proof of the Kepler Conjecture
L
large theoriesStronger Automation for Flyspeck by Feature Weighting and Strategy Evolution
linear programmingExternal Tools for the Formal Proof of the Kepler Conjecture
M
machine learningStronger Automation for Flyspeck by Feature Weighting and Strategy Evolution
O
OpenTheoryChallenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4
P
proof assistantsRedirecting Proofs by Contradiction
Initial Experiments on Deriving a Complete HOL Simplification Set
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs
proof checkingA Shallow Embedding of Resolution and Superposition Proofs into the $\lambda\Pi$-Calculus Modulo
Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract)
proof theoryFrom Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction
Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract)
proof transportChallenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4
prover cooperationLEO-II Version 1.5
R
Reasoning frameworkTranslating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs
resolutionLEO-II Version 1.5
Redirecting Proofs by Contradiction
rewritingA 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 theoryLEO-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
SkolemizationRobust, Semi-Intelligible Isabelle Proofs from ATP Proofs
SledgehammerRedirecting Proofs by Contradiction
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs
Strategy evolutionStronger Automation for Flyspeck by Feature Weighting and Strategy Evolution
structured proofsRobust, Semi-Intelligible Isabelle Proofs from ATP Proofs
syntax translationTranslating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs
T
tableauxFrom Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction
Extended Resolution as Certificates for Propositional Logic