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 |