PAAR-2014: Keyword Index

Keyword	Papers
a
ATP Competitions	Machine Learner for Automated Reasoning 0.4 and 0.5
automated reasoning	Machine Learner for Automated Reasoning 0.4 and 0.5
automated theorem proving	The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics Beagle as a HOL4 external ATP method Automated Theorem Proving using the TPTP Process Instruction Language
automated theorem proving process	Automated Theorem Proving using the TPTP Process Instruction Language
b
Beagle	Beagle as a HOL4 external ATP method
c
constraints	A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
d
de Bruijn	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
Description Logics	The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics
discrimination tree	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
e
EPR	The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics
equational logic	A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
f
first-order logic	The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics
formal mathematics	Machine Learner for Automated Reasoning 0.4 and 0.5
g
geometric logic	Razor: Provenance and Exploration in Model-Finding
h
HOL4	Beagle as a HOL4 external ATP method
i
instance-based theorem proving	SGGS Theorem Proving: an Exposition
l
large theories	Machine Learner for Automated Reasoning 0.4 and 0.5
m
machine learning	Machine Learner for Automated Reasoning 0.4 and 0.5
model finding	A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories Razor: Provenance and Exploration in Model-Finding
model-based theorem proving	SGGS Theorem Proving: an Exposition
p
polymorphism	Polymorphic+Typeclass Superposition
prime implicates	A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
Provenance	Razor: Provenance and Exploration in Model-Finding
q
Quantifier Instantiation	A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories
s
semantic guidance	SGGS Theorem Proving: an Exposition
substitution	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
superposition	Polymorphic+Typeclass Superposition
superposition calculus	A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories
t
term representation	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
theorem proving	Polymorphic+Typeclass Superposition
TPTP	Automated Theorem Proving using the TPTP Process Instruction Language
TPTP Process Instruction language	Automated Theorem Proving using the TPTP Process Instruction Language
u
unification	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation