Home
EPiC Series
Kalpa Publications
Preprints
For Authors
For Editors
Volume
•
Abstracts
•
Preface
•
Authors
•
Keywords
•
BibTex Entries
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
Copyright © 2012-2024 easychair.org. All rights reserved.