PAAR-2014:Keyword Index

KeywordPapers
A
ATP CompetitionsMachine Learner for Automated Reasoning 0.4 and 0.5
automated reasoningMachine Learner for Automated Reasoning 0.4 and 0.5
automated theorem provingThe 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 processAutomated Theorem Proving using the TPTP Process Instruction Language
B
BeagleBeagle as a HOL4 external ATP method
C
constraintsA Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
D
de BruijnLogtk : A Logic ToolKit for Automated Reasoning and its Implementation
Description LogicsThe Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics
discrimination treeLogtk : A Logic ToolKit for Automated Reasoning and its Implementation
E
EPRThe Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics
equational logicA Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
F
first-order logicThe Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics
formal mathematicsMachine Learner for Automated Reasoning 0.4 and 0.5
G
geometric logicRazor: Provenance and Exploration in Model-Finding
H
HOL4Beagle as a HOL4 external ATP method
I
instance-based theorem provingSGGS Theorem Proving: an Exposition
L
large theoriesMachine Learner for Automated Reasoning 0.4 and 0.5
M
machine learningMachine Learner for Automated Reasoning 0.4 and 0.5
model findingA Model Guided Instantiation Heuristic for the Superposition Calculus with Theories
Razor: Provenance and Exploration in Model-Finding
model-based theorem provingSGGS Theorem Proving: an Exposition
P
polymorphismPolymorphic+Typeclass Superposition
prime implicatesA Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
ProvenanceRazor: Provenance and Exploration in Model-Finding
Q
Quantifier InstantiationA Model Guided Instantiation Heuristic for the Superposition Calculus with Theories
S
semantic guidanceSGGS Theorem Proving: an Exposition
substitutionLogtk : A Logic ToolKit for Automated Reasoning and its Implementation
superpositionPolymorphic+Typeclass Superposition
superposition calculusA Model Guided Instantiation Heuristic for the Superposition Calculus with Theories
T
term representationLogtk : A Logic ToolKit for Automated Reasoning and its Implementation
theorem provingPolymorphic+Typeclass Superposition
TPTPAutomated Theorem Proving using the TPTP Process Instruction Language
TPTP Process Instruction languageAutomated Theorem Proving using the TPTP Process Instruction Language
U
unificationLogtk : A Logic ToolKit for Automated Reasoning and its Implementation