PAAR 2014 PROCEEDINGS: KEYWORD INDEX

Papers Papers with Abstracts Preface Author Index Keyword Index

Shortcuts: A B C D E F G H I L M O P Q S T U

A
Artificial Intelligence	Machine Learner for Automated Reasoning 0.4 and 0.5 (PDF, talk) BliStr: The Blind Strategymaker (PDF, talk)
ATP	Beagle as a HOL4 external ATP method (PDF, talk)
ATP Competitions	Machine Learner for Automated Reasoning 0.4 and 0.5 (PDF, talk)
ATP process	Automated Theorem Proving using the TPTP Process Instruction Language (PDF, talk)
automated reasoning	Machine Learner for Automated Reasoning 0.4 and 0.5 (PDF, talk)
automated theorem proving	The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics (PDF, talk) Automated Theorem Proving using the TPTP Process Instruction Language (PDF, talk) BliStr: The Blind Strategymaker (PDF, talk)
B
Beagle	Beagle as a HOL4 external ATP method (PDF, talk)
C
Constraints	A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses (PDF, talk)
D
De Bruijn	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation (PDF, talk)
discrimination tree	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation (PDF, talk)
E
equational logic	A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses (PDF, talk)
F
formal mathematics	Machine Learner for Automated Reasoning 0.4 and 0.5 (PDF, talk)
G
geometric logic	Razor: Provenance and Exploration in Model-Finding (PDF, talk)
H
HOL4	Beagle as a HOL4 external ATP method (PDF, talk)
I
instance-based theorem proving	SGGS Theorem Proving: an Exposition (PDF, talk)
L
Large Theories	Machine Learner for Automated Reasoning 0.4 and 0.5 (PDF, talk)
large-theory automated reasoning	BliStr: The Blind Strategymaker (PDF, talk)
Logics	The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics (PDF, talk)
M
machine learning	Machine Learner for Automated Reasoning 0.4 and 0.5 (PDF, talk)
Model Finding	A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories (PDF, talk)
model-based theorem proving	SGGS Theorem Proving: an Exposition (PDF, talk)
model-finding	Razor: Provenance and Exploration in Model-Finding (PDF, talk)
O
OCaml	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation (PDF, talk)
P
polymorphism	Polymorphic+Typeclass Superposition (PDF, talk)
prime impliquates	A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses (PDF, talk)
provenance	Razor: Provenance and Exploration in Model-Finding (PDF, talk)
Q
Quantifier Instantiation	A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories (PDF, talk)
S
semantic guidance	SGGS Theorem Proving: an Exposition (PDF, talk)
strategy development	BliStr: The Blind Strategymaker (PDF, talk)
substitution	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation (PDF, talk)
superposition	Polymorphic+Typeclass Superposition (PDF, talk)
superposition calculus	A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories (PDF, talk)
T
term representation	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation (PDF, talk)
theorem proving	Polymorphic+Typeclass Superposition (PDF, talk)
TPTP Process Instruction language	Automated Theorem Proving using the TPTP Process Instruction Language (PDF, talk)
Translation	The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics (PDF, talk) Beagle as a HOL4 external ATP method (PDF, talk)
U
Unification	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation (PDF, talk)